OAI/Geometry/RCD/Metric/ScaledCentralMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_scaled_central_mass_comparison line 18

   Source documentation

   The central cumulative constant is fixed before selecting any neighborhood realizing the construction parameters.

   theorem exists_scaled_central_mass_comparison {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {base : X} {ker : ℝ → X → X → ℝ}
       (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
       (c : RegularHeatConstants n) :
       ∃ T : ℝ, 0 < T ∧ ∀ {enlargement zeta : ℝ}
         (d : RegularBilinearData hX base hk enlargement zeta), c.Matches d →
         ∀ q, q ∈ ball base (d.radius / 32) → ∀ (xi : Euclidean n) (k : ℕ),
         let Q := fun i => d.heatAt q (d.shift + i + 17)
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularHeatConstants, OAI.RegularPointCoordinates.RegularBilinearData, OAI.RegularPointCoordinates.Euclidean