OAI/Geometry/RCD/Coordinates/RegularCutoffDerivatives.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_cutoff_directional_bounds line 18

   Source documentation

   The one fixed Gevrey base controls both derivative orders needed by the metric update. The source radius is the actual pinching scale.

   theorem regular_cutoff_directional_bounds {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)
       (hzeta0 : 0 ≤ zeta) (hzeta : zeta ≤ 1 / 64)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 2 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
       (psi : EuclideanGevreyCutoff n) (i : ℕ)
       {q y : X} (hq : q ∈ e.heat.patchRegion) (hy : y ∈ e.heat.patchNet i)
       (hactive : e.heat.values q ∈ tsupport (e.heat.patchCutoff psi.value i y))
       (xi : Euclidean n) :
   …

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