TracialDihedralColumns.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Actual dihedral columns and reduced-word columns agree on the completed tracial base space. Their normalizations are derived from the trace; equality of the two realizations is needed only on bounded algebra vectors.

def OAI.KadisonSimilarity.symmetryUnit line 20
Source documentation
An involution, regarded as a unit with itself as inverse.
```
def symmetryUnit (s : P) (hsquare : s * s = 1) : Pˣ := ⟨s, s, hsquare, hsquare⟩
…
```
theorem OAI.KadisonSimilarity.symmetryUnit_coe line 23
theorem OAI.KadisonSimilarity.symmetryUnit_inv line 27
theorem OAI.KadisonSimilarity.symmetryUnit_star line 30
theorem OAI.KadisonSimilarity.dihedral_inverse_mul_reflection line 38
Source documentation
The reflected rotation appearing in the Hankel entry is the second involution itself.
```
theorem dihedral_inverse_mul_reflection (d s : Pˣ) (hs : s⁻¹ = s) :
    ((d * s)⁻¹ * d : Pˣ) = s := by
…
```
def OAI.KadisonSimilarity.projectionReflection line 44
Source documentation
The reflection associated to a projection, written without scalar coercions so that its algebraic identities apply in any star ring.
```
def projectionReflection (p : P) : P := p + p - 1
…
```
theorem OAI.KadisonSimilarity.projectionReflection_eq_two_mul line 47
theorem OAI.KadisonSimilarity.projectionReflection_star line 51
theorem OAI.KadisonSimilarity.projectionReflection_sq line 55
theorem OAI.KadisonSimilarity.trace_projectionReflection line 68
Source documentation
A half-trace projection gives a centered reflection.
```
theorem trace_projectionReflection (τ : P →ₗ[ℂ] ℂ) (hτ : τ 1 = 1)
    (p : P) (hp : τ p = (1 / 2 : ℂ)) : τ (projectionReflection p) = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.projectionReflection
theorem OAI.KadisonSimilarity.include_scaled_endpoint line 85
Source documentation
Endpoint normalization commutes with every continuous word inclusion.
```
theorem include_scaled_endpoint {n : ℕ}
    (L : HilbertTensor J (EndpointTensor E F n) →L[ℂ] H)
    (v : J) (e : E) (x : Fin n → F) (c : ℂ) :
    L (hilbertTensorInsert v (endpointWord (c • e) x)) =
      c • L (hilbertTensorInsert v (endpointWord e x)) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord
def OAI.KadisonSimilarity.TracialCornerGeometry.projectionEndpoint line 102
Source documentation
The normalized initial endpoint used by the dihedral word columns.
```
def projectionEndpoint (e : D) (t : ℝ) : G.baseSpace D :=
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_projectionVector line 106

Source documentation

A trace-t projection has Hilbert norm sqrt t.

theorem norm_projectionVector (e : D) (he : IsStarProjection e) {t : ℝ}
    (ht : 0 ≤ t) (hte : G.trace (e : P) = (t : ℂ)) :
    ‖G.baseVector D e‖ = Real.sqrt t := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_projectionEndpoint line 119

Source documentation

The actual normalized endpoint has norm one.

theorem norm_projectionEndpoint (e : D) (he : IsStarProjection e) {t : ℝ}
    (ht : 0 < t) (hte : G.trace (e : P) = (t : ℂ)) :
    ‖G.projectionEndpoint D e t‖ = 1 := by
…

def OAI.KadisonSimilarity.TracialCornerGeometry.projectionReflectionLetter line 133
Source documentation
The actual centered letter associated to a half-trace projection.
```
def projectionReflectionLetter : centeredSubspace (G.baseVector D 1) :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_projectionReflectionLetter line 140
Source documentation
Its Hilbert norm is one, by the reflection and normalized-trace identities.
```
theorem norm_projectionReflectionLetter :
    ‖G.projectionReflectionLetter D hτ p hhalf‖ = 1 :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseCompression_dihedral_reflection line 159
Source documentation
The Hankel coefficient's reflected-rotation compression is the actual restricted base symmetry. No independent compression operator is required.
```
theorem baseCompression_dihedral_reflection (dU : Pˣ) :
    G.baseCompression A (↑((dU * symmetryUnit (s : P)
      (congrArg (fun x : A => (x : P)) hssq))⁻¹ * dU) : P) =
      G.baseRepresentation A s := by
…
```
Mentions: OAI.KadisonSimilarity.symmetryUnit
def OAI.KadisonSimilarity.TracialCornerGeometry.tracialDihedralInclusion line 168
Source documentation
Actual dihedral word inclusion, with all base-space and compression data supplied by the ambient tracial representation.
```
def tracialDihedralInclusion (k : ℕ) : G.baseSpace A →ₗᵢ[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialDihedralInclusion_apply line 180

theorem OAI.KadisonSimilarity.TracialCornerGeometry.inner_tracialDihedralInclusion line 189

Source documentation

The dihedral columns are orthogonal on all completed base vectors.

theorem inner_tracialDihedralInclusion (k j : ℕ) (v w : G.baseSpace A) :
    inner ℂ
      (G.tracialDihedralInclusion D A hf hτ d s e hdstar hdsq hd0 hsstar hssq hs0 he ht hte k v)
      (G.tracialDihedralInclusion D A hf hτ d s e hdstar hdsq hd0 hsstar hssq hs0 he ht hte j w) =
      if k = j then inner ℂ v w else 0 := by
…

def OAI.KadisonSimilarity.TracialCornerGeometry.tracialDihedralColumns line 205
Source documentation
The actual finite dihedral column family on the tracial base.
```
def tracialDihedralColumns (N : ℕ) : Fin N → G.baseSpace A →L[ℂ] H := fun i =>
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_tracialDihedralColumns_le_one line 210
Source documentation
Orthogonality makes the assembled finite column a contraction.
```
theorem norm_tracialDihedralColumns_le_one (N : ℕ) :
    ‖sumColumns (G.tracialDihedralColumns D A hf hτ d s e hdstar hdsq hd0
      hsstar hssq hs0 he ht hte N)‖ ≤ 1 := by
…
```
Mentions: OAI.KadisonSimilarity.sumColumns
def OAI.KadisonSimilarity.TracialCornerGeometry.repeatedDihedralInclusion line 227
Source documentation
The repeated-word column at the actual normalized projection endpoint.
```
def repeatedDihedralInclusion (k : ℕ) : G.baseSpace A →ₗᵢ[ℂ] H :=
…
```