OAI/Analysis/FiniteFactor/SubmeasureL2Density.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.submeasure_L2_density line 13

   Source documentation

   A finite submeasure of an L2 density has an actual nonnegative L2 Radon--Nikodym density, with no increase in its squared integral.

   theorem submeasure_L2_density {Ω : Type*} [MeasurableSpace Ω]
       (μ ν : Measure Ω) [SigmaFinite μ] [IsFiniteMeasure ν] (f : Ω → ℝ)
       (hf : MemLp f 2 μ) (hν : ν ≤ μ.withDensity (fun x => ENNReal.ofReal (f x))) :
       ∃ g : Ω → ℝ, Measurable g ∧ (∀ x, 0 ≤ g x) ∧
         ν = μ.withDensity (fun x => ENNReal.ofReal (g x)) ∧
         (∀ᵐ x ∂μ, g x ≤ |f x|) ∧ MemLp g 2 μ ∧
         (∫ x, g x ^ 2 ∂μ) ≤ ∫ x, f x ^ 2 ∂μ := by
   …