ActualArcCompression.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The narrow-arc finite Fourier compression with actual normalized tracial dihedral word inclusions. Their formulas and orthogonality are proved.

theorem OAI.KadisonSimilarity.involution_unit_val_mul_self line 17
theorem OAI.KadisonSimilarity.involution_unit_val_star line 23
theorem OAI.KadisonSimilarity.dihedral_negative_nat_power line 27
theorem OAI.KadisonSimilarity.dihedral_reflection_relation line 33
theorem OAI.KadisonSimilarity.dihedralNormalization_sq line 38

theorem OAI.KadisonSimilarity.tracial_base_inner_of_compression line 47

Source documentation

The tracial inner-product formula on the base space follows from its unital compression representation.

theorem tracial_base_inner_of_compression (A : StarSubalgebra ℂ R)
    (τ : R →ₗ[ℂ] ℂ) (VA : A →ₗ[ℂ] K) (ρ : R →ₗ[ℂ] (K →L[ℂ] K))
    (hρ : ∀ (a b : A) x,
      inner ℂ (VA a) (ρ x (VA b)) = τ (star (a : R) * x * (b : R)))
    (hρone : ρ 1 = ContinuousLinearMap.id ℂ K) (a b : A) :
    inner ℂ (VA a) (VA b) = τ (star (a : R) * (b : R)) := by
…

def OAI.KadisonSimilarity.actualDihedralInclusion line 68
Source documentation
Actual normalized word inclusion for the unit convention of the Fourier calculation.
```
def actualDihedralInclusion (k : ℕ) : K →ₗᵢ[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.actualDihedralInclusion_apply line 75
theorem OAI.KadisonSimilarity.inner_actualDihedralInclusion line 83
def OAI.KadisonSimilarity.actualDihedralColumns line 96
Source documentation
The finite column of actual word inclusions.
```
def actualDihedralColumns (N : ℕ) : Fin N → K →L[ℂ] H := fun i =>
…
```
theorem OAI.KadisonSimilarity.norm_actualDihedralColumns_le_one line 101

theorem OAI.KadisonSimilarity.narrow_arc_actual_dihedral_compression line 121

Source documentation

The narrow-arc compression for the constructed normalized word maps. Neither their word formula nor their orthogonality is an input.

theorem narrow_arc_actual_dihedral_compression
    {N : ℕ} (hN : 0 < N)
    (L : R →ₗ[ℂ] (H →L[ℂ] H)) (hleft : ∀ a b, L a (V b) = V (a * b))
    (ρ : R →ₗ[ℂ] (K →L[ℂ] K))
    (hρ : ∀ (a b : A) x, inner ℂ (VA a) (ρ x (VA b)) = τ (star (a : R) * x * (b : R)))
    (hρone : ρ 1 = ContinuousLinearMap.id ℂ K)
    (E₀ EC : R →ₗ[ℂ] R) (htrace : ∀ x, τ (E₀ x) = τ x)
    (hbase : ∀ (a b : A) x, E₀ ((a : R) * x * (b : R)) = (a : R) * E₀ x * (b : R))
    (f h : R) (heh : e * h = h) (hhe : h * e = h)
    (hEC : EC h = (2 * (t : ℂ)) ^ 2 • (f * dihedralHalfProjection d))
    (hbimod : ∀ j k : ℤ, EC ((↑((d * s) ^ j) : R) * h * (↑((d * s) ^ (-k)) : R)) =
      (↑((d * s) ^ j) : R) * EC h * (↑((d * s) ^ (-k)) : R))
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection