OAI/Geometry/RCD/Sobolev/LevelSetHolderStep.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.upper_level_square_integrable line 16
2. theorem OAI.RegularPointCoordinates.level_set_holder_step line 23

   Source documentation

   A higher moment on the outer domain, together with agreement of the cutoff on the inner domain, gives the superlinear level-set estimate.

   theorem level_set_holder_step {Ω B D : Set X} (hΩ : MeasurableSet Ω)
       (hB : MeasurableSet B) (hBΩ : B ⊆ Ω) (hBD : B ⊆ D) (hfin : μ Ω < ∞)
       (u z : Lp ℝ 2 μ) {k h p : ℝ} (hk : 0 ≤ k) (hkh : k < h) (hp : 2 < p)
       (hrep : z =ᵐ[μ.restrict B] fun x => max (u x-k) 0)
       (hi : IntegrableOn (fun x => |z x|^p) Ω μ) :
       (∫ x in B, (max (u x-h) 0)^2 ∂μ) ≤
         (∫ x in Ω, |z x|^p ∂μ)^(2/p)*
           ((∫ x in D, (max (u x-k) 0)^2 ∂μ)/(h-k)^2)^(1-2/p) := by
   …