AnchorAdaptiveSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Adaptive selection for the constructed anchor

The analytic hypotheses of the generic finite-selection theorem are discharged by the actual tail-limit set and closed-convex-hull conclusions of AnchorPoint. resolventAnchorPoint chooses that record from the proved compact-semigroup construction for the actual resolvent tails.

theorem OAI.ReflexiveFixedPoints.AnchorPoint.adaptive_selection line 29

Source documentation

An anchor supports finite successive selections with arbitrary state-dependent thresholds and post-map auxiliary choices.

theorem AnchorPoint.adaptive_selection
    [TopologicalSpace.MetrizableSpace (WeakCarrier K)]
    {H : ℕ → Set (K → K)} (A : AnchorPoint H)
    {S : Type v} (threshold : ℕ → S → ℕ)
    (hthreshold : ∀ i s, 1 ≤ threshold i s)
    (transition : ℕ → S → (K → K) → S → Prop) (initial : S)
    (htransition : ∀ i s G,
      G ∈ H (threshold i s) → ∃ s', transition i s G s')
    {τ : ℝ} (hτ : 0 < τ) :
    ∃ (N : ℕ), 0 < N ∧
      ∃ (state : Fin (N + 1) → S) (selected : Fin N → K → K)
        (β : Fin N → ℝ),
…

Mentions: OAI.ReflexiveFixedPoints.WeakCarrier, OAI.ReflexiveFixedPoints.AnchorPoint

def OAI.ReflexiveFixedPoints.resolventAnchorPoint line 53
Source documentation
The anchor is constructed from actual resolvent tails. No idempotent, return law, or tail-limit convex-hull statement is an extra premise.
```
def resolventAnchorPoint [CompleteSpace X]
    (hKnonempty : K.Nonempty) (hKclosed : IsClosed K) (hKconvex : Convex ℝ K)
    (T : K → K) (hT : LipschitzWith 1 T) (hKweak : WeaklyCompact K) :
    AnchorPoint (tailFamily hKclosed hKconvex T hT) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.AnchorPoint, OAI.ReflexiveFixedPoints.tailFamily