L² transport by measure and target isometries

Applying a target isometry pointwise is an isometry of L² classes.

Pointwise target transport has the prescribed a.e. representative.

noncomputable def LiebThirring.l2TargetEquiv {α : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (μ : MeasureTheory.Measure α) (A : E ≃ₗᵢ[ℂ] F) : ↥(MeasureTheory.Lp E 2 μ) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp F 2 μ)

Applying a target isometry pointwise is an isometry of L² classes.

Equations

• LiebThirring.l2TargetEquiv μ A = { toFun := (↑↑A).compLp, map_add' := ⋯, map_smul' := ⋯, invFun := (↑↑A.symm).compLp, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

theorem LiebThirring.l2TargetEquiv_ae {α : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (μ : MeasureTheory.Measure α) (A : E ≃ₗᵢ[ℂ] F) (f : ↥(MeasureTheory.Lp E 2 μ)) : ↑↑((l2TargetEquiv μ A) f) =ᵐ[μ] fun (x : α) => A (↑↑f x)

Pointwise target transport has the prescribed a.e. representative.

noncomputable def LiebThirring.l2PullbackEquiv {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℂ E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β) (he : MeasureTheory.MeasurePreserving (⇑e) μ ν) : ↥(MeasureTheory.Lp E 2 ν) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp E 2 μ)

Pullback by a measure-preserving measurable equivalence is an L² isometry.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.l2PullbackEquiv_ae {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℂ E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β) (he : MeasureTheory.MeasurePreserving (⇑e) μ ν) (f : ↥(MeasureTheory.Lp E 2 ν)) : ↑↑((l2PullbackEquiv e he) f) =ᵐ[μ] fun (x : α) => ↑↑f (e x)

The measure transport is pullback on a.e. representatives.