GramNormalization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact mean normalizations and their metric consequences

An exact normalization is the identity for the mean Sobolev Gram operator, as in Huang--Huang, Theorem 4.1(2). All conclusions below are derived from that identity. In particular, nondegeneracy of the original Gram operator is not separately assumed.

def OAI.RegularPointCoordinates.IsExactMeanNormalization line 28
Source documentation
The adjoint of a coordinate normalization acts on the coefficients of the scalar Sobolev column.
```
def IsExactMeanNormalization (s : Set X) (hs : MeasurableSet s)
    (A : E ≃L[ℝ] E) : Prop :=
…
```
theorem OAI.RegularPointCoordinates.meanGram_energy_of_exact_normalization line 33
theorem OAI.RegularPointCoordinates.meanGram_strictly_positive_of_exact_normalization line 42
theorem OAI.RegularPointCoordinates.meanGram_lower_of_exact_normalization line 50
theorem OAI.RegularPointCoordinates.meanGram_upper_of_exact_normalization line 63

theorem OAI.RegularPointCoordinates.meanGram_comparison_of_normalizations line 76

Source documentation

The precise comparison needed for neighboring centers or scales.

theorem meanGram_comparison_of_normalizations
    (s t : Set X) (hs : MeasurableSet s) (ht : MeasurableSet t)
    (A B : E ≃L[ℝ] E)
    (hA : IsExactMeanNormalization μ hQ U s hs A)
    (hB : IsExactMeanNormalization μ hQ U t ht B)
    {C : ℝ} (hC : 0 ≤ C)
    (hcompare : ∀ v, ‖B.symm v‖ ≤ C * ‖A.symm v‖) (v : E) :
    ⟪v, sobolevMeanGram μ hQ U t ht v⟫_ℝ ≤
      C ^ 2 * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevMeanGram