AdaptiveSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite adaptive return to an anchor

The tail closures and the anchor's closed-convex-hull membership are the actual analytic input to this helper. The anchor construction proves those inputs for the actual resolvent tails. The arbitrary state below can retain every earlier candidate and its auxiliary detector, including the candidates which eventually receive coefficient zero.

theorem OAI.ReflexiveFixedPoints.mem_closedConvexHull_of_weak_subsequence line 31
Source documentation
Every weak limit of points from a sequence lies in the norm-closed convex hull of that sequence. This uses weak closedness of a convex norm closure, not weak continuity of any nonlinear map.
```
theorem mem_closedConvexHull_of_weak_subsequence
    (u : ℕ → X) (j : ℕ → ℕ) {d : X}
    (h : Tendsto (fun n => toWeakSpace ℝ X (u (j n))) atTop
      (𝓝 (toWeakSpace ℝ X d))) :
    d ∈ closure (convexHull ℝ (range u)) := by
…
```
theorem OAI.ReflexiveFixedPoints.adaptive_finite_selection line 57
Source documentation
Fully state-dependent finite selection. Every threshold is read from the preceding state, and the legal next state is chosen after the map. Only after a finite prefix has been obtained are its coefficients chosen.
The returned selected list includes every candidate, including those of zero weight. positive_support_reindex separately extracts the retained children in their original order without changing this full history.
```
theorem adaptive_finite_selection
    {K : Set X} [TopologicalSpace.MetrizableSpace (WeakCarrier K)]
    {M : Type v} {S : Type w}
    (eval : M → K) (family : ℕ → Set M) (x : K) (D : Set X)
    (hDK : D ⊆ K)
    (hx : (x : X) ∈ closure (convexHull ℝ D))
    (hD : ∀ m, 1 ≤ m → ∀ d : D,
      normToWeak K ⟨d, hDK d.property⟩ ∈
        closure ((fun a => normToWeak K (eval a)) '' family m))
    (threshold : ℕ → S → ℕ)
    (hthreshold : ∀ i s, 1 ≤ threshold i s)
    (transition : ℕ → S → M → S → Prop) (initial : S)
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier, OAI.ReflexiveFixedPoints.normToWeak