RegularHeatNormalization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Changing actual mean frames in the cumulative heat estimates

def OAI.RegularPointCoordinates.RegularBilinearData.heatAt line 25
Source documentation
The same positive heat Gram used in the neighborhood construction.
```
def heatAt (q : X) (i : ℕ) : Euclidean n ≃L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.RegularBilinearData.heatAt_isPositive line 30

theorem OAI.RegularPointCoordinates.regular_nearby_mean_heat_lower line 37

Source documentation

A nearby mean dominates one quarter of the central heat metric. Both means are compared inside a single larger normalized ball.

theorem regular_nearby_mean_heat_lower {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 + 1)
    (hroom : dist z q ≤ e.heat.radius / (2 : ℝ) ^ (i + 1)) (v : Euclidean n) :
    (1 / 4 : ℝ) * ⟪v, e.heat.heatAt q (i + 1) v⟫_ℝ ≤
…

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

theorem OAI.RegularPointCoordinates.regular_inverse_mean_heat_error line 77

Source documentation

The actual inverse-frame discrepancy has the weighted envelope bound needed for summing over patch centers.

theorem regular_inverse_mean_heat_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 + 1)
    (hroom : dist z q ≤ e.heat.radius / (2 : ℝ) ^ (i + 1))
    (henlargement : dist q z ≤ enlargement * (e.heat.radius / (2 : ℝ) ^ (i + 1)))
…