RegularCutoffJets.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform Gevrey jets of the actual heat-coordinate cutoffs

theorem OAI.RegularPointCoordinates.regular_active_patch_distance line 19

Source documentation

The support localization places its net center within the radius where the frozen heat frames can be compared.

theorem regular_active_patch_distance {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)
    (hzeta : zeta ≤ 1 / 64) (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)) :
    dist y q ≤ e.heat.radius / 2 ^ (e.heat.shift + i + 17) := by
…

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

theorem OAI.RegularPointCoordinates.regular_cutoff_normalized_jet line 44

Source documentation

The affine input of the actual cutoff has uniformly bounded norm after normalization at the testing point. The scale ratio is exactly 2^27; the numerical bound also absorbs the nearby-frame comparison.

theorem regular_cutoff_normalized_jet {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)) (m : ℕ) :
    ‖iteratedFDeriv ℝ m (fun z => e.heat.patchCutoff psi.value i y
…