FiniteMomentConvergence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Passing finite affine fits through convergence of actual L² moments

Only the finitely many pairings of the target, constant and coordinate functions are needed. The spaces containing them may vary with the index. This is the algebraic step following local strong L² compactness.

theorem OAI.RegularPointCoordinates.norm_sum_smul_sq line 24

Source documentation

The squared norm of a finite linear combination uses precisely its finite Gram matrix.

theorem norm_sum_smul_sq {H : Type*} [NormedAddCommGroup H]
    [InnerProductSpace ℝ H] (f : ι → H) (a : ι → ℝ) :
    ‖∑ i, a i • f i‖ ^ 2 = ∑ i, ∑ j, a i * a j * ⟪f i, f j⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.norm_sum_smul_tendsto_of_inner_tendsto line 38

Source documentation

Joint local L² convergence implies convergence of every fixed affine fit error, without choosing minimizers or identifying the varying spaces.

theorem norm_sum_smul_tendsto_of_inner_tendsto
    {H : ℕ → Type*} [∀ k, NormedAddCommGroup (H k)]
    [∀ k, InnerProductSpace ℝ (H k)]
    {Hlim : Type*} [NormedAddCommGroup Hlim] [InnerProductSpace ℝ Hlim]
    (f : ∀ k, ι → H k) (flim : ι → Hlim)
    (h : ∀ i j, Tendsto (fun k => ⟪f k i, f k j⟫_ℝ) atTop (𝓝 ⟪flim i, flim j⟫_ℝ))
    (a : ι → ℝ) :
    Tendsto (fun k => ‖∑ i, a i • f k i‖) atTop (𝓝 ‖∑ i, a i • flim i‖) := by
…

theorem OAI.RegularPointCoordinates.eventually_norm_sum_smul_lt line 61

Source documentation

A strict bound on one Euclidean candidate is inherited by the actual finite linear combinations for all sufficiently late indices.

theorem eventually_norm_sum_smul_lt
    {H : ℕ → Type*} [∀ k, NormedAddCommGroup (H k)]
    [∀ k, InnerProductSpace ℝ (H k)]
    {Hlim : Type*} [NormedAddCommGroup Hlim] [InnerProductSpace ℝ Hlim]
    (f : ∀ k, ι → H k) (flim : ι → Hlim)
    (h : ∀ i j, Tendsto (fun k => ⟪f k i, f k j⟫_ℝ) atTop (𝓝 ⟪flim i, flim j⟫_ℝ))
    (a : ι → ℝ) {η : ℝ} (hη : ‖∑ i, a i • flim i‖ < η) :
    ∀ᶠ k in atTop, ‖∑ i, a i • f k i‖ < η :=
…