OAI/Geometry/RCD/Coordinates/RegularMassScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.regularPinchingMassConstant line 15
2. theorem OAI.RegularPointCoordinates.regular_pair_mass_scaling line 25

   Source documentation

   Both terms of the actual mass estimate are controlled by the same squared source. The constant has no dependence on center or scale.

   theorem regular_pair_mass_scaling {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {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)
       {Ccut Q L sigma : ℝ} (hCcut : 0 ≤ Ccut) (hB : 0 ≤ B) (hJ : 0 ≤ J) (hCχ : 0 ≤ Cχ)
       (i : ℕ) :
       let μ := hausdorff n X
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.RegularCenterRadialData, OAI.RegularPointCoordinates.sigma