WeakCommonTerminal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common actual resolvent terminal for weak prediction detectors

The scalar convergence is derived from weak convergence of the fully evaluated predictions. The displacement convergence is the proved estimate for the actual resolvent terminal sequence and actual generated maps.

theorem OAI.ReflexiveFixedPoints.detector_tendsto_of_weak_tendsto line 27

Source documentation

A continuous linear functional converts an actual weak prediction limit to the scalar detector limit. No weak continuity of a nonlinear map is used.

theorem detector_tendsto_of_weak_tendsto {X : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    {J : Type*} {l : Filter J} (f : X →L[ℝ] ℝ) (y z : X) (q : J → X)
    (hq : Tendsto (fun j => toWeakSpace ℝ X (q j)) l
      (𝓝 (toWeakSpace ℝ X z))) :
    Tendsto (fun j => f (y - q j)) l (𝓝 (f (y - z))) := by
…

theorem OAI.ReflexiveFixedPoints.exists_common_terminalSequence line 43

Source documentation

Choose one index of the actual terminal resolvent sequence satisfying every finite weak prediction detector and every fixed generated map's total bound.

theorem exists_common_terminalSequence
    (hKclosed : IsClosed K) (hKconvex : Convex ℝ K)
    (T : K → K) (hT : LipschitzWith 1 T)
    (hdiam : ∀ a c : K, ‖(a : X) - c‖ ≤ 1) (x : K)
    {I J : Type*} [Finite I] [Fintype J]
    {l : Filter ℕ} [NeBot l] (hl : l ≤ atTop)
    (q : I → K → K) (y z : I → K) (f : I → X →L[ℝ] ℝ) (e : I → ℝ)
    (he : ∀ i, 0 < e i)
    (hz : ∀ i, Tendsto
      (fun j => toWeakSpace ℝ X (q i (terminalSequence hKclosed hKconvex T hT x j)))
      l (𝓝 (toWeakSpace ℝ X (z i))))
    (hdet : ∀ i, 1 - e i ≤ f i ((y i : X) - z i))
…

Mentions: OAI.ReflexiveFixedPoints.terminalSequence