LaurentAlgebra.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The algebraic star algebra generated by one unitary is exactly the linear span of all its integer powers. No topology on the ambient algebra is needed.

def OAI.Generator.unitaryPowerMonoid line 22
theorem OAI.Generator.unitary_power_mem_adjoin line 29
theorem OAI.Generator.unitary_adjoin_eq_span line 43
def OAI.Generator.nonzeroUnitaryPowers line 71
def OAI.Generator.centerLinear line 74
theorem OAI.Generator.centerLinear_apply line 78
theorem OAI.Generator.center_adjoin_mem_span line 81

theorem OAI.Generator.centered_elemental_mem_closedSpan line 108

Source documentation

Every centered element of the actual norm-closed generated star algebra is a norm limit of linear combinations of nonzero powers.

theorem centered_elemental_mem_closedSpan (v : unitary A) (φ : A →L[ℂ] ℂ)
    (h1 : φ 1=1) (hhaar : ∀ n : ℤ,n ≠ 0 → φ (↑(v^n) : A)=0)
    (x : A) (hx : x ∈ StarAlgebra.elemental ℂ (v : A)) (hcenter : φ x=0) :
    x ∈ (Submodule.span ℂ (nonzeroUnitaryPowers v)).topologicalClosure := by
…

Mentions: OAI.Generator.nonzeroUnitaryPowers

def OAI.Generator.sandwichFunctional line 130
theorem OAI.Generator.functional_sandwich_closedSpan line 136
theorem OAI.Generator.functional_product_closedSpan line 146
theorem OAI.Generator.alternatingFrom_closedSpan_slots line 163
theorem OAI.Generator.alternatingMomentsZero_closedSpan line 173
def OAI.Generator.freeSets line 195
Source documentation
Standard freeness: every nonempty alternating product of centered elements vanishes, starting with either algebra and with no restriction on length parity.
```
def freeSets (φ : A → ℂ) (S T : Set A) : Prop :=
…
```

theorem OAI.Generator.centered_subalgebra_closure_mem line 205

Source documentation

Centering commutes with norm approximation in a unital subalgebra.

theorem centered_subalgebra_closure_mem (φ : A →L[ℂ] ℂ) (h1 : φ 1=1)
    (D : Subalgebra ℂ A) (x : A) (hx : x ∈ D.topologicalClosure) (hcenter : φ x=0) :
    x ∈ (Submodule.span ℂ {d | d ∈ D ∧ φ d=0}).topologicalClosure := by
…

theorem OAI.Generator.unitary_generated_free_of_power_moments line 225