HilbertConvexTails.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Deterministic convex extraction in a Hilbert space. Nested closed convex tail hulls have a common point, and finite convex combinations of the original tails converge to that point.

lemma OAI.SLEExactGauge.nested_closed_convex_intersection line 21

theorem OAI.SLEExactGauge.exists_convex_tail_combinations line 68

Source documentation

The combinations use indices n+i, so every term is in the n-th original tail. No weak-convergence or separability hypothesis is needed.

theorem exists_convex_tail_combinations (u : ℕ → E)
    (B : ℝ) (hB : ∀ n, ‖u n‖ ≤ B) :
    ∃ x : E, ∃ s : ℕ → Finset ℕ, ∃ w : ℕ → ℕ → ℝ,
      (∀ n i, i ∈ s n → 0 ≤ w n i) ∧
      (∀ n, ∑ i ∈ s n, w n i = 1) ∧
      (∀ n, dist (∑ i ∈ s n, w n i • u (n+i)) x < (1/2:ℝ)^n) ∧
      Tendsto (fun n => ∑ i ∈ s n, w n i • u (n+i)) atTop (𝓝 x) := by
…