OAI/Analysis/FiniteFactor/L2UniformAbsoluteContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.withDensity_L2_set_le line 13

   Source documentation

   Cauchy--Schwarz bounds the mass of any Borel set under an actual L2 density, in terms of the original reference measure of the set.

   theorem withDensity_L2_set_le {X : Type*} [MeasurableSpace X]
       (μ : Measure X) [IsFiniteMeasure μ] (g : X → ℝ)
       (hg : MemLp g 2 μ) (hg0 : ∀ x, 0 ≤ g x)
       (A : Set X) (hA : MeasurableSet A) (C : ℝ) (hC : (∫ x, g x ^ 2 ∂μ) ≤ C) :
       (μ.withDensity (fun x => ENNReal.ofReal (g x))) A ≤
         ENNReal.ofReal (Real.sqrt C * Real.sqrt ((μ A).toReal)) := by
   …

2. theorem OAI.FiniteFactor.uniformAC_of_L2_densities line 44

   Source documentation

   Uniform L2 density bounds imply uniform absolute continuity, with no measurable-selection premise for the densities.

   theorem uniformAC_of_L2_densities {X : Type*} [MeasurableSpace X]
       (μ : Measure X) [IsFiniteMeasure μ] (ν : ℕ → Measure X) (C : ℝ)
       (hν : ∀ n, ∃ g : X → ℝ, MemLp g 2 μ ∧ (∀ x, 0 ≤ g x) ∧
         ν n = μ.withDensity (fun x => ENNReal.ofReal (g x)) ∧ (∫ x, g x^2 ∂μ) ≤ C)
       (ε : ℝ≥0) (hε : 0 < ε) :
       ∃ δ : ℝ≥0∞, 0 < δ ∧ ∀ A, MeasurableSet A → μ A < δ → ∀ n, ν n A ≤ ε := by
   …