RegularHeatFrameGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Coordinate separation measured in the actual frozen heat frames

theorem OAI.RegularPointCoordinates.RegularBilinearData.coordinateFrame_norm_sq line 23
Source documentation
An exact coordinate frame realizes the quadratic inverse mean.
```
theorem coordinateFrame_norm_sq (q : X) (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (v : Euclidean n) :
    ‖coordinateFrame (d.frameAt q hq i) v‖ ^ 2 = ⟪v, (d.meanAt q hq i).symm v⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.coordinateFrame

theorem OAI.RegularPointCoordinates.RegularBilinearData.mean_heat_frame_comparison line 37

Source documentation

Heat and mean frames at the same radius are uniformly comparable.

theorem mean_heat_frame_comparison (q : X) (hq : q ∈ ball base (d.radius / 32))
    (i : ℕ) (hi : d.shift ≤ i) (v : Euclidean n) :
    ‖coordinateFrame (d.frameAt q hq i) v‖ ≤
        (3 / 2 : ℝ) * ‖inverseMetricFrame (d.heatAt q i) (d.heatAt_isPositive q i) v‖ ∧
    ‖inverseMetricFrame (d.heatAt q i) (d.heatAt_isPositive q i) v‖ ≤
        (3 / 2 : ℝ) * ‖coordinateFrame (d.frameAt q hq i) v‖ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.coordinateFrame, OAI.RegularPointCoordinates.inverseMetricFrame

theorem OAI.RegularPointCoordinates.RegularBilinearData.heat_frame_mono_indices line 65

Source documentation

Monotonicity holds between any two sufficiently late heat scales.

theorem heat_frame_mono_indices {q : X} (hq : q ∈ ball base (d.radius / 32))
    {i j : ℕ} (hi : d.shift ≤ i) (hij : i ≤ j) (v : Euclidean n) :
    ‖inverseMetricFrame (d.heatAt q i) (d.heatAt_isPositive q i) v‖ ≤
      ‖inverseMetricFrame (d.heatAt q j) (d.heatAt_isPositive q j) v‖ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.inverseMetricFrame

theorem OAI.RegularPointCoordinates.RegularBilinearData.coarse_frame_le_frozen line 81
Source documentation
A coarser exact harmonic frame is bounded by the actual fine frozen heat frame. This supplies the global separation bound for patch supports.
```
theorem coarse_frame_le_frozen {q : X} (hq : q ∈ ball base (d.radius / 32))
    (i j : ℕ) (hj : d.shift ≤ j) (hji : j ≤ d.shift + i + 17) (v : Euclidean n) :
    ‖coordinateFrame (d.frameAt q hq j) v‖ ≤ 2 * ‖d.frozenAt q i v‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.coordinateFrame