CenteredNormalization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact harmonic normalization survives centering

theorem OAI.RegularPointCoordinates.centeredColumn_meanGram line 19
Source documentation
Centering has zero local gradient in every covector, so it preserves the complete actual mean Gram operator on the region.
```
theorem centeredColumn_meanGram {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (Ω : Set X) (hΩ : MeasurableSet Ω) (c : Euclidean n) (eta : SobolevSpace μ hQ)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ)) :
    sobolevMeanGram μ hQ (sobolevColumnMap μ hQ (centeredColumn μ hQ u c eta)) Ω hΩ =
      sobolevMeanGram μ hQ (sobolevColumnMap μ hQ u) Ω hΩ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.centeredColumn

theorem OAI.RegularPointCoordinates.IsExactMeanNormalization.center line 43

Source documentation

The exact same frame normalizes both the original and centered coordinate columns; no new normalizing matrix is chosen.

theorem IsExactMeanNormalization.center {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (Ω : Set X) (hΩ : MeasurableSet Ω) (c : Euclidean n) (eta : SobolevSpace μ hQ)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (N : Euclidean n ≃L[ℝ] Euclidean n)
    (hN : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u) Ω hΩ N) :
    IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ (centeredColumn μ hQ u c eta)) Ω hΩ N := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.centeredColumn

theorem OAI.RegularPointCoordinates.sobolevMeanGram_eq_of_local_representatives line 56
Source documentation
Globally clipped coordinate extensions retain the same local mean Gram whenever their representatives agree on the region.
```
theorem sobolevMeanGram_eq_of_local_representatives {n : ℕ}
    (u v : Fin n → SobolevSpace μ hQ) (Ω : Set X) (hΩ : MeasurableSet Ω)
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ (v j)) :
    sobolevMeanGram μ hQ (sobolevColumnMap μ hQ u) Ω hΩ =
      sobolevMeanGram μ hQ (sobolevColumnMap μ hQ v) Ω hΩ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.sobolevColumnMap