OAI/Geometry/RCD/Harmonic/WeightedDirectionalVanishing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.tendstoUniformly_of_directional_bound line 15

   Source documentation

   The dominating mass and the directional bound stay fixed as the weighted directional energy tends uniformly to zero.

   theorem tendstoUniformly_of_directional_bound {Y : Type*} {A E : ℕ → Y → ℝ}
       {C M : ℝ} (hC : 0≤C) (hM : 0≤M)
       (hA : ∀ k y, 0≤A k y)
       (hE : TendstoUniformly E (fun _ => 0) atTop)
       (hb : ∀ k y r, 0<r → 4*r*A k y ≤ 4*r^2*C+M*E k y) :
       TendstoUniformly A (fun _ => 0) atTop := by
   …