DihedralArcProjection.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The concrete projection underlying the centered dihedral arc. Its Fourier moments are separate from the operator construction: the projection is the open spectral cut of the real part of the rotation at cos θ.

theorem OAI.KadisonSimilarity.upperSpectralCut_commutes line 20
Source documentation
Spectral cuts preserve every star commutation relation.
```
theorem upperSpectralCut_commutes (A T : H →L[ℂ] H) (t : ℝ)
    (h : Commute A T) (hs : Commute A (star T)) :
    Commute (upperSpectralCut A t) T := by
…
```
Mentions: OAI.KadisonSimilarity.upperSpectralCut

theorem OAI.KadisonSimilarity.norm_projection_sub_scalar_le_one line 29

Source documentation

Centering a projection by any scalar in [0,1] keeps norm at most one.

theorem norm_projection_sub_scalar_le_one (p : H →L[ℂ] H)
    (hp : IsStarProjection p) {r : ℝ} (hr : 0 ≤ r) (hr1 : r ≤ 1) :
    ‖p - r • 1‖ ≤ 1 := by
…

def OAI.KadisonSimilarity.dihedralArcProjection line 50
Source documentation
The open centered angular arc, expressed as a spectral cut of the real part.
```
def dihedralArcProjection (w : H →L[ℂ] H) (θ : ℝ) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.dihedralArcProjection_isStarProjection line 53
def OAI.KadisonSimilarity.centeredDihedralArc line 57
Source documentation
The actual centered operator used for the Haar arc.
```
def centeredDihedralArc (w : H →L[ℂ] H) (θ : ℝ) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.centeredDihedralArc_selfAdjoint line 60
theorem OAI.KadisonSimilarity.centeredDihedralArc_norm_le line 65
theorem OAI.KadisonSimilarity.dihedralArcProjection_mem line 71
theorem OAI.KadisonSimilarity.centeredDihedralArc_mem line 78
theorem OAI.KadisonSimilarity.realPart_commutes_rotation line 85
Source documentation
Normality makes the rotation commute with the real spectral variable.
```
theorem realPart_commutes_rotation (w : H →L[ℂ] H)
    (hw : Commute w (star w)) : Commute (realPart w : H →L[ℂ] H) w := by
…
```

theorem OAI.KadisonSimilarity.realPart_commutes_reflection line 91

Source documentation

Reflection interchanges the two summands of the real spectral variable.

theorem realPart_commutes_reflection (w d : H →L[ℂ] H)
    (hd : d * d = 1) (h : d * w = star w * d) :
    Commute (realPart w : H →L[ℂ] H) d := by
…

theorem OAI.KadisonSimilarity.centeredDihedralArc_commutes_rotation line 105
theorem OAI.KadisonSimilarity.centeredDihedralArc_commutes_reflection line 113

theorem OAI.KadisonSimilarity.centeredProjection_second_moment line 125

Source documentation

Once the projection's trace is known, its centered second moment is forced algebraically; no separate spectral calculation is necessary.

theorem centeredProjection_second_moment (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ)
    (p : H →L[ℂ] H) (hp : p * p = p) (r : ℂ)
    (hτ : τ 1 = 1) (ht : τ p = r) :
    τ ((p - r • 1) * (p - r • 1)) = r * (1 - r) := by
…

theorem OAI.KadisonSimilarity.centeredProjection_square_reflection line 135

Source documentation

Vanishing of the reflection-coset moments also controls the square.

theorem centeredProjection_square_reflection (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ)
    (p d : H →L[ℂ] H) (hp : p * p = p) (r : ℂ)
    (hτd : τ d = 0) (hτpd : τ (p * d) = 0) :
    τ (((p - r • 1) * (p - r • 1)) * d) = 0 := by
…