OAI/Geometry/RCD/Coordinates/RegularShiftedNormalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_shifted_inverse_error line 17

   Source documentation

   Changing from the patch mean to a heat scale two steps finer costs a mean-normalization error and a telescoping heat increment.

   theorem regular_shifted_inverse_error {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {base : X} {a κ B J C A Cχ enlargement zeta eta : ℝ}
       {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)
       {q z : X} (hq : q ∈ ball base (e.heat.radius / 32))
       (hz : z ∈ ball base (e.heat.radius / 32)) (hzeta : 0 ≤ zeta)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 2 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
       (i : ℕ) (hi : e.heat.shift ≤ i + 15)
       (hroom : dist z q ≤ e.heat.radius / (2 : ℝ) ^ (i + 15))
       (henlargement : dist q z ≤ enlargement * (e.heat.radius / (2 : ℝ) ^ (i + 15)))
   …

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