LocalAffineMoments.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Normalized local L² moments of the actual Sobolev affine family

def OAI.RegularPointCoordinates.normalizeLocalL2 line 19
Source documentation
Scaling by the norm of the constant function is the normalized local L² convention; the zero-measure case uses the usual inverse-zero convention.
```
def normalizeLocalL2 (s : Set X) (hfin : μ s ≠ ∞)
    (f : Lp ℝ 2 (μ.restrict s)) : Lp ℝ 2 (μ.restrict s) :=
…
```
theorem OAI.RegularPointCoordinates.restrictedOne_norm line 24
def OAI.RegularPointCoordinates.localAffineMomentFamily line 34
Source documentation
Target, constant and coordinates with the same normalized local L² scale.
```
def localAffineMomentFamily {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (w : SobolevSpace μ hQ) (s : Set X) (hfin : μ s ≠ ∞) :
    Option (Option (Fin n)) → Lp ℝ 2 (μ.restrict s) :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.localAffineMomentFamily_sum line 44
Source documentation
The finite moment expression is exactly the normalized error of the actual Sobolev affine candidate, including its constant term.
```
theorem localAffineMomentFamily_sum {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (w : SobolevSpace μ hQ) (s : Set X) (hfin : μ s ≠ ∞)
    (c : ℝ) (v : Euclidean n) :
    (∑ i, affineErrorCoefficients c (fun j => v j) i •
      localAffineMomentFamily μ hQ u w s hfin i) =
      normalizeLocalL2 μ s hfin
        (SobolevSpace.restrictLp μ hQ s w - affineCoordinateMap μ hQ u s hfin (c, v)) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineErrorCoefficients, OAI.RegularPointCoordinates.localAffineMomentFamily, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.affineCoordinateMap
theorem OAI.RegularPointCoordinates.normalized_affineResidual_le line 59
Source documentation
The least-squares projection has no greater normalized error than any of the affine candidates whose joint moments are controlled.
```
theorem normalized_affineResidual_le {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (w : SobolevSpace μ hQ) (s : Set X) (hfin : μ s ≠ ∞) (c : ℝ) (v : Euclidean n) :
    ‖normalizeLocalL2 μ s hfin
      (affineResidual μ hQ u s hfin (SobolevSpace.restrictLp μ hQ s w))‖ ≤
        ‖∑ i, affineErrorCoefficients c (fun j => v j) i •
          localAffineMomentFamily μ hQ u w s hfin i‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.affineResidual, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.affineErrorCoefficients, OAI.RegularPointCoordinates.localAffineMomentFamily

theorem OAI.RegularPointCoordinates.eventually_normalized_affineResidual_lt line 72

Source documentation

Passing the finite moments to a model controls the actual normalized least-squares residual, not just a separately chosen trial function.

theorem eventually_normalized_affineResidual_lt {n : ℕ}
    (u : ℕ → Fin n → SobolevSpace μ hQ) (w : ℕ → SobolevSpace μ hQ)
    (s : ℕ → Set X) (hfin : ∀ k, μ (s k) ≠ ∞)
    {Hlim : Type*} [NormedAddCommGroup Hlim] [InnerProductSpace ℝ Hlim]
    (model : Option (Option (Fin n)) → Hlim)
    (hconv : ∀ i j, Tendsto
      (fun k => ⟪localAffineMomentFamily μ hQ (u k) (w k) (s k) (hfin k) i,
        localAffineMomentFamily μ hQ (u k) (w k) (s k) (hfin k) j⟫_ℝ) atTop
      (𝓝 ⟪model i, model j⟫_ℝ))
    (c : ℝ) (v : Euclidean n) {η : ℝ}
    (hmodel : ‖∑ i, affineErrorCoefficients c (fun j => v j) i • model i‖ < η) :
    ∀ᶠ k in atTop,
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localAffineMomentFamily, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineErrorCoefficients