OAI/Analysis/NuclearUltrapower/CuntzIntertwining.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUltrapower.CuntzAveraging.rowSum line 16
2. theorem OAI.NuclearUltrapower.CuntzAveraging.rowSum_apply line 18
3. theorem OAI.NuclearUltrapower.CuntzAveraging.inner_rows line 21
4. theorem OAI.NuclearUltrapower.CuntzAveraging.inner_rowSum line 27
5. theorem OAI.NuclearUltrapower.CuntzAveraging.rowSum_norm_sq line 32
6. def OAI.NuclearUltrapower.CuntzAveraging.weight line 40

   Source documentation

   Square-length averages avoid square-root denominators while retaining the exact isometry on the support of an arbitrary nonunital representation.

   def weight (n : ℕ) : ℂ := (((n : ℝ)+1)⁻¹ : ℝ)

7. theorem OAI.NuclearUltrapower.CuntzAveraging.weight_norm line 42
8. def OAI.NuclearUltrapower.CuntzAveraging.averaged line 45
9. theorem OAI.NuclearUltrapower.CuntzAveraging.averaged_norm line 47
10. theorem OAI.NuclearUltrapower.CuntzAveraging.averaged_norm_le line 55
11. theorem OAI.NuclearUltrapower.CuntzAveraging.range_telescope line 62
12. theorem OAI.NuclearUltrapower.CuntzAveraging.range_telescope_rev line 69
13. theorem OAI.NuclearUltrapower.CuntzAveraging.rowSum_generator line 76

    Source documentation

    Only two boundary rows survive for a generator.

    theorem rowSum_generator (N : ℕ) (i : Fin 2) :
        (rowSum R N).comp (R (generator i)) - (left i).comp (rowSum R N) =
          ((row R 0)-(row R N)).comp (R (generator i)) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzAveraging.rowSum, OAI.NuclearUltrapower.CuntzAveraging.left, OAI.NuclearUltrapower.CuntzAveraging.row

14. theorem OAI.NuclearUltrapower.CuntzAveraging.rowSum_adjoint line 87

    Source documentation

    The adjoint generator has the same two-boundary estimate.

    theorem rowSum_adjoint (N : ℕ) (i : Fin 2) :
        (rowSum R N).comp (star (R (generator i))) - (star (left i)).comp (rowSum R N) =
          (star (left i)).comp ((row R N)-(row R 0)) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzAveraging.rowSum, OAI.NuclearUltrapower.CuntzAveraging.left, OAI.NuclearUltrapower.CuntzAveraging.row

15. theorem OAI.NuclearUltrapower.dense_bounded_tendsto_zero line 113

    Source documentation

    A uniformly bounded sequence of linear maps converges to zero everywhere once it does so on a dense range. This elementary argument requires no separability or pointwise boundedness theorem.

    theorem dense_bounded_tendsto_zero {A E P : Type*}
        [NormedAddCommGroup A] [NormedSpace ℂ A]
        [NormedAddCommGroup E] [NormedSpace ℂ E]
        (D : ℕ → A →ₗ[ℂ] E) (C : ℝ) (hC : 0 < C)
        (hbound : ∀ n a, ‖D n a‖ ≤ C * ‖a‖)
        (g : P → A) (hg : DenseRange g)
        (hlim : ∀ p, Tendsto (fun n => D n (g p)) atTop (𝓝 0)) (a : A) :
        Tendsto (fun n => D n a) atTop (𝓝 0) := by
    …

16. def OAI.NuclearUltrapower.intertwiningDefect line 143
17. theorem OAI.NuclearUltrapower.intertwiningDefect_apply line 151
18. theorem OAI.NuclearUltrapower.intertwiningDefect_bound line 154
19. theorem OAI.NuclearUltrapower.intertwiningDefect_mul line 167
20. theorem OAI.NuclearUltrapower.intertwiningDefect_tendsto_mul line 177

    Source documentation

    Approximate intertwining propagates through products without any finite coordinate relation being silently imposed.

    theorem intertwiningDefect_tendsto_mul (W : ℕ → H →L[ℂ] K) {a b : A}
        (ha : Tendsto (fun n => intertwiningDefect R T (W n) a) atTop (𝓝 0))
        (hb : Tendsto (fun n => intertwiningDefect R T (W n) b) atTop (𝓝 0)) :
        Tendsto (fun n => intertwiningDefect R T (W n) (a*b)) atTop (𝓝 0) := by
    …

    Mentions: OAI.NuclearUltrapower.intertwiningDefect

21. def OAI.NuclearUltrapower.CuntzAveraging.concrete line 205
22. def OAI.NuclearUltrapower.CuntzAveraging.amplified line 208
23. theorem OAI.NuclearUltrapower.CuntzAveraging.amplified_generator line 211
24. abbrev OAI.NuclearUltrapower.CuntzAveraging.defect line 216
25. theorem OAI.NuclearUltrapower.CuntzAveraging.averaged_support line 219
26. theorem OAI.NuclearUltrapower.CuntzAveraging.defect_one line 229
27. theorem OAI.NuclearUltrapower.CuntzAveraging.generator_norm_le line 235
28. theorem OAI.NuclearUltrapower.CuntzAveraging.rowSum_generator_bound line 239
29. theorem OAI.NuclearUltrapower.CuntzAveraging.rowSum_adjoint_bound line 249
30. theorem OAI.NuclearUltrapower.CuntzAveraging.defect_generator_bound line 259
31. theorem OAI.NuclearUltrapower.CuntzAveraging.defect_adjoint_bound line 271
32. theorem OAI.NuclearUltrapower.CuntzAveraging.inverse_weight_tendsto line 284
33. theorem OAI.NuclearUltrapower.CuntzAveraging.defect_generator_tendsto line 289
34. theorem OAI.NuclearUltrapower.CuntzAveraging.defect_adjoint_tendsto line 295
35. theorem OAI.NuclearUltrapower.CuntzAveraging.averaged_commuting line 302

    Source documentation

    Second-coordinate intertwining is exact, even for a degenerate range.

    theorem averaged_commuting (n : ℕ) (T : H →L[ℂ] H)
        (hT : ∀ a, Commute (R a) T) :
        (averaged R n).comp T = (right T).comp (averaged R n) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzAveraging.averaged, OAI.NuclearUltrapower.CuntzAveraging.right