MeanGramInverse.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.meanGram_injective_of_exact_normalization line 22
Source documentation
Exact normalization makes the original mean Gram injective.
```
theorem meanGram_injective_of_exact_normalization :
    Function.Injective (sobolevMeanGram μ hQ U Ω hΩ) := by
…
```
Mentions: OAI.RegularPointCoordinates.sobolevMeanGram
def OAI.RegularPointCoordinates.meanGramEquiv line 33
Source documentation
The mean Gram itself, with the inverse supplied by its proved nondegeneracy. This is independent of which exact normalizer witnesses it.
```
def meanGramEquiv [FiniteDimensional ℝ E] : E ≃L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.meanGramEquiv_apply line 37
theorem OAI.RegularPointCoordinates.meanGram_apply_normalizer_adjoint line 42
Source documentation
The inverse Gram direction is exactly A A* xi, without a symmetry assumption on the chosen normalizer.
```
theorem meanGram_apply_normalizer_adjoint (xi : E) :
    sobolevMeanGram μ hQ U Ω hΩ (A (A.toContinuousLinearMap.adjoint xi)) = xi := by
…
```
Mentions: OAI.RegularPointCoordinates.sobolevMeanGram
theorem OAI.RegularPointCoordinates.meanGramEquiv_symm_apply line 53