`RellichKondrachov.MeasureTheory.Function.LpSpace.ChangeMeasureLeSmul` #

Transfer L^p spaces across comparable measures.

This file packages a common pattern used in manifold analysis: if two measures are comparable up to a scalar multiple (ν ≤ c • μ with c ≠ ∞), then any L^p(μ) function is also in L^p(ν), and the identity map induces a bounded linear operator Lp E p μ →L[ℝ] Lp E p ν.

If the measures are mutually comparable (ν ≤ c₁ • μ and μ ≤ c₂ • ν), we get a continuous linear equivalence between Lp spaces, and compactness of operators can be transported across it.

Tracking: Beads lean-103.5.2.26.5.3.3.1.

source

noncomputable def MeasureTheory.Lp.changeMeasureFun {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} {E : Type u_2} [NormedAddCommGroup E] {p c : ENNReal} (hc : c ≠ ⊤) (hν : ν ≤ c • μ) (f : ↥(Lp E p μ)) :

↥(Lp E p ν)

View an Lp function under a measure bounded by a finite multiple of the original measure.

Equations

MeasureTheory.Lp.changeMeasureFun hc hν f = MeasureTheory.MemLp.toLp (fun (x : α) => ↑↑f x) ⋯

Instances For

source

noncomputable def MeasureTheory.Lp.changeMeasureₗ {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {p c : ENNReal} (hc : c ≠ ⊤) (hν : ν ≤ c • μ) :

↥(Lp E p μ) →ₗ[ℝ ] ↥(Lp E p ν)

The identity map as a linear map Lp E p μ →ₗ[ℝ] Lp E p ν under a measure bound ν ≤ c • μ.

Equations

MeasureTheory.Lp.changeMeasureₗ hc hν = { toFun := MeasureTheory.Lp.changeMeasureFun hc hν, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

noncomputable def MeasureTheory.Lp.changeMeasureL {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {p : ENNReal} [Fact (1 ≤ p)] {c : ENNReal} (hc : c ≠ ⊤) (hν : ν ≤ c • μ) (hp : p ≠ ⊤) :

↥(Lp E p μ) →L[ℝ ] ↥(Lp E p ν)

The identity map as a continuous linear map Lp E p μ →L[ℝ] Lp E p ν under ν ≤ c • μ.

This is stated for p ≠ ∞ (the only case needed in this repo; in particular we use p = 2).

Equations

MeasureTheory.Lp.changeMeasureL hc hν hp = (MeasureTheory.Lp.changeMeasureₗ hc hν).mkContinuous (c ^ (1 / p).toReal).toReal ⋯

Instances For

source

theorem MeasureTheory.Lp.changeMeasureL_coeFn_ae_eq {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {p : ENNReal} [Fact (1 ≤ p)] {c : ENNReal} (hc : c ≠ ⊤) (hν : ν ≤ c • μ) (hp : p ≠ ⊤) (f : ↥(Lp E p μ)) :

↑↑((changeMeasureL hc hν hp) f) =ᵐ[ν] ↑↑f

source

theorem MeasureTheory.Lp.changeMeasureL_congr {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {p : ENNReal} [Fact (1 ≤ p)] {c : ENNReal} (hc₁ hc₂ : c ≠ ⊤) (hν₁ hν₂ : ν ≤ c • μ) (hp₁ hp₂ : p ≠ ⊤) :

changeMeasureL hc₁ hν₁ hp₁ = changeMeasureL hc₂ hν₂ hp₂

Mutual comparability: `Lp` equivalence #

If we have both ν ≤ c₁ • μ and μ ≤ c₂ • ν (with finite constants), then the identity map gives a continuous linear equivalence between the two Lp spaces.

source

noncomputable def MeasureTheory.Lp.changeMeasureEquiv {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {p : ENNReal} [Fact (1 ≤ p)] {c₁ c₂ : ENNReal} (hc₁ : c₁ ≠ ⊤) (hc₂ : c₂ ≠ ⊤) (hν : ν ≤ c₁ • μ) (hμ : μ ≤ c₂ • ν) (hp : p ≠ ⊤) :

↥(Lp E p μ) ≃L[ℝ ] ↥(Lp E p ν)

If ν ≤ c₁ • μ and μ ≤ c₂ • ν (with c₁, c₂ ≠ ∞) and p ≠ ∞, then the identity map induces a continuous linear equivalence Lp E p μ ≃L[ℝ] Lp E p ν.

Equations