StrongContractionLimits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Recovering a strong contraction limit from countable coordinates

theorem OAI.KadisonKastler.cauchySeq_apply_of_dense_contractions line 18

theorem OAI.KadisonKastler.exists_strong_limit_of_dense_contractions line 42

Source documentation

No convergence is assumed away from the fixed dense sequence.

theorem exists_strong_limit_of_dense_contractions (ξ : ℕ → H) (hξ : DenseRange ξ)
    (A : ℕ → H →L[ℂ] H) (hA : ∀ n, ‖A n‖ ≤ 1)
    (h : ∀ j, CauchySeq (fun n => A n (ξ j))) :
    ∃ T : H →L[ℂ] H, ‖T‖ ≤ 1 ∧
      ∀ x, Tendsto (fun n => A n x) atTop (𝓝 (T x)) := by
…

theorem OAI.KadisonKastler.tendsto_apply_contractions line 73

Source documentation

Uniform contraction bounds permit a varying input vector.

theorem tendsto_apply_contractions {ι : Type*} {l : Filter ι}
    (A : ι → H →L[ℂ] H) (T : H →L[ℂ] H) (hA : ∀ i, ‖A i‖ ≤ 1)
    (hT : ∀ x, Tendsto (fun i => A i x) l (𝓝 (T x)))
    {x : ι → H} {y : H} (hx : Tendsto x l (𝓝 y)) :
    Tendsto (fun i => A i (x i)) l (𝓝 (T y)) := by
…

theorem OAI.KadisonKastler.tendsto_mul_contractions line 85