Products.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Bounded C-star products and the generated separable unital algebra.

abbrev OAI.Kaplansky.BoundedProduct line 21
instance OAI.Kaplansky.boundedProductCStarAlgebra line 23
def OAI.Kaplansky.boundedProductLift line 25
theorem OAI.Kaplansky.boundedProductLift_apply line 29
theorem OAI.Kaplansky.boundedProduct_nonneg_iff line 34
Source documentation
Positivity in the bounded product is equivalent to coordinatewise positivity. Boundedness of the adjoint-square witnesses is proved.
```
theorem boundedProduct_nonneg_iff (f : BoundedProduct A) :
    0 ≤ f ↔ ∀ i, 0 ≤ f i := by
…
```
Mentions: OAI.Kaplansky.BoundedProduct
theorem OAI.Kaplansky.boundedProduct_le_iff line 61
def OAI.Kaplansky.boundedProductEval line 65
theorem OAI.Kaplansky.boundedProduct_sum_apply line 71

theorem OAI.Kaplansky.boundedProduct_column line 76

Source documentation

The coordinate column identities give the actual product identity.

theorem boundedProduct_column {N : ℕ} (x : Fin N → ∀ i, A i)
    (hx : ∀ k i, ‖x k i‖ ≤ 1)
    (hcol : ∀ i, ∑ k, star (x k i) * x k i = 1) :
    ∑ k, star (boundedProductLift (x k) (hx k)) * boundedProductLift (x k) (hx k) =
      (1 : BoundedProduct A) := by
…

Mentions: OAI.Kaplansky.boundedProductLift, OAI.Kaplansky.BoundedProduct

theorem OAI.Kaplansky.boundedProduct_row line 86
theorem OAI.Kaplansky.countable_monoid_closure line 107
Source documentation
Countably many letters have only countably many finite multiplicative words.
```
theorem countable_monoid_closure {A : Type*} [Monoid A] {s : Set A}
    (hs : s.Countable) : (Submonoid.closure s : Set A).Countable := by
…
```
def OAI.Kaplansky.generatedAlgebra line 117
Source documentation
The actual unital closed C*-subalgebra generated by the specified set.
```
def generatedAlgebra (s : Set A) : StarSubalgebra ℂ A :=
…
```
instance OAI.Kaplansky.generatedAlgebra_closed line 120
instance OAI.Kaplansky.generatedAlgebra_cstar line 123
theorem OAI.Kaplansky.generatedAlgebra_separable line 126
def OAI.Kaplansky.generatedGenerator line 138
instance OAI.Kaplansky.finiteGeneratedAlgebra_separable line 142
theorem OAI.Kaplansky.closedSubalgebra_nonneg_iff line 165
Source documentation
Closed C*-subalgebras reflect positivity. The square-root witness belongs to the subalgebra by continuous functional calculus.
```
theorem closedSubalgebra_nonneg_iff (S : StarSubalgebra ℂ A)
    [IsClosed (S : Set A)] (a : S) : 0 ≤ a ↔ 0 ≤ (a : A) := by
…
```
theorem OAI.Kaplansky.closedSubalgebra_le_iff line 182
theorem OAI.Kaplansky.generatedGenerator_column line 187
theorem OAI.Kaplansky.generatedGenerator_row line 196
theorem OAI.Kaplansky.bounded_generated_relations line 205
theorem OAI.Kaplansky.generatedAlgebra_nontrivial line 226
Source documentation
The closed generated algebra contains the ambient unit and is nontrivial whenever the ambient algebra is nontrivial.
```
theorem generatedAlgebra_nontrivial {A : Type*} [CStarAlgebra A] [Nontrivial A]
    (s : Set A) : Nontrivial (generatedAlgebra s) := by
…
```
Mentions: OAI.Kaplansky.generatedAlgebra
theorem OAI.Kaplansky.boundedProduct_nontrivial line 232
Source documentation
A nonempty family of nontrivial coordinate algebras has a nontrivial bounded product. Nonemptiness is explicit; an empty product is excluded.
```
theorem boundedProduct_nontrivial {I : Type*} [Nonempty I] {A : I → Type*}
    [∀ i, CStarAlgebra (A i)] [∀ i, Nontrivial (A i)] : Nontrivial (BoundedProduct A) := by
…
```
Mentions: OAI.Kaplansky.BoundedProduct
theorem OAI.Kaplansky.boundedGeneratedAlgebra_nontrivial line 240