CommonTerminal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common terminal index for finitely many detectors

This finite-filter argument chooses one actual index at which all scalar prediction detectors and the total displacement bound hold. Its applications supply the scalar limits by evaluating continuous linear functionals on the actual weak prediction limits, and supply displacement convergence for the actual finite collection of node maps.

theorem OAI.ReflexiveFixedPoints.common_terminal_of_tendsto line 27

Source documentation

Finitely many detector limits and one displacement limit can be met at the same index. No uniform lower bound on the positive detector errors is needed.

theorem common_terminal_of_tendsto
    {I J : Type*} [Finite I] {l : Filter J} [NeBot l]
    (e a : I → ℝ) (g : I → J → ℝ) (D : J → ℝ) (M : ℝ)
    (he : ∀ i, 0 < e i)
    (ha : ∀ i, 1 - e i ≤ a i)
    (hg : ∀ i, Tendsto (g i) l (𝓝 (a i)))
    (hD : Tendsto D l (𝓝 0)) (hM : 0 < M) :
    ∃ j, (∀ i, 1 - 2 * e i ≤ g i j) ∧ D j ≤ M := by
…

theorem OAI.ReflexiveFixedPoints.common_terminal_of_tendsto_mono line 49

Source documentation

The displacement may converge in a larger filter, in particular the cofinite filter contained in a fixed free ultrafilter.

theorem common_terminal_of_tendsto_mono
    {I J : Type*} [Finite I] {l l' : Filter J} [NeBot l]
    (hll' : l ≤ l')
    (e a : I → ℝ) (g : I → J → ℝ) (D : J → ℝ) (M : ℝ)
    (he : ∀ i, 0 < e i)
    (ha : ∀ i, 1 - e i ≤ a i)
    (hg : ∀ i, Tendsto (g i) l (𝓝 (a i)))
    (hD : Tendsto D l' (𝓝 0)) (hM : 0 < M) :
    ∃ j, (∀ i, 1 - 2 * e i ≤ g i j) ∧ D j ≤ M :=
…