OAI/Analysis/NuclearUltrapower/VariableUltraproduct.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NuclearUltrapower.tendsto_ultralimit_of_bounded line 18

   Source documentation

   A bounded scalar family has a genuine ultralimit.

   theorem tendsto_ultralimit_of_bounded {ι : Type u} (ω : Ultrafilter ι)
       {F : Type v} [NormedAddCommGroup F] [ProperSpace F] (f : ι → F)
       (hf : ∃ C : ℝ, ∀ i, ‖f i‖ ≤ C) :
       Tendsto f (ω : Filter ι) (𝓝 (limUnder (ω : Filter ι) f)) := by
   …

2. abbrev OAI.NuclearUltrapower.VariableUltra.Seq line 34
3. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 35) line 35
4. def OAI.NuclearUltrapower.VariableUltra.Rel line 38

   Source documentation

   Equality modulo norm-null sequences, with unrestricted varying dimensions.

   def Rel (x y : Seq A) : Prop :=
   …

   Mentions: OAI.NuclearUltrapower.VariableUltra.Seq

5. theorem OAI.NuclearUltrapower.VariableUltra.null_add line 42
6. theorem OAI.NuclearUltrapower.VariableUltra.null_mul_left line 50
7. theorem OAI.NuclearUltrapower.VariableUltra.null_mul_right line 59
8. def OAI.NuclearUltrapower.VariableUltra.con line 67
9. abbrev OAI.NuclearUltrapower.VariableUltra.Algebra line 88
10. theorem OAI.NuclearUltrapower.VariableUltra.rel_star line 91
11. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 95) line 95
12. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 97) line 97
13. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 109) line 109
14. def OAI.NuclearUltrapower.VariableUltra.mk line 114
15. def OAI.NuclearUltrapower.VariableUltra.seqNorm line 118
16. theorem OAI.NuclearUltrapower.VariableUltra.seqNorm_tendsto line 121
17. theorem OAI.NuclearUltrapower.VariableUltra.seqNorm_nonneg line 127
18. theorem OAI.NuclearUltrapower.VariableUltra.seqNorm_le line 131
19. theorem OAI.NuclearUltrapower.VariableUltra.seqNorm_lipschitz line 135
20. def OAI.NuclearUltrapower.VariableUltra.null line 143
21. theorem OAI.NuclearUltrapower.VariableUltra.mem_null_iff line 151
22. instance OAI.NuclearUltrapower.VariableUltra.null_closed line 159
23. def OAI.NuclearUltrapower.VariableUltra.quotientEquiv line 167

    Source documentation

    Identification with the ordinary complete normed linear quotient.

    def quotientEquiv : Algebra A ω ≃ₗ[ℂ] (Seq A ⧸ null A ω) :=
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Algebra, OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.VariableUltra.null

24. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 189) line 189
25. theorem OAI.NuclearUltrapower.VariableUltra.norm_eq_quotient_norm line 192
26. theorem OAI.NuclearUltrapower.VariableUltra.seqNorm_eq_of_rel line 196
27. theorem OAI.NuclearUltrapower.VariableUltra.mk_norm line 204

    Source documentation

    Exact quotient norm, including the truncation upper bound.

    theorem mk_norm (x : Seq A) : ‖mk A ω x‖ = seqNorm A ω x := by
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.VariableUltra.mk, OAI.NuclearUltrapower.VariableUltra.seqNorm

28. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 235) line 235
29. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 245) line 245
30. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 253) line 253
31. def OAI.NuclearUltrapower.VariableUltra.quotientIsometry line 263
32. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 266) line 266
33. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 268) line 268
34. instance OAI.NuclearUltrapower.VariableUltra.(instance at line 269) line 269
35. theorem OAI.NuclearUltrapower.VariableUltra.matrix_norm_le_sum line 291

    Source documentation

    A dimension-controlled bound for the C*-matrix norm, independent of the entry algebra. This also proves continuity for bounded varying-algebra families.

    theorem matrix_norm_le_sum {A : Type*} [CStarAlgebra A]
        [PartialOrder A] [StarOrderedRing A] {n : Type*} [Fintype n]
        (M : CStarMatrix n n A) : ‖M‖ ≤ ∑ j, ∑ i, ‖M i j‖ := by
    …

36. def OAI.NuclearUltrapower.VariableUltra.matrixEntry line 317

    Source documentation

    One entry of a bounded family of matrices is a bounded family.

    def matrixEntry (M : Seq (fun i => CStarMatrix n n (A i))) (j k : n) : Seq A :=
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Seq

