OAI/Geometry/RCD/Sobolev/GeometricMeanBootstrap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.geometric_mean_bootstrap line 14

   Source documentation

   Iterating an interior estimate with a summable loss removes the initial upper bound. This is the scalar step from L² to L¹ mean bounds.

   theorem geometric_mean_bootstrap {X : Type*} [MeasurableSpace X] (μ : Measure X)
       (u : X → ℝ) (Ω : Set X) (S : ℕ → Set X) (hS : ∀ i, S i ⊆ Ω)
       {θ b D H B : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ < 1)
       (hD : 0 ≤ D) (hH : 0 ≤ H) (hB : 0 ≤ B)
       (hbalance : θ*b^2 = 1/2)
       (hbound : ∀ᵐ x ∂μ.restrict Ω, u x ≤ B)
       (hstep : ∀ i C, 0 ≤ C →
         (∀ᵐ x ∂μ.restrict (S (i+1)), u x ≤ C) →
         ∀ᵐ x ∂μ.restrict (S i), u x ≤ θ*C+D*(b^2)^i*H) :
       ∀ᵐ x ∂μ.restrict (S 0), u x ≤ 2*D*H := by
   …