AdaptiveConvexPrefix.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite convex witnesses for adaptive anchors

Closure of a convex hull is approximated by actual finite convex combinations. For a sequence, the coefficients can be extended by zero to a whole initial segment. Removing zero coefficients then preserves their original order.

theorem OAI.ReflexiveFixedPoints.closure_convexHull_exists_fin line 26

Source documentation

A point of a closed convex hull admits a convex approximation indexed by a nonempty Fin type. The points belong to the original set.

theorem closure_convexHull_exists_fin {D : Set X} {x : X}
    (hx : x ∈ closure (convexHull ℝ D)) {τ : ℝ} (hτ : 0 < τ) :
    ∃ (q : ℕ), 0 < q ∧ ∃ (d : Fin q → X) (w : Fin q → ℝ),
      (∀ i, d i ∈ D) ∧ (∀ i, 0 ≤ w i) ∧ (∑ i, w i = 1) ∧
      ‖(∑ i, w i • d i) - x‖ < τ := by
…

theorem OAI.ReflexiveFixedPoints.sum_prefix_zero_extension line 55

Source documentation

Extending a finitely supported sum by zero to a natural-number prefix does not change it.

theorem sum_prefix_zero_extension {A : Type*} [AddCommMonoid A]
    (s : Finset ℕ) (f : ℕ → A) :
    (∑ i : Fin (s.sup id + 1), if (i : ℕ) ∈ s then f i else 0) =
      ∑ i ∈ s, f i := by
…

theorem OAI.ReflexiveFixedPoints.closure_convexHull_range_exists_prefix line 74

Source documentation

A convex approximation from a sequence uses coefficients on an entire finite prefix; missing indices receive zero weight.

theorem closure_convexHull_range_exists_prefix (u : ℕ → X) {x : X}
    (hx : x ∈ closure (convexHull ℝ (range u))) {τ : ℝ} (hτ : 0 < τ) :
    ∃ (N : ℕ), 0 < N ∧ ∃ (β : Fin N → ℝ),
      (∀ i, 0 ≤ β i) ∧ (∑ i, β i = 1) ∧
      ‖(∑ i, β i • u i) - x‖ < τ := by
…

theorem OAI.ReflexiveFixedPoints.sum_ordered_finset line 107

Source documentation

Enumerating a finite subset in increasing order preserves every sum.

theorem sum_ordered_finset {N : ℕ} {A : Type*} [AddCommMonoid A]
    (s : Finset (Fin N)) (f : Fin N → A) :
    (∑ j : Fin s.card, f (s.orderEmbOfFin rfl j)) = ∑ i ∈ s, f i := by
…

theorem OAI.ReflexiveFixedPoints.positive_support_reindex line 116

Source documentation

Remove exactly the zero coefficients of a finite convex combination. The order embedding retains the original prefix order and index bounds.

theorem positive_support_reindex {N : ℕ} (u : Fin N → X) (β : Fin N → ℝ)
    (hβ : ∀ i, 0 ≤ β i) (hβ1 : ∑ i, β i = 1) :
    ∃ (q : ℕ), 0 < q ∧ ∃ (e : Fin q ↪o Fin N),
      (∀ j, 0 < β (e j)) ∧ (∑ j, β (e j) = 1) ∧
      (∑ j, β (e j) • u (e j)) = ∑ i, β i • u i := by
…