Lean/Mathlib: multiplication operator on L² and isometric extension from C(X)

To build T ≅ M_z on L²(μ) you need almost nothing new. (1) Mathlib's LinearMap.extendOfIsometry (f : E →ₗ F) (h_dense : DenseRange e) (h_norm : ∀ x, ‖f x‖ = ‖e x‖) (Analysis/Normed/Operator/Extend) extends f ↦ f(T)x from C(X,ℂ) to Lp ℂ 2 μ. Use e := (ContinuousMap.toLp 2 μ ℂ).toLinearMap, which is dense by ContinuousMap.toLp_denseRange (compact X, finite measure). (2) Multiplication by g ∈ L^∞ on L² is ((ContinuousLinearMap.mul ℂ ℂ).holderL μ 2 ∞ 2).flip g (MeasureTheory/Function/Holder, using HolderTriple.instInfty). coeFn_holder gives the a.e. formula. You need open ENNReal for ∞. (3) For the L² norm of toLp f, use ContinuousMap.inner_toLp (import L2Space) plus integral_re. (4) Intertwining on the dense set, then DenseRange.equalizer. Surjectivity for a cyclic vector: the range of an isometry is closed (isometry.isClosedEmbedding.isClosed_range), then LinearIsometryEquiv.ofSurjective.