ExactNormalizationComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Relative comparison from exact harmonic normalization

Restricting a normalized splitting map to a subball costs only its volume ratio. The comparison is relative to the original mean Gram, even if that Gram has arbitrarily small eigenvalues.

theorem OAI.RegularPointCoordinates.exact_mean_inverse_norm_sq line 26
Source documentation
Exact mean normalization identifies the inverse-coordinate norm with the original mean energy, even for a very anisotropic Gram.
```
theorem exact_mean_inverse_norm_sq {n : ℕ}
    (U : Euclidean n →L[ℝ] SobolevSpace μ hQ)
    (s : Set X) (hs : MeasurableSet s) (A : Euclidean n ≃L[ℝ] Euclidean n)
    (hA : IsExactMeanNormalization μ hQ U s hs A) (v : Euclidean n) :
    ‖A.symm v‖ ^ 2 = ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevMeanGram

theorem OAI.RegularPointCoordinates.exact_normalization_subball_bounds line 42

Source documentation

Exact normalization on the large ball improves the two-mean comparison: only the restricted mean incurs an error.

theorem exact_normalization_subball_bounds {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (A : Euclidean n ≃L[ℝ] Euclidean n)
    {p : X} {r ε C : ℝ} {w : X → Euclidean n}
    (hfirst : FirstOrderSplittingOn μ hQ p r ε (transformedColumn μ hQ u A) w)
    (hexact : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
      (ball p r) measurableSet_ball A)
    (s : Set X) (hs : MeasurableSet s) (hsub : s ⊆ ball p r)
    (hszero : μ s ≠ 0) (hsfin : μ s ≠ ∞)
    (hrzero : μ (ball p r) ≠ 0) (hrfin : μ (ball p r) ≠ ∞)
    (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hvol : μ.real (ball p r) ≤ C * μ.real s) (v : Euclidean n) :
    (1 - (n : ℝ) ^ 2 * (C * ε)) *
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap