RegularNearbyFrozen.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Comparing actual frozen frames at nearby centers

theorem OAI.RegularPointCoordinates.regular_nearby_frozen_bound line 18

Source documentation

The existing subball Gram estimate compares the two actual heat frames. No continuity estimate for an arbitrarily chosen normalizer is assumed.

theorem regular_nearby_frozen_bound {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 : ℕ) (hroom : dist z q ≤ e.heat.radius / 2 ^ (e.heat.shift + i + 17))
    (v : Euclidean n) :
    ‖e.heat.frozenAt z i v‖ ≤ 3 * ‖e.heat.frozenAt q i v‖ := by
…

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

theorem OAI.RegularPointCoordinates.regular_nearby_frozen_operator line 57

Source documentation

Operator-norm form of the same comparison.

theorem regular_nearby_frozen_operator {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 : ℕ) (hroom : dist z q ≤ e.heat.radius / 2 ^ (e.heat.shift + i + 17)) :
    ‖(e.heat.frozenAt z i).toContinuousLinearMap.comp
      (e.heat.frozenAt q i).symm.toContinuousLinearMap‖ ≤ 3 := by
…