LinearNormalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Construction of exact normalizers for positive definite Gram operators

theorem OAI.RegularPointCoordinates.exists_exact_operator_normalization line 18

Source documentation

A positive definite symmetric operator admits an exact congruence normalization. The proof constructs it in an orthonormal eigenbasis.

theorem exists_exact_operator_normalization (Q : E →L[ℝ] E)
    (hQ : Q.IsSymmetric) (hpos : ∀ v : E, v ≠ 0 → 0 < ⟪v, Q v⟫_ℝ) :
    ∃ A : E ≃L[ℝ] E,
      (A : E →L[ℝ] E).adjoint.comp (Q.comp (A : E →L[ℝ] E)) =
        ContinuousLinearMap.id ℝ E := by
…

theorem OAI.RegularPointCoordinates.exists_exact_mean_normalization line 91
Source documentation
Positive definiteness of the actual mean energy suffices to construct the exact normalizer; the normalizer itself need not be assumed.
```
theorem exists_exact_mean_normalization (s : Set X) (hs : MeasurableSet s)
    (hpos : ∀ v : E, v ≠ 0 → 0 < ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ) :
    ∃ A : E ≃L[ℝ] E, IsExactMeanNormalization μ hQ U s hs A := by
…
```
Mentions: OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.IsExactMeanNormalization