InverseMetricFrames.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact Euclidean frames for the inverse heat metrics

theorem OAI.RegularPointCoordinates.positive_equiv_strict line 18

Source documentation

An invertible positive form is strictly positive on nonzero vectors.

theorem positive_equiv_strict (Q : E ≃L[ℝ] E)
    (hQ : Q.toContinuousLinearMap.IsPositive) {v : E} (hv : v ≠ 0) :
    0 < ⟪v, Q v⟫_ℝ := by
…

def OAI.RegularPointCoordinates.inverseMetricFrame line 32
Source documentation
A finite-dimensional inverse metric represented by an actual linear frame.
```
def inverseMetricFrame (Q : E ≃L[ℝ] E)
    (hQ : Q.toContinuousLinearMap.IsPositive) : E ≃L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.inverseMetricFrame_norm_sq line 38

theorem OAI.RegularPointCoordinates.inverseMetricFrame_mono line 55

Source documentation

Decreasing positive forms have increasing inverse-frame norms.

theorem inverseMetricFrame_mono (P Q : E ≃L[ℝ] E)
    (hP : P.toContinuousLinearMap.IsPositive) (hQ : Q.toContinuousLinearMap.IsPositive)
    (hD : (P.toContinuousLinearMap - Q.toContinuousLinearMap).IsPositive) (v : E) :
    ‖inverseMetricFrame P hP v‖ ≤ ‖inverseMetricFrame Q hQ v‖ := by
…

Mentions: OAI.RegularPointCoordinates.inverseMetricFrame

theorem OAI.RegularPointCoordinates.inverseMetricFrame_step line 66

Source documentation

Slow heat decay gives a uniform comparison of successive frozen frames.

theorem inverseMetricFrame_step (P Q : E ≃L[ℝ] E)
    (hP : P.toContinuousLinearMap.IsPositive) (hQ : Q.toContinuousLinearMap.IsPositive)
    (hstep : ∀ v, ⟪v, P v⟫_ℝ ≤ (9 / 8 : ℝ) * ⟪v, Q v⟫_ℝ) (v : E) :
    ‖inverseMetricFrame Q hQ v‖ ≤ 2 * ‖inverseMetricFrame P hP v‖ := by
…

Mentions: OAI.RegularPointCoordinates.inverseMetricFrame

theorem OAI.RegularPointCoordinates.inverse_difference_energy_le line 81

Source documentation

A relative half-small decrement controls the inverse discrepancy in both endpoint metrics, including the finer metric used by patch assembly.

theorem inverse_difference_energy_le (P Q : E ≃L[ℝ] E)
    (hP : P.toContinuousLinearMap.IsPositive) (hQ : Q.toContinuousLinearMap.IsPositive)
    (hD : (P.toContinuousLinearMap - Q.toContinuousLinearMap).IsPositive)
    (hstep : ∀ v, ⟪v, P v⟫_ℝ ≤ 2 * ⟪v, Q v⟫_ℝ) (xi : E) :
    let d := Q.symm xi - P.symm xi
…