FaithfulGNS.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.norm_positive_center line 16
Source documentation
The disk estimate which exposes a positive element to Hahn--Banach.
```
theorem norm_positive_center (a : A) (ha : 0 ≤ a) :
    ‖a - (‖a‖ / 2 : ℝ) • (1 : A)‖ ≤ ‖a‖ / 2 := by
…
```
theorem OAI.NuclearUltrapower.complex_disk_intersection line 32
Source documentation
Elementary disk intersection, used to retain the unit under norm-preserving extension.
```
theorem complex_disk_intersection (z : ℂ) (h0 : ‖z‖ ≤ 1) (h2 : ‖2-z‖ ≤ 1) : z = 1 := by
…
```

theorem OAI.NuclearUltrapower.exists_unital_norming_functional line 48

Source documentation

Hahn--Banach norms a positive element by a unital contraction.

theorem exists_unital_norming_functional (a : A) (ha : 0 ≤ a) (ha0 : a ≠ 0) :
    ∃ f : A →L[ℂ] ℂ, ‖f‖ = 1 ∧ f 1 = 1 ∧ f a = (‖a‖ : ℂ) := by
…

theorem OAI.NuclearUltrapower.contractive_unital_real line 70

Source documentation

A contractive unital functional is real on self-adjoint elements.

theorem contractive_unital_real (f : A →L[ℂ] ℂ) (hf : ‖f‖ ≤ 1) (h1 : f 1 = 1)
    (a : A) (ha : IsSelfAdjoint a) : (f a).im = 0 := by
…

theorem OAI.NuclearUltrapower.contractive_unital_positive line 119

Source documentation

The norm-one / unit-preserving criterion for positivity.

theorem contractive_unital_positive (f : A →L[ℂ] ℂ) (hf : ‖f‖ ≤ 1) (h1 : f 1 = 1)
    (a : A) (ha : 0 ≤ a) : 0 ≤ f a := by
…

theorem OAI.NuclearUltrapower.exists_norming_state line 133
Source documentation
Sufficiently many states, proved rather than assumed.
```
theorem exists_norming_state (a : A) (ha : 0 ≤ a) :
    ∃ f : A →ₚ[ℂ] ℂ, f 1 = 1 ∧ f a = (‖a‖ : ℂ) := by
…
```
theorem OAI.NuclearUltrapower.gns_unit_norm line 153
Source documentation
The GNS cyclic vector for a state has norm one.
```
theorem gns_unit_norm (f : A →ₚ[ℂ] ℂ) (h1 : f 1 = 1) :
    ‖(f.toPreGNS 1 : f.GNS)‖ = 1 := by
…
```
theorem OAI.NuclearUltrapower.exists_norming_gns line 160
Source documentation
Every C*-algebra element attains its norm in one of its GNS representations. This supplies norm-separation with no external faithful-representation axiom.
```
theorem exists_norming_gns (a : A) :
    ∃ f : A →ₚ[ℂ] ℂ, f 1 = 1 ∧ ‖f.gnsStarAlgHom a‖ = ‖a‖ := by
…
```

theorem OAI.NuclearUltrapower.norm_le_of_all_hilbert_representations line 179

Source documentation

Testing on all Hilbert space representations detects the original norm.

theorem norm_le_of_all_hilbert_representations (a : A) (M : ℝ)
    (h : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
      (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)), ‖ρ a‖ ≤ M) : ‖a‖ ≤ M := by
…

def OAI.NuclearUltrapower.hilbertDiagonal line 191

Source documentation

A uniformly bounded diagonal family acts on the Hilbert direct sum.

def hilbertDiagonal (T : ∀ i, E i →L[ℂ] E i) (M : ℝ) (hM : 0 ≤ M)
    (hT : ∀ i, ‖T i‖ ≤ M) : lp E 2 →L[ℂ] lp E 2 := by
…

theorem OAI.NuclearUltrapower.hilbertDiagonal_apply line 205
abbrev OAI.NuclearUltrapower.UniversalGNS line 211
Source documentation
Universal GNS Hilbert space, with all positive functionals as coordinates.
```
abbrev UniversalGNS (A : Type u) [CStarAlgebra A] :=
…
```
def OAI.NuclearUltrapower.universalGNS line 216
Source documentation
The faithful unital Hilbert representation obtained by summing the GNS representations of all positive functionals.
```
def universalGNS : A →⋆ₐ[ℂ] (UniversalGNS A →L[ℂ] UniversalGNS A) where
…
```
Mentions: OAI.NuclearUltrapower.UniversalGNS
theorem OAI.NuclearUltrapower.universalGNS_apply line 238
theorem OAI.NuclearUltrapower.universalGNS_injective line 241
theorem OAI.NuclearUltrapower.universalGNS_isometry line 256
Source documentation
The representation loses neither norm nor spectrum.
```
theorem universalGNS_isometry : Isometry (universalGNS (A := A)) :=
…
```
Mentions: OAI.NuclearUltrapower.universalGNS