OAI/Geometry/RCD/Coordinates/RegularPairMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_pair_mass_from_estimates line 18

   Source documentation

   The two estimates already proved for the actual replacements control an actual direction of the original heat measure, including singular mass.

   theorem regular_pair_mass_from_estimates {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       (hhessian : LocalPoissonHessianInput hX) (hcutoff : LocalGoodCutoffInput hX) (hn : 2 ≤ n) :
       ∃ Ccut : ℝ, 1 ≤ Ccut ∧
       ∀ {base first center : X} {a B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
         {ker : ℝ → X → X → ℝ}
         {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
         (e : RegularProjectionEnvironment hX base hk a |K| B J C A Cχ enlargement zeta eta)
         (_hcenter : center ∈ ball base (e.heat.radius / 32))
         (d1 : RegularCenterRadialData hX e.heat |K| B J C A Cχ eta Cg D Ca first)
         (d2 : RegularCenterRadialData hX e.heat |K| B J C A Cχ eta Cg D Ca center),
       0 ≤ A → 0 ≤ Cχ → 0 ≤ zeta → zeta ≤ 1 →
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalGoodCutoffInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.RegularCenterRadialData