RegularFrozenMetrics.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Frozen frames constructed from the actual heat metrics

theorem OAI.RegularPointCoordinates.RegularBilinearData.heatAt_decrement_positive line 24

Source documentation

The original heat decrement is positive as an operator.

theorem heatAt_decrement_positive {q : X} (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (hi : d.shift ≤ i) :
    ((d.heatAt q i).toContinuousLinearMap -
      (d.heatAt q (i + 1)).toContinuousLinearMap).IsPositive := by
…

theorem OAI.RegularPointCoordinates.RegularBilinearData.heatAt_two_step_decrement_positive line 36

Source documentation

The sum of two consecutive positive heat decrements.

theorem heatAt_two_step_decrement_positive {q : X} (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (hi : d.shift ≤ i) :
    ((d.heatAt q i).toContinuousLinearMap -
      (d.heatAt q (i + 2)).toContinuousLinearMap).IsPositive := by
…

theorem OAI.RegularPointCoordinates.RegularBilinearData.heatAt_two_step_bound line 51

Source documentation

Two successive 9/8 bounds still give a half-small total decrement.

theorem heatAt_two_step_bound {q : X} (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (hi : d.shift ≤ i) (v : Euclidean n) :
    ⟪v, d.heatAt q i v⟫_ℝ ≤ 2 * ⟪v, d.heatAt q (i + 2) v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.RegularBilinearData.heatAt_two_step_inverse_error line 64
Source documentation
The two-scale inverse error costs only the corresponding inverse-energy increment.
```
theorem heatAt_two_step_inverse_error {q : X} (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (hi : d.shift ≤ i) (xi : Euclidean n) :
    let delta := (d.heatAt q (i + 2)).symm xi - (d.heatAt q i).symm xi
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
def OAI.RegularPointCoordinates.RegularBilinearData.frozenAt line 74
Source documentation
Freeze at the heat scale two dyadic steps below the pinching mean radius.
```
def frozenAt (q : X) (i : ℕ) : Euclidean n ≃L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.RegularBilinearData.frozenAt_norm_sq line 78
theorem OAI.RegularPointCoordinates.RegularBilinearData.frozenAt_mono line 83
Source documentation
The actual heat monotonicity gives monotone frozen norms at every center.
```
theorem frozenAt_mono {q : X} (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (v : Euclidean n) :
    ‖d.frozenAt q i v‖ ≤ ‖d.frozenAt q (i + 1) v‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.RegularBilinearData.frozenAt_step line 93
Source documentation
A single dyadic step changes the frozen norm by at most two.
```
theorem frozenAt_step {q : X} (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (v : Euclidean n) :
    ‖d.frozenAt q (i + 1) v‖ ≤ 2 * ‖d.frozenAt q i v‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean