WordPrefixRealization.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The fixed alternating prefixes in propagation are isometries on the appropriate reduced-word subspace. This follows by iterating the two one-letter Fock creation formulas. Their global operator bounds follow from the algebraic symmetry and normalized corner-unitary relations.

structure OAI.KadisonSimilarity.AlternatingCreationCoordinates line 24
Source documentation
The two elementary creation formulas for reduced words starting in the opposite free factor. The tensor maps are the usual isometric inclusions of reduced-word summands, and the specified letters have Hilbert norm one.
```
structure AlternatingCreationCoordinates (EA ED : Type*)
    [NormedAddCommGroup EA] [InnerProductSpace ℂ EA]
    [NormedAddCommGroup ED] [InnerProductSpace ℂ ED]
    (S : H →L[ℂ] H) (X : ℕ → H →L[ℂ] H) (DLead : Submodule ℂ H) where
…
```
theorem OAI.KadisonSimilarity.AlternatingCreationCoordinates.actionA_isometry line 46
Source documentation
The first elementary creation step has norm one and the expected range.
```
theorem actionA_isometry (y : H) (hy : y ∈ DLead) :
    S y ∈ C.ALead ∧ ‖S y‖ = ‖y‖ := by
…
```
theorem OAI.KadisonSimilarity.AlternatingCreationCoordinates.actionD_isometry line 57
Source documentation
The second elementary creation step has norm one and returns to the subspace of words starting in the other free factor.
```
theorem actionD_isometry (n : ℕ) (y : H) (hy : y ∈ C.ALead) :
    X n y ∈ DLead ∧ ‖X n y‖ = ‖y‖ := by
…
```
theorem OAI.KadisonSimilarity.AlternatingCreationCoordinates.prefix_isometry line 68
Source documentation
Iterating the elementary formulas proves the fixed alternating-prefix isometry; no bound on a complete prefix is assumed.
```
theorem prefix_isometry (m n : ℕ) (y : H) (hy : y ∈ DLead) :
    ((S * X n) ^ m * S) y ∈ C.ALead ∧
      ‖((S * X n) ^ m * S) y‖ = ‖y‖ := by
…
```
theorem OAI.KadisonSimilarity.norm_unitary_le_one line 89
Source documentation
A unitary has norm at most one, including in the zero C-star algebra.
```
theorem norm_unitary_le_one (u : unitary P) : ‖(u : P)‖ ≤ 1 := by
…
```
theorem OAI.KadisonSimilarity.norm_haarCornerLetter_le line 97
Source documentation
The algebra norm of every corner Haar letter is bounded uniformly in its frequency, using only its normalization and corner unitarity.
```
theorem norm_haarCornerLetter_le {q : P} {hq : IsStarProjection q}
    (z : unitary (CStarCorner q hq)) (a : ℝ) (n : ℕ) :
    ‖haarCornerLetter z a n‖ ≤ (Real.sqrt a)⁻¹ := by
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.haarCornerLetter
theorem OAI.KadisonSimilarity.norm_symmetry_le_one line 111
Source documentation
A selfadjoint involution is contractive without a nontriviality assumption on its C-star algebra.
```
theorem norm_symmetry_le_one (s : P) (hstar : star s = s) (hsq : s * s = 1) :
    ‖s‖ ≤ 1 :=
…
```
def OAI.KadisonSimilarity.tracialWordPrefix line 134
Source documentation
The degree-m + 1 alternating algebra prefix.
```
def tracialWordPrefix (m n : ℕ) : P :=
…
```
theorem OAI.KadisonSimilarity.tracialWordPrefix_isometry line 140
Source documentation
The left multiplier of the actual algebra prefix is isometric on the nonvacuum head subspace, by the elementary Fock creation identities.
```
theorem tracialWordPrefix_isometry
    (C : AlternatingCreationCoordinates EA ED (G.left s)
      (fun n => G.left (ι (haarCornerLetter z a n))) W.vacuumᗮ)
    (m n : ℕ) (y : H) (hy : y ∈ W.vacuumᗮ) :
    ‖G.left (tracialWordPrefix (ι := ι) z a s m n) y‖ = ‖y‖ := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCreationCoordinates, OAI.KadisonSimilarity.haarCornerLetter, OAI.KadisonSimilarity.tracialWordPrefix
theorem OAI.KadisonSimilarity.norm_tracialWordPrefix_le line 150
Source documentation
The complete prefix has a uniform bound for each fixed degree. Only the algebraic unitary relations enter this global estimate.
```
theorem norm_tracialWordPrefix_le (hstar : star s = s) (hsq : s * s = 1)
    (m n : ℕ) :
    ‖G.left (tracialWordPrefix (ι := ι) z a s m n)‖ ≤ ((Real.sqrt a)⁻¹) ^ m := by
…
```
Mentions: OAI.KadisonSimilarity.tracialWordPrefix

def OAI.KadisonSimilarity.tracialRepeatedWordRealizationOfCreation line 181

Source documentation

Construct the propagation realization from elementary reduced-word creation and multiplication. Both complete-prefix fields are conclusions.

def tracialRepeatedWordRealizationOfCreation
    (hstar : star s = s) (hsq : s * s = 1)
    (C : AlternatingCreationCoordinates EA ED (G.left s)
      (fun n => G.left (ι (haarCornerLetter z a n))) W.vacuumᗮ)
    (m : ℕ) (Y : H →L[ℂ] H) (B₀ : B →L[ℂ] B) (Bₖ : V →L[ℂ] V)
    (repeatVector : B →ₗᵢ[ℂ] V) (word : ℕ → V →ₗᵢ[ℂ] H)
    (small : B →L[ℂ] H)
    (hsmall : ∀ v, ‖small v‖ = Real.sqrt a * ‖v‖)
    (hzero : ∀ v, Y (small v) = small (B₀ v))
    (hlevel : ∀ n v, Y (word n (repeatVector v)) = word n (Bₖ (repeatVector v)))
    (hsupport : ∀ v, G.left (ι q) (small v) = small v)
    (hword : ∀ n v, word n (repeatVector v) =
…

Mentions: OAI.KadisonSimilarity.AlternatingCreationCoordinates, OAI.KadisonSimilarity.haarCornerLetter