OAI/Geometry/RCD/Sobolev/StampacchiaBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_extinction_level line 16

   Source documentation

   The extinction level depends only on the coefficient, exponent, and initial volume bound, not on the particular decreasing distribution.

   theorem exists_extinction_level {R M p : ℝ} (hR : 0 ≤ R) (hM : 0 < M) (hp : 2 < p) :
       ∃ K : ℝ, 0 < K ∧ ∀ Y : ℝ → ℝ,
         (∀ k, 0 ≤ k → 0 ≤ Y k) → Y 0 ≤ M →
         (∀ k l, 0 ≤ k → k ≤ l → Y l ≤ Y k) →
         (∀ k l, 0 ≤ k → k < l → Y l ≤ R * Y k ^ (p - 1) / (l - k) ^ p) →
         Y K = 0 := by
   …