OAI/Analysis/KadisonSimilarity/Representation/CountableLpSubsequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common almost-everywhere subsequence for countably many L² columns. The fast diagonal choice uses summable errors, so the same sequence works for every column.

  1. theorem OAI.KadisonSimilarity.exists_countable_L2_ae_subsequence line 21

    Source documentation

    Countably many L² limits have one choice of indices with simultaneous pointwise convergence almost everywhere.

    theorem exists_countable_L2_ae_subsequence
    (f : ℕ → ℕ → Lp H 2 μ) (g : ℕ → Lp H 2 μ)
    (hf : ∀ j, Tendsto (fun n => f n j) atTop (𝓝 (g j))) :
    ∃ k : ℕ → ℕ, (∀ n, n ≤ k n) ∧
      ∀ᵐ a ∂μ, ∀ j, Tendsto (fun n => f (k n) j a) atTop (𝓝 (g j a)) := by
…