AdaptiveRun.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Successive choices with arbitrary auxiliary state

The state may contain the entire preceding candidate history. A threshold is read before the next map is selected; the transition relation supplies auxiliary choices only after that map is known. No convex coefficients are involved in this infinite sequence.

theorem OAI.ReflexiveFixedPoints.exists_adaptive_metric_run line 29

Source documentation

A legal infinite sequence exists even when every threshold and every legal auxiliary transition depends on the whole preceding state. The caller may take the state to be a list of all previous candidate records.

theorem exists_adaptive_metric_run
    {S : Type u} {M : Type v} {W : Type w} [PseudoMetricSpace W]
    {q : ℕ} (hq : 0 < q) (target : Fin q → W)
    (eval : M → W) (family : ℕ → Set M)
    (threshold : ℕ → S → ℕ)
    (transition : ℕ → S → M → S → Prop) (initial : S)
    (hclosure : ∀ (i : ℕ) (s : S) (r : Fin q),
      target r ∈ closure (eval '' family (threshold i s)))
    (htransition : ∀ (i : ℕ) (s : S) (a : M),
      a ∈ family (threshold i s) → ∃ s', transition i s a s') :
    ∃ (state : ℕ → S) (selected : ℕ → M),
      state 0 = initial ∧ ∀ i,
…

theorem OAI.ReflexiveFixedPoints.tendsto_cyclic_target line 65

Source documentation

Cycling through finitely many targets with a vanishing error gives a convergent subsequence for each target. The selected maps and their state history are otherwise unrestricted.

theorem tendsto_cyclic_target
    {W : Type w} [PseudoMetricSpace W] {q : ℕ} (hq : 0 < q)
    (target : Fin q → W) (u : ℕ → W)
    (hclose : ∀ i, dist (u i) (target ⟨i % q, Nat.mod_lt i hq⟩) <
      1 / ((i : ℝ) + 1)) (r : Fin q) :
    Tendsto (fun n : ℕ => u (q * n + r.val)) atTop (𝓝 (target r)) := by
…