SpectralArc.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The bounded Borel spectral calculus input, specialized to the centered arc of a Haar rotation in a finite dihedral von Neumann algebra. Blackadar, Operator Algebras, I.6.2.4 and I.6.2.8, supply the calculus and commutation; integration against its Haar spectral measure gives the stated moments.

The interface is local to the specified trace and algebra. Its intended application has the normal finite trace and the von Neumann algebra generated by the two symmetries. No existence assertion is made for an arbitrary C-star subalgebra or an arbitrary linear functional. The corner estimates below are proved from the spectral data, rather than included in the published input.

theorem OAI.KadisonSimilarity.isStarProjection_dihedralHalfProjection line 24
Source documentation
The half projection of a selfadjoint involution.
```
theorem isStarProjection_dihedralHalfProjection (d : Pˣ)
    (hd : star (d : P) = (d : P)) (hdd : d * d = 1) :
    IsStarProjection (dihedralHalfProjection d) := by
…
```
Mentions: OAI.KadisonSimilarity.dihedralHalfProjection
theorem OAI.KadisonSimilarity.trace_dihedralHalfProjection line 38
Source documentation
Centering the reflection fixes the trace of its half projection.
```
theorem trace_dihedralHalfProjection (τ : P →ₗ[ℂ] ℂ) (hτ : τ 1 = 1)
    (d : Pˣ) (hd : τ (d : P) = 0) : τ (dihedralHalfProjection d) = (1 / 2 : ℂ) := by
…
```
Mentions: OAI.KadisonSimilarity.dihedralHalfProjection
structure OAI.KadisonSimilarity.DihedralSpectralArc line 44
Source documentation
Exactly the spectral data of the centered arc used in the argument.
```
structure DihedralSpectralArc (τ : P →ₗ[ℂ] ℂ) (C : StarSubalgebra ℂ P)
    (w d : Pˣ) (θ : ℝ) where
…
```
def OAI.KadisonSimilarity.DihedralSpectralArcInput line 59
Source documentation
The local bounded Borel functional calculus specialization. In its application C is the dihedral von Neumann algebra and τ its normal trace.
```
def DihedralSpectralArcInput (τ : P →ₗ[ℂ] ℂ) (C : StarSubalgebra ℂ P)
    (w d : Pˣ) : Prop :=
…
```
theorem OAI.KadisonSimilarity.DihedralSpectralArc.trace_zero line 68
theorem OAI.KadisonSimilarity.DihedralSpectralArc.rotation_commutes line 72
theorem OAI.KadisonSimilarity.DihedralSpectralArc.shifted_reflection_moment line 78
Source documentation
The reflection used in the Hankel term is w⁻¹d, rather than d. Traciality shifts the Fourier index and supplies its zero mixed moment.
```
theorem shifted_reflection_moment (htr : ∀ x y, τ (x * y) = τ (y * x)) (l : ℤ) :
    τ ((↑(w⁻¹ * d) : P) * (F.element * (↑(w ^ l) : P))) = 0 := by
…
```
theorem OAI.KadisonSimilarity.DihedralSpectralArc.halfProjection_commutes line 94
def OAI.KadisonSimilarity.DihedralSpectralArc.corner line 102
Source documentation
The actual arc element in the normalized half corner.
```
def corner (hp : IsStarProjection (dihedralHalfProjection d)) :
    CStarCorner (dihedralHalfProjection d) hp :=
…
```
Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_coe line 110
theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_mem line 113
theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_selfAdjoint line 117
theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_norm_le line 125
theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_trace_zero line 131
theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_square line 138

theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_second_moment line 151

Source documentation

Normalization cancels the half-corner trace, leaving the arc variance.

theorem corner_second_moment (hp : IsStarProjection (dihedralHalfProjection d))
    (ht : τ (dihedralHalfProjection d) = (1 / 2 : ℂ)) :
    CStarCorner.normalizedTrace (dihedralHalfProjection d) hp τ
      (star (F.corner hp) * F.corner hp) = ((θ / Real.pi) * (1 - θ / Real.pi) : ℝ) := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.CStarCorner.normalizedTrace

theorem OAI.KadisonSimilarity.DihedralSpectralArc.corner_second_moment_le line 161

theorem OAI.KadisonSimilarity.DihedralSpectralArc.compressed_expectation line 172

Source documentation

The trace-pairing expectation of the actual compressed arc is derived from normalized corner freeness. The factor 2t is not an extra hypothesis.

theorem compressed_expectation
    (E : TracialExpectation τ C)
    (hfaithful : ∀ x, τ (star x * x) = 0 → x = 0)
    (htr : ∀ x y, τ (x * y) = τ (y * x))
    (hp : IsStarProjection (dihedralHalfProjection d))
    (hpC : dihedralHalfProjection d ∈ C)
    (D : StarSubalgebra ℂ P) (hpD : dihedralHalfProjection d ∈ D)
    (htp : τ (dihedralHalfProjection d) = (1 / 2 : ℂ))
    (hfree : ScalarFree (CStarCorner.normalizedTrace (dihedralHalfProjection d) hp τ)
      (CStarCorner.subalgebra (dihedralHalfProjection d) hp D hpD)
      (CStarCorner.subalgebra (dihedralHalfProjection d) hp C hpC))
    (e : CStarCorner (dihedralHalfProjection d) hp) (heD : (e : P) ∈ D)
…

Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CStarCorner.normalizedTrace, OAI.KadisonSimilarity.CStarCorner.subalgebra, OAI.KadisonSimilarity.CStarCorner