OAI/Geometry/RCD/Sobolev/LocalHolderMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.square_integral_le_higher_moment line 17

   Source documentation

   On a finite measure space, a superquadratic moment controls L² with the exact measure power used in the level-set iteration.

   theorem square_integral_le_higher_moment [IsFiniteMeasure μ]
       {f : X → ℝ} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 2 < p)
       (hi : Integrable (fun x => |f x|^p) μ) :
       (∫ x, (f x)^2 ∂μ) ≤ (∫ x, |f x|^p ∂μ)^(2/p)*
         (μ.real univ)^(1-2/p) := by
   …

2. theorem OAI.RegularPointCoordinates.square_setIntegral_le_higher_moment line 51

   Source documentation

   Restricting the L² integral to a level set inserts a positive power of its measure while retaining the moment on the outer domain.

   theorem square_setIntegral_le_higher_moment {Ω A : Set X}
       (_hΩ : MeasurableSet Ω) (_hA : MeasurableSet A) (hAΩ : A ⊆ Ω)
       (hfin : μ Ω < ∞) {f : X → ℝ} (hf : AEStronglyMeasurable f (μ.restrict Ω))
       {p : ℝ} (hp : 2 < p) (hi : IntegrableOn (fun x => |f x|^p) Ω μ) :
       (∫ x in A, (f x)^2 ∂μ) ≤ (∫ x in Ω, |f x|^p ∂μ)^(2/p)*
         (μ.real A)^(1-2/p) := by
   …