Transporting an Lp element along an equality of measures

Equal measures give equal (not merely isomorphic) Lp types, so an element of Lp E p μ can be moved to Lp E p ν by cast whenever μ = ν. The cast is the identity on representatives, which is what TauCeti.coeFn_cast_lp records.

This is the bookkeeping a statement needs when a space is defined with one description of its measure and used with another, for example a basis of L²(γ) fed to TauCeti.weightL2Isometry, whose domain is spelled L²(volume.withDensity …).

Bundling that cast as a linear isometric equivalence, TauCeti.castLpₗᵢ, is what lets an equality of measures be composed with other isometries — for instance to feed HilbertBasis.mapₗᵢ, which needs a genuine ≃ₗᵢ and not a cast.

Main statements

• TauCeti.coeFn_cast_lp: the cast does not move representatives.
• TauCeti.castLpₗᵢ: the cast as a linear isometric equivalence.

@[simp]

theorem TauCeti.coeFn_cast_lp {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ ν : MeasureTheory.Measure α} (h : μ = ν) (f : ↥(MeasureTheory.Lp E p μ)) (x : α) : ↑↑(cast ⋯ f) x = ↑↑f x

Transporting an Lp element along an equality of measures does not move its representative. The cast is along the equality of types ↥(Lp E p μ) = ↥(Lp E p ν) induced by μ = ν, so it acts as the identity on functions.

noncomputable def TauCeti.castLpₗᵢ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace α] [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ ν : MeasureTheory.Measure α} (h : μ = ν) : ↥(MeasureTheory.Lp E p μ) ≃ₗᵢ[𝕜] ↥(MeasureTheory.Lp E p ν)

Equal measures give isometrically identical Lp spaces. This is cast along the equality of types ↥(Lp E p μ) = ↥(Lp E p ν), packaged as a linear isometric equivalence so that it can be composed with other isometries; TauCeti.coeFn_castLpₗᵢ records that it still does not move representatives.

Equations

• TauCeti.castLpₗᵢ h = h ▸ LinearIsometryEquiv.refl 𝕜 ↥(MeasureTheory.Lp E p μ)

@[simp]

theorem TauCeti.castLpₗᵢ_apply {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace α] [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ ν : MeasureTheory.Measure α} (h : μ = ν) (f : ↥(MeasureTheory.Lp E p μ)) : (castLpₗᵢ h) f = cast ⋯ f

The isometric cast is the transport cast. This is what lets a consumer rewrite the transported vector itself, rather than only its representative, so no extensionality step is needed to get at it.

theorem TauCeti.coeFn_castLpₗᵢ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace α] [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ ν : MeasureTheory.Measure α} (h : μ = ν) (f : ↥(MeasureTheory.Lp E p μ)) (x : α) : ↑↑((castLpₗᵢ h) f) x = ↑↑f x

The isometric cast does not move representatives. This is not itself a simp lemma: TauCeti.castLpₗᵢ_apply followed by TauCeti.coeFn_cast_lp already reduces its left-hand side, so simp reaches the same normal form and marking it too would only duplicate them.

@[simp]

theorem TauCeti.castLpₗᵢ_symm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace α] [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ ν : MeasureTheory.Measure α} (h : μ = ν) : (castLpₗᵢ h).symm = castLpₗᵢ ⋯

The inverse of the isometric cast is the cast along the reversed equality.