OAI/Geometry/RCD/Coordinates/RegularRebasedRadialData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_rebased_radial_data line 20

   Source documentation

   Both value and gradient estimates transfer together to the common commutator ball. The added affine constant is the actual coordinate displacement paired with the transported coefficient.

   theorem regular_rebased_radial_data {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 κ B J C A Cχ enlargement zeta eta)
       (hfirst : first ∈ ball base (e.heat.radius / 32))
       (hcenter : center ∈ ball base (e.heat.radius / 32))
       (d1 : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca first)
       (d2 : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca center)
       (hκ : 0 ≤ κ) (hB : 0 ≤ B) (hJ : 0 ≤ J) (hCχ : 0 ≤ Cχ) (hzeta : 0 ≤ zeta)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * (2 : ℝ) ^ n) * zeta) ≤ 1 / 3)
   …

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