OAI/Geometry/RCD/Sobolev/GeometricTailMoment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.geometric_tail_moment line 19

   Source documentation

   Geometrically decaying level measures yield a strong moment whenever the decay exceeds the growth of the moment on successive levels.

   theorem geometric_tail_moment (μ : Measure X) [IsFiniteMeasure μ]
       {f : X → ℝ} (hf : Measurable f) (hf0 : ∀ x, 0 ≤ f x)
       {S B A q p : ℝ} (hS : 0 < S) (hB : 1 < B) (hA : 0 ≤ A) (hq : 0 ≤ q)
       (hp : 0 < p) (hdecay : B^p*q < 1)
       (htail : ∀ k : ℕ, μ.real {x | S*B^k < f x} ≤ A*q^k) :
       Integrable (fun x => f x ^ p) μ ∧
         (∫ x, f x ^ p ∂μ) ≤ (S*B)^p * μ.real univ +
           A*(S*B^2)^p / (1-B^p*q) := by
   …