DihedralFourier.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The exact dihedral word identity and the finite Fourier matrix entries.

theorem OAI.KadisonSimilarity.dihedral_word_identity line 18

Source documentation

The reflection relation fixes the sum-index in the Hankel term.

theorem dihedral_word_identity (w d : G) (hd : d * w = w⁻¹ * d) (j k : ℤ) :
    w ^ j * d * w ^ (-k) = w ^ (j + k + 1) * (w⁻¹ * d) := by
…

def OAI.KadisonSimilarity.dihedralHalfProjection line 38
Source documentation
The corner of a symmetry, written algebraically.
```
def dihedralHalfProjection (d : Rˣ) : R := (1 / 2 : ℂ) • (1 + (d : R))
```

theorem OAI.KadisonSimilarity.dihedral_corner_word line 41

Source documentation

Exact rotation-plus-reflection decomposition of the corner word.

theorem dihedral_corner_word (w d : Rˣ) (hd : d * w = w⁻¹ * d) (j k : ℤ) :
    (↑(w ^ j) : R) * dihedralHalfProjection d * (↑(w ^ (-k)) : R) =
      (1 / 2 : ℂ) • ((↑(w ^ (j - k)) : R) +
        (↑(w ^ (j + k + 1)) : R) * (↑(w⁻¹ * d) : R)) := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.dihedral_fourier_entry line 56

Source documentation

Once the two Fourier coefficient identities hold, the corner entry has both its Toeplitz difference index and its Hankel sum-plus-one index.

theorem dihedral_fourier_entry
    (w d : Rˣ) (hd : d * w = w⁻¹ * d) (f : R) (E : R →ₗ[ℂ] R)
    (γ : ℤ → ℂ)
    (hrot : ∀ l : ℤ, E (f * (↑(w ^ l) : R)) = γ l • (1 : R))
    (href : ∀ l : ℤ, E (f * (↑(w ^ l) : R) * (↑(w⁻¹ * d) : R)) =
      γ l • (↑(w⁻¹ * d) : R)) (j k : ℤ) :
    E (f * ((↑(w ^ j) : R) * dihedralHalfProjection d * (↑(w ^ (-k)) : R))) =
      (1 / 2 : ℂ) • (γ (j - k) • (1 : R) +
        γ (j + k + 1) • (↑(w⁻¹ * d) : R)) := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

def OAI.KadisonSimilarity.symmetryExpectation line 69
Source documentation
The trace-orthogonal projection onto the span of a centered symmetry.
```
def symmetryExpectation (τ : R →ₗ[ℂ] ℂ) (s : R) : R →ₗ[ℂ] R where
…
```
theorem OAI.KadisonSimilarity.symmetryExpectation_apply line 76

theorem OAI.KadisonSimilarity.symmetryExpectation_mul_symmetry line 80

Source documentation

The two coefficients of x and xs exchange when s²=1.

theorem symmetryExpectation_mul_symmetry
    (τ : R →ₗ[ℂ] ℂ) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (s x : R) (hs : s * s = 1) (hcoset : τ (s * x) = 0) :
    symmetryExpectation τ s x = τ x • 1 ∧
      symmetryExpectation τ s (x * s) = τ x • s := by
…

Mentions: OAI.KadisonSimilarity.symmetryExpectation

theorem OAI.KadisonSimilarity.dihedral_fourier_entry_from_moments line 94

Source documentation

Scalar group Fourier moments alone determine the finite compression entry. The coset moment vanishes by dihedral group orthogonality.

theorem dihedral_fourier_entry_from_moments
    (w d : Rˣ) (hd : d * w = w⁻¹ * d) (f : R)
    (τ : R →ₗ[ℂ] ℂ) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (hs : (↑(w⁻¹ * d) : R) * (↑(w⁻¹ * d) : R) = 1)
    (γ : ℤ → ℂ) (hcoef : ∀ l : ℤ, τ (f * (↑(w ^ l) : R)) = γ l)
    (hcoset : ∀ l : ℤ, τ ((↑(w⁻¹ * d) : R) * (f * (↑(w ^ l) : R))) = 0)
    (j k : ℤ) :
    symmetryExpectation τ (↑(w⁻¹ * d) : R)
        (f * ((↑(w ^ j) : R) * dihedralHalfProjection d * (↑(w ^ (-k)) : R))) =
      (1 / 2 : ℂ) • (γ (j - k) • (1 : R) +
        γ (j + k + 1) • (↑(w⁻¹ * d) : R)) := by
…

Mentions: OAI.KadisonSimilarity.symmetryExpectation, OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.compressed_dihedral_fourier_entry line 113

Source documentation

Bimodularity and the tower identity transfer the free-compression expectation to a dihedral Fourier entry.

theorem compressed_dihedral_fourier_entry
    (w d : Rˣ) (hd : d * w = w⁻¹ * d) (f h : R)
    (EC E₀ : R →ₗ[ℂ] R) (γ : ℤ → ℂ) (u : ℂ)
    (hEC : EC h = u ^ 2 • (f * dihedralHalfProjection d))
    (hbimod : ∀ j k : ℤ, EC ((↑(w ^ j) : R) * h * (↑(w ^ (-k)) : R)) =
      (↑(w ^ j) : R) * EC h * (↑(w ^ (-k)) : R))
    (htower : ∀ j k : ℤ,
      E₀ (EC ((↑((w) ^ j) : R) * h * (↑((w) ^ (-k)) : R))) =
        E₀ ((↑((w) ^ j) : R) * h * (↑((w) ^ (-k)) : R)))
    (hcomm : ∀ j : ℤ, (↑(w ^ j) : R) * f = f * (↑(w ^ j) : R))
    (hrot : ∀ l : ℤ, E₀ (f * (↑(w ^ l) : R)) = γ l • (1 : R))
    (href : ∀ l : ℤ, E₀ (f * (↑(w ^ l) : R) * (↑(w⁻¹ * d) : R)) =
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.normalized_corner_scalar line 140
Source documentation
The normalized corner coefficient is exactly u when u = 2t.
```
theorem normalized_corner_scalar (t : ℂ) (ht : t ≠ 0) :
    t⁻¹ * ((2 * t) ^ 2 / 2) = 2 * t := by field_simp
…
```