OAI/Geometry/RCD/Coordinates/RegularLinearRadialData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_linear_radial_data line 21

   Source documentation

   Linear assembly keeps the same radial representatives and coefficients in both the value and gradient bounds. It also gives the near-identity bound for the covector operator used in the two-center commutator.

   theorem regular_linear_radial_data {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {p q : X} {ker : ℝ → X → X → ℝ}
       {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
       {a κ B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
       (e : RegularProjectionEnvironment hX p hk a κ B J C A Cχ enlargement zeta eta)
       (hq : q ∈ ball p (e.heat.radius / 32))
       (d : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca q)
       (hκ : 0 ≤ κ) (hB : 0 ≤ B) (hCχ : 0 ≤ Cχ) (hzeta : 0 ≤ zeta) (i : ℕ) :
       let μ := hausdorff n X
   …

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