FunctionalVanishing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of uniformly bounded functionals on a closed span

Convergence on the generators extends first by linearity to their span, then by an explicit epsilon estimate to its norm closure. Summable budgets also vanish along any injective sequence of their actual indices.

theorem OAI.ReflexiveFixedPoints.tendsto_zero_of_mem_closedSpan line 22

Source documentation

A sequence of functionals of norm at most one that tends to zero on a set of generators tends to zero at each point of their closed linear span.

theorem tendsto_zero_of_mem_closedSpan
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (φ : ℕ → X →L[ℝ] ℝ) (hφ : ∀ n, ‖φ n‖ ≤ 1)
    {s : Set X}
    (hs : ∀ x ∈ s, Tendsto (fun n => φ n x) atTop (𝓝 0))
    {x : X} (hx : x ∈ (Submodule.span ℝ s).topologicalClosure) :
    Tendsto (fun n => φ n x) atTop (𝓝 0) := by
…

theorem OAI.ReflexiveFixedPoints.summable_budget_tendsto line 58

Source documentation

Summable budgets tend to zero along any injective sequence of indices.

theorem summable_budget_tendsto {I : Type*}
    (e : I → ℝ) (he : Summable e)
    (b : ℕ → I) (hb : Function.Injective b) :
    Tendsto (fun n => e (b n)) atTop (𝓝 0) :=
…