AffineCompactness.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The compactness contradiction for a uniform affine improvement

Convergence of the joint L² moments transfers a strict Euclidean affine improvement to the approximating harmonic functions.

def OAI.RegularPointCoordinates.affineMomentFamily line 19

Source documentation

Target, constant and coordinate functions, in that order.

def affineMomentFamily {H : Type*} (n : ℕ) (f one : H) (u : Fin n → H) :
    Option (Option (Fin n)) → H
  | none => f
  | some none => one
  | some (some i) => u i

def OAI.RegularPointCoordinates.affineErrorCoefficients line 25
theorem OAI.RegularPointCoordinates.affineMomentFamily_sum line 31

theorem OAI.RegularPointCoordinates.affine_error_tendsto_of_moments line 41

Source documentation

Strict improvement for the limiting model transfers to the same coefficients in every sufficiently late actual function space.

theorem affine_error_tendsto_of_moments
    {n : ℕ} {H : ℕ → Type*} [∀ k, NormedAddCommGroup (H k)]
    [∀ k, InnerProductSpace ℝ (H k)]
    {Hlim : Type*} [NormedAddCommGroup Hlim] [InnerProductSpace ℝ Hlim]
    (f one : ∀ k, H k) (u : ∀ k, Fin n → H k)
    (flim onelim : Hlim) (ulim : Fin n → Hlim)
    (h : ∀ i j, Tendsto
      (fun k => ⟪affineMomentFamily n (f k) (one k) (u k) i,
        affineMomentFamily n (f k) (one k) (u k) j⟫_ℝ) atTop
      (𝓝 ⟪affineMomentFamily n flim onelim ulim i,
        affineMomentFamily n flim onelim ulim j⟫_ℝ))
    (c : ℝ) (v : Fin n → ℝ) :
…

Mentions: OAI.RegularPointCoordinates.affineMomentFamily

theorem OAI.RegularPointCoordinates.eventually_affine_fit_of_moment_compactness line 63

Source documentation

The uniform threshold follows by contradiction from subsequential compactness of the finite moments and the strict Euclidean candidate bound. The coefficient choices need not be bounded or continuous in the index.

theorem eventually_affine_fit_of_moment_compactness
    {n : ℕ} {H : ℕ → Type*} [∀ k, NormedAddCommGroup (H k)]
    [∀ k, InnerProductSpace ℝ (H k)]
    {Hlim : Type*} [NormedAddCommGroup Hlim] [InnerProductSpace ℝ Hlim]
    (f one : ∀ k, H k) (u : ∀ k, Fin n → H k)
    {Models : Type*} (flim onelim : Models → Hlim) (ulim : Models → Fin n → Hlim)
    (hcompact : ∀ s : ℕ → ℕ, StrictMono s →
      ∃ (t : ℕ → ℕ), StrictMono t ∧ ∃ model : Models,
        ∀ i j, Tendsto
          (fun k => ⟪affineMomentFamily n (f (s (t k))) (one (s (t k))) (u (s (t k))) i,
            affineMomentFamily n (f (s (t k))) (one (s (t k))) (u (s (t k))) j⟫_ℝ) atTop
          (𝓝 ⟪affineMomentFamily n (flim model) (onelim model) (ulim model) i,
…

Mentions: OAI.RegularPointCoordinates.affineMomentFamily