37. theorem OAI.NuclearUltrapower.VariableUltra.matrixEntry_apply line 323
38. def OAI.NuclearUltrapower.VariableUltra.matrixFamily line 328

    Source documentation

    Assemble a finite matrix of bounded families. There is no bound on the dimension of any of the entry algebras.

    def matrixFamily (M : CStarMatrix n n (Seq A)) : Seq (fun i => CStarMatrix n n (A i)) :=
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Seq

39. theorem OAI.NuclearUltrapower.VariableUltra.matrixFamily_apply line 340
40. def OAI.NuclearUltrapower.VariableUltra.matrixQuotient line 344

    Source documentation

    Pass to the ultraproduct in every matrix entry.

    def matrixQuotient : Algebra (fun i => CStarMatrix n n (A i)) ω →⋆ₐ[ℂ]
        CStarMatrix n n (Algebra A ω) where
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Algebra

41. theorem OAI.NuclearUltrapower.VariableUltra.matrixQuotient_mk line 428
42. theorem OAI.NuclearUltrapower.VariableUltra.matrixQuotient_injective line 432

    Source documentation

    Fixed finite matrix amplification commutes with the quotient, entry by entry.

    theorem matrixQuotient_injective : Function.Injective (matrixQuotient A ω n) := by
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.matrixQuotient

43. theorem OAI.NuclearUltrapower.VariableUltra.matrixQuotient_surjective line 446
44. theorem OAI.NuclearUltrapower.VariableUltra.matrixQuotient_norm line 462

    Source documentation

    No matrix norm is lost in the entrywise quotient identification.

    theorem matrixQuotient_norm (M : Algebra (fun i => CStarMatrix n n (A i)) ω) :
        ‖matrixQuotient A ω n M‖ = ‖M‖ :=
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Algebra, OAI.NuclearUltrapower.VariableUltra.matrixQuotient

45. def OAI.NuclearUltrapower.VariableUltra.matrixQuotientEquiv line 468

    Source documentation

    This is the norm-ultrafilter version of the fixed-size amplification identity in the tensor-norm formulation.

    def matrixQuotientEquiv : Algebra (fun i => CStarMatrix n n (A i)) ω ≃⋆ₐ[ℂ]
        CStarMatrix n n (Algebra A ω) :=
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Algebra

46. def OAI.NuclearUltrapower.matrixMap line 479

    Source documentation

    Entrywise amplification of a unital star homomorphism.

    def matrixMap {A B : Type*} [CStarAlgebra A] [CStarAlgebra B]
        (n : Type*) [Fintype n] [DecidableEq n] (f : A →⋆ₐ[ℂ] B) :
        CStarMatrix n n A →⋆ₐ[ℂ] CStarMatrix n n B where
    …

47. theorem OAI.NuclearUltrapower.matrixMap_apply line 501
48. theorem OAI.NuclearUltrapower.VariableUltra.matrixQuotient_matrixFamily line 516
49. theorem OAI.NuclearUltrapower.VariableUltra.matrixMap_mk_norm line 524

    Source documentation

    The norm of each FIXED finite matrix over the quotient is its coordinate ultralimit. The entry algebras and their dimensions are unrestricted.

    theorem matrixMap_mk_norm (M : CStarMatrix n n (Seq A)) :
        ‖matrixMap n (mk A ω) M‖ =
          seqNorm (fun i => CStarMatrix n n (A i)) ω (matrixFamily A n M) := by
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.matrixMap, OAI.NuclearUltrapower.VariableUltra.mk, OAI.NuclearUltrapower.VariableUltra.seqNorm, OAI.NuclearUltrapower.VariableUltra.matrixFamily

50. theorem OAI.NuclearUltrapower.VariableUltra.matrixMap_mk_norm_le line 530

    Source documentation

    Finite exceptional coordinates can be discarded before amplification.

    theorem matrixMap_mk_norm_le (M : CStarMatrix n n (Seq A)) {C : ℝ}
        (h : ∀ᶠ i in (ω : Filter ι), ‖matrixFamily A n M i‖ ≤ C) :
        ‖matrixMap n (mk A ω) M‖ ≤ C := by
    …

    Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.VariableUltra.matrixFamily, OAI.NuclearUltrapower.matrixMap, OAI.NuclearUltrapower.VariableUltra.mk