PL1/WeightedL1.lean

All source files · Download exact source

SHA-256: d91cb3eda6a4a8315ad699e1be3f37507f20235ab86c07eebee59f623edb9d6c

1import PL1.IntervalModel23noncomputable section4open MeasureTheory Set Filter5open scoped ENNReal NNReal Topology67namespace PL1.IntervalModel89variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]10variable (μ : Measure Ω) (w : Ω → ℝ≥0) (hw : Measurable w) (hw0 : ∀ x, w x ≠ 0)1112include hw hw01314/-- Reweighting L1 by multiplication with a positive density, over either scalar field. -/15def densityIsometry : Lp 𝕜 1 (μ.withDensity (fun x => w x)) →ₗᵢ[𝕜] Lp 𝕜 1 μ where16  toFun := withDensitySMulLI μ hw17  map_add' := (withDensitySMulLI μ hw).map_add18  map_smul' := by19    intro c u20    apply Lp.ext21    simp only [withDensitySMulLI_apply, RingHom.id_apply]22    filter_upwards [(ae_withDensity_iff hw.coe_nnreal_ennreal).1 (Lp.coeFn_smul c u),23      (memL1_smul_of_L1_withDensity hw (c • u)).coeFn_toLp,24      Lp.coeFn_smul c ((memL1_smul_of_L1_withDensity hw u).toLp _),25      (memL1_smul_of_L1_withDensity hw u).coeFn_toLp] with x hx h1 h2 h326    rw [h1, h2, Pi.smul_apply, h3, hx (by simpa using hw0 x), Pi.smul_apply, smul_comm]27  norm_map' := (withDensitySMulLI μ hw).norm_map2829theorem densityIsometry_coeFn (u : Lp 𝕜 1 (μ.withDensity (fun x => w x))) :30    (densityIsometry μ w hw hw0 u : Ω → 𝕜) =ᵐ[μ] (fun x => w x • u x) :=31  (memL1_smul_of_L1_withDensity hw u).coeFn_toLp3233theorem integrable_inverse_density (u : Lp 𝕜 1 μ) :34    Integrable (fun x => (w x)⁻¹ • u x) (μ.withDensity (fun x => w x)) := by35  apply (integrable_withDensity_iff_integrable_smul hw).236  simpa only [smul_smul, mul_inv_cancel₀ (hw0 _), one_smul] using L1.integrable_coeFn u3738/-- Divide by the density to recover an L1 class for the weighted measure. -/39def inverseDensity (u : Lp 𝕜 1 μ) : Lp 𝕜 1 (μ.withDensity (fun x => w x)) :=40  (integrable_inverse_density μ w hw hw0 u).toL1 _4142theorem densityIsometry_inverseDensity (u : Lp 𝕜 1 μ) :43    densityIsometry μ w hw hw0 (inverseDensity μ w hw hw0 u) = u := by44  apply Lp.ext45  apply (densityIsometry_coeFn μ w hw hw0 _).trans46  have h := (ae_withDensity_iff hw.coe_nnreal_ennreal).147    (integrable_inverse_density μ w hw hw0 u).coeFn_toL148  filter_upwards [h] with x hx49  simp only [inverseDensity]50  rw [hx (by simpa using hw0 x), smul_smul, mul_inv_cancel₀ (hw0 x), one_smul]5152/-- An everywhere positive finite measurable density gives an actual surjective L1 isometry. -/53def densityEquiv : Lp 𝕜 1 (μ.withDensity (fun x => w x)) ≃ₗᵢ[𝕜] Lp 𝕜 1 μ :=54  LinearIsometryEquiv.ofSurjective (densityIsometry μ w hw hw0)55    (fun u => ⟨inverseDensity μ w hw hw0 u, densityIsometry_inverseDensity μ w hw hw0 u⟩)5657omit hw hw05859/-- Geometric mass of component n in the probability disjoint union. -/60def componentWeight (n : ℕ) : ℝ≥0 := (2⁻¹ : ℝ≥0) ^ (n + 1)6162@[simp] theorem componentWeight_ne_zero (n : ℕ) : componentWeight n ≠ 0 := by63  simp [componentWeight]6465theorem measurable_componentWeight : Measurable componentWeight := measurable_of_countable _6667/-- The explicit geometric probability law on the natural numbers. -/68def componentMeasure : Measure ℕ := Measure.count.withDensity (fun n => componentWeight n)6970instance componentMeasure_isProbabilityMeasure : IsProbabilityMeasure componentMeasure := by71  constructor72  rw [componentMeasure, withDensity_apply _ MeasurableSet.univ, setLIntegral_univ, lintegral_count]73  simp only [componentWeight, ENNReal.coe_pow]74  rw [ENNReal.tsum_geometric_add_one]75  norm_num76  exact ENNReal.inv_mul_cancel (by norm_num) (by simp)7778/-- The actual probability measure with masses 2^(-n-1) on copies of Ω. -/79def probabilityMeasure (μ : Measure Ω) : Measure (ℕ × Ω) := componentMeasure.prod μ8081instance probabilityMeasure_isProbabilityMeasure [IsProbabilityMeasure μ] :82    IsProbabilityMeasure (probabilityMeasure μ) := by83  unfold probabilityMeasure84  infer_instance8586theorem probabilityMeasure_eq_withDensity [SFinite μ] :87    probabilityMeasure μ = (disjointMeasure μ).withDensity88      (fun z => (componentWeight z.1 : ℝ≥0∞)) := by89  exact prod_withDensity_left measurable_componentWeight.coe_nnreal_ennreal9091/-- Multiplication by the geometric component masses identifies the weighted and92counting L1 models isometrically. -/93def probabilityDisjointEquiv [SFinite μ] :94    Lp 𝕜 1 (probabilityMeasure μ) ≃ₗᵢ[𝕜] DisjointL1 (𝕜 := 𝕜) μ := by95  rw [probabilityMeasure_eq_withDensity μ]96  exact densityEquiv (disjointMeasure μ) (fun z => componentWeight z.1)97    (measurable_componentWeight.comp measurable_fst) (fun z => componentWeight_ne_zero z.1)9899/-- Explicit probability normalization of the ell1 sum. -/100def sumProbabilityEquiv [SFinite μ] :101    SumSpace (𝕜 := 𝕜) μ ≃ₗᵢ[𝕜] Lp 𝕜 1 (probabilityMeasure μ) :=102  (sumDisjointEquiv μ).trans (probabilityDisjointEquiv μ).symm103104/-- The probability model used for transport of the actual Walsh projection. -/105def walshSumProbabilityEquiv : L1Sum (Lp 𝕜 1 Walsh.haar) ≃ₗᵢ[𝕜]106    Lp 𝕜 1 (probabilityMeasure Walsh.haar) :=107  sumProbabilityEquiv Walsh.haar108109end PL1.IntervalModel110111112113114115