OAI/Analysis/WeakInfiniteness/TensorFoundations.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.norm_completion_le line 20

   Distinct definitions of this name: ComparatorChallenges/ExactInfiniteness.lean:17 (different declaration text). Qualify references as OAI.WeakPureInfiniteness.norm_completion_le@path.

2. lemma OAI.WeakPureInfiniteness.norm_completion line 27

   Distinct definitions of this name: ComparatorChallenges/ExactInfiniteness.lean:25 (different declaration text). Qualify references as OAI.WeakPureInfiniteness.norm_completion@path.

3. lemma OAI.WeakPureInfiniteness.completion_comp line 33
4. lemma OAI.WeakPureInfiniteness.completion_add line 40
5. lemma OAI.WeakPureInfiniteness.completion_smul line 47
6. lemma OAI.WeakPureInfiniteness.completion_zero line 57
7. lemma OAI.WeakPureInfiniteness.inner_mapL_star line 70
8. lemma OAI.WeakPureInfiniteness.completion_mapL_star line 82
9. structure OAI.WeakPureInfiniteness.ComplexHilbert line 100

   Also declared: ComparatorChallenges/ExactInfiniteness.lean:34 (same declaration text).

10. instance OAI.WeakPureInfiniteness.(instance at line 109) line 109
11. instance OAI.WeakPureInfiniteness.completedTensorCStar line 111

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:44 (same declaration text).

12. instance OAI.WeakPureInfiniteness.hilbertOperatorsCStar line 114

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:47 (same declaration text).

13. structure OAI.WeakPureInfiniteness.SpatialRepresentation line 117

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:50 (same declaration text).

14. abbrev OAI.WeakPureInfiniteness.SpatialRepresentation.hilbert line 124

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:57 (same declaration text).

15. abbrev OAI.WeakPureInfiniteness.SpatialRepresentation.space line 129

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:62 (same declaration text).

16. def OAI.WeakPureInfiniteness.SpatialAmbient line 133

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:66 (same declaration text).

17. instance OAI.WeakPureInfiniteness.spatialAmbientCStar line 137

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:70 (same declaration text).

18. instance OAI.WeakPureInfiniteness.spatialAmbientCoeFun line 143

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:76 (same declaration text).

19. def OAI.WeakPureInfiniteness.spatialElementary line 148

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:81 (same declaration text).

20. lemma OAI.WeakPureInfiniteness.spatialElementary_zero_left line 165
21. lemma OAI.WeakPureInfiniteness.spatialElementary_zero_right line 172
22. lemma OAI.WeakPureInfiniteness.spatialElementary_add_left line 178
23. lemma OAI.WeakPureInfiniteness.spatialElementary_add_right line 187
24. lemma OAI.WeakPureInfiniteness.spatialElementary_smul_left line 196
25. lemma OAI.WeakPureInfiniteness.spatialElementary_smul_right line 204
26. lemma OAI.WeakPureInfiniteness.spatialElementary_mul line 212
27. lemma OAI.WeakPureInfiniteness.spatialElementary_star line 223
28. lemma OAI.WeakPureInfiniteness.norm_spatialElementary_le line 232
29. def OAI.WeakPureInfiniteness.minimalTensorSubalgebra line 243

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:93 (same declaration text).

30. abbrev OAI.WeakPureInfiniteness.MinimalTensor line 248

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:98 (same declaration text).

31. instance OAI.WeakPureInfiniteness.(instance at line 251) line 251
32. def OAI.WeakPureInfiniteness.SpatialRepresentation.precompRight line 263

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:113 (same declaration text).

33. def OAI.WeakPureInfiniteness.tensorKernelIdeal line 270

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:120 (same declaration text).

34. def OAI.WeakPureInfiniteness.Exact line 276

    Also declared: ComparatorChallenges/ExactInfiniteness.lean:126 (same declaration text).

35. def OAI.WeakPureInfiniteness.CompletelyPositive line 288
36. def OAI.WeakPureInfiniteness.CompletelyPositive.toMap line 292
37. lemma OAI.WeakPureInfiniteness.completelyPositive_of_map line 297
38. def OAI.WeakPureInfiniteness.Nuclear line 306
39. structure OAI.WeakPureInfiniteness.CuntzRepresentation line 316
40. abbrev OAI.WeakPureInfiniteness.CuntzAmbient line 324
41. instance OAI.WeakPureInfiniteness.(instance at line 327) line 327
42. lemma OAI.WeakPureInfiniteness.CuntzRepresentation.norm_generator line 329
43. def OAI.WeakPureInfiniteness.cuntzGenerator line 335
44. def OAI.WeakPureInfiniteness.oInfinitySubalgebra line 340
45. abbrev OAI.WeakPureInfiniteness.OInfinity line 343
46. instance OAI.WeakPureInfiniteness.(instance at line 345) line 345
47. abbrev OAI.WeakPureInfiniteness.FockSpace line 352
48. def OAI.WeakPureInfiniteness.fockBasis line 354
49. lemma OAI.WeakPureInfiniteness.fockBasis_apply line 361
50. lemma OAI.WeakPureInfiniteness.fockPrefix_orthogonal line 364
51. def OAI.WeakPureInfiniteness.fockShift line 371
52. lemma OAI.WeakPureInfiniteness.fockShift_single line 375
53. lemma OAI.WeakPureInfiniteness.fockShift_apply line 379
54. lemma OAI.WeakPureInfiniteness.fockShift_apply_ne line 395
55. lemma OAI.WeakPureInfiniteness.fockShift_adjoint_apply line 409
56. lemma OAI.WeakPureInfiniteness.fockShift_relations line 417
57. instance OAI.WeakPureInfiniteness.fockSpace_nontrivial line 428
58. def OAI.WeakPureInfiniteness.fockRepresentation line 434
59. instance OAI.WeakPureInfiniteness.(instance at line 439) line 439
60. instance OAI.WeakPureInfiniteness.(instance at line 441) line 441
61. instance OAI.WeakPureInfiniteness.(instance at line 447) line 447
62. def OAI.WeakPureInfiniteness.oInfinityEvaluation line 449
63. def OAI.WeakPureInfiniteness.oInfinityIsometry line 459
64. lemma OAI.WeakPureInfiniteness.oInfinityEvaluation_isometry line 464
65. lemma OAI.WeakPureInfiniteness.oInfinityIsometry_relations line 467