DihedralPositiveDensity.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The centered dihedral corner is generated in L² by the positive compressed rotation powers. Apply the bounded centered corner map to the ordinary rotation/reflection word span; no bounded approximation theorem or corner-freeness hypothesis is needed.

theorem OAI.KadisonSimilarity.halfProjection_absorbs_reflection line 18

Source documentation

Both sides of the half projection absorb its reflection.

theorem halfProjection_absorbs_reflection (d : Pˣ) (hd : d * d = 1) :
    dihedralHalfProjection d * (d : P) = dihedralHalfProjection d ∧
      (d : P) * dihedralHalfProjection d = dihedralHalfProjection d := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.halfProjection_compressed_neg line 32

Source documentation

Reflection conjugation makes opposite rotation powers equal after compression to the half projection.

theorem halfProjection_compressed_neg (d w : Pˣ) (hd : d * d = 1)
    (hconj : d * w = w⁻¹ * d) (l : ℤ) :
    dihedralHalfProjection d * (↑(w ^ (-l)) : P) * dihedralHalfProjection d =
      dihedralHalfProjection d * (↑(w ^ l) : P) * dihedralHalfProjection d := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.halfProjection_compressed_natAbs line 51

Source documentation

Every compressed nonzero integer power is a positive compressed power.

theorem halfProjection_compressed_natAbs (d w : Pˣ) (hd : d * d = 1)
    (hconj : d * w = w⁻¹ * d) (l : ℤ) :
    dihedralHalfProjection d * (↑(w ^ l) : P) * dihedralHalfProjection d =
      dihedralHalfProjection d * (w : P) ^ l.natAbs * dihedralHalfProjection d := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.halfProjection_compressed_coset line 65

Source documentation

Reflection-coset words have the same corner compression as rotations.

theorem halfProjection_compressed_coset (d w : Pˣ) (hd : d * d = 1) (l : ℤ) :
    dihedralHalfProjection d * ((↑(w ^ l) : P) * (d : P)) * dihedralHalfProjection d =
      dihedralHalfProjection d * (↑(w ^ l) : P) * dihedralHalfProjection d := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

def OAI.KadisonSimilarity.TracialCornerGeometry.centeredCornerProjection line 80
Source documentation
The bounded map that compresses to the corner and removes its scalar part.
```
def centeredCornerProjection (p : P) : H →L[ℂ] H :=
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.centeredCornerProjection_vector line 84

Source documentation

Its value on algebra vectors is the centered corner compression.

theorem centeredCornerProjection_vector (p : P) (hp : IsStarProjection p) (x : P) :
    G.centeredCornerProjection p (G.vector x) =
      G.vector (p * x * p) - ((G.trace p)⁻¹ * G.trace (p * x)) • G.vector p := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.centeredCornerProjection_fixed line 92
Source documentation
Every centered corner vector is fixed by the bounded centered compression.
```
theorem centeredCornerProjection_fixed (p : P) (hp : IsStarProjection p)
    (x : CStarCorner p hp) (hx : G.trace (x : P) = 0) :
    G.centeredCornerProjection p (G.vector (x : P)) = G.vector (x : P) := by
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.TracialCornerGeometry.centeredCornerProjection_one line 99
Source documentation
The identity contributes only the scalar part of the corner.
```
theorem centeredCornerProjection_one (p : P) (hp : IsStarProjection p)
    (ht : G.trace p ≠ 0) :
    G.centeredCornerProjection p (G.vector 1) = 0 := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.dihedralGroupWordVectors line 106
Source documentation
All ordinary dihedral rotation and reflection-coset vectors.
```
def dihedralGroupWordVectors (d w : Pˣ) : Set H :=
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_halfProjection_rotation line 112

Source documentation

The normalized Haar and coset moments kill the scalar coefficient of every nonidentity compressed rotation.

theorem trace_halfProjection_rotation (d w : Pˣ)
    (hhaar : ∀ l : ℤ, G.trace (↑(w ^ l) : P) = if l = 0 then 1 else 0)
    (hcoset : ∀ l : ℤ, G.trace ((↑(w ^ l) : P) * (d : P)) = 0)
    (l : ℤ) (hl : l ≠ 0) :
    G.trace (dihedralHalfProjection d * (↑(w ^ l) : P)) = 0 := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_halfProjection_coset line 122
Source documentation
Reflection does not change the trace coefficient in the corner.
```
theorem trace_halfProjection_coset (d w : Pˣ) (hd : d * d = 1) (l : ℤ) :
    G.trace (dihedralHalfProjection d * ((↑(w ^ l) : P) * (d : P))) =
      G.trace (dihedralHalfProjection d * (↑(w ^ l) : P)) := by
…
```
Mentions: OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.TracialCornerGeometry.centeredCornerProjection_group_word_mem line 130

Source documentation

Centered compression sends every group word into the closed span of positive compressed rotation powers.

theorem centeredCornerProjection_group_word_mem
    (d w : Pˣ) (hd : d * d = 1) (hconj : d * w = w⁻¹ * d)
    (hp : IsStarProjection (dihedralHalfProjection d))
    (ht : G.trace (dihedralHalfProjection d) ≠ 0)
    (hhaar : ∀ l : ℤ, G.trace (↑(w ^ l) : P) = if l = 0 then 1 else 0)
    (hcoset : ∀ l : ℤ, G.trace ((↑(w ^ l) : P) * (d : P)) = 0)
    {z : H} (hz : z ∈ G.dihedralGroupWordVectors d w) :
    G.centeredCornerProjection (dihedralHalfProjection d) z ∈
      (Submodule.span ℂ (G.vector '' DihedralCornerWords.positiveCornerPowers
        (dihedralHalfProjection d) (w : P))).topologicalClosure := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.DihedralCornerWords.positiveCornerPowers

theorem OAI.KadisonSimilarity.TracialCornerGeometry.positive_corner_density_of_group_word_density line 171

Source documentation

Applying the centered corner map to the raw group-word L²-span gives the desired positive-power density for each centered corner vector.

theorem positive_corner_density_of_group_word_density
    (d w : Pˣ) (hd : d * d = 1) (hconj : d * w = w⁻¹ * d)
    (hp : IsStarProjection (dihedralHalfProjection d))
    (ht : G.trace (dihedralHalfProjection d) ≠ 0)
    (hhaar : ∀ l : ℤ, G.trace (↑(w ^ l) : P) = if l = 0 then 1 else 0)
    (hcoset : ∀ l : ℤ, G.trace ((↑(w ^ l) : P) * (d : P)) = 0)
    (x : CStarCorner (dihedralHalfProjection d) hp) (hx : G.trace (x : P) = 0)
    (hspan : G.vector (x : P) ∈
      (Submodule.span ℂ (G.dihedralGroupWordVectors d w)).topologicalClosure) :
    G.vector (x : P) ∈
      (Submodule.span ℂ (G.vector '' DihedralCornerWords.positiveCornerPowers
        (dihedralHalfProjection d) (w : P))).topologicalClosure := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.DihedralCornerWords.positiveCornerPowers

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_symmetry_rotation_conjugation line 201
Source documentation
For two involutions, the first one reverses their product.
```
theorem free_symmetry_rotation_conjugation (d s : Pˣ)
    (hdi : d⁻¹ = d) (hsi : s⁻¹ = s) : d * (d * s) = (d * s)⁻¹ * d := by
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_symmetry_first_coset_moments line 211

Source documentation

The reflection-coset moments used by the centered corner map follow from the scalar-freeness moments.

theorem free_symmetry_first_coset_moments
    (D A : StarSubalgebra ℂ P) (hf : ScalarFree G.trace D A)
    (d s : Pˣ) (hd : (d : P) ∈ D) (hs : (s : P) ∈ A)
    (hd0 : G.trace (d : P) = 0) (hs0 : G.trace (s : P) = 0)
    (hdi : d⁻¹ = d) (hsi : s⁻¹ = s) (l : ℤ) :
    G.trace ((↑((d * s) ^ l) : P) * (d : P)) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.TracialCornerGeometry.scalarFree_corner_of_dihedral_word_density line 227

Source documentation

The full normalized-corner freeness theorem requires only the raw L²-span of the dihedral group words, in addition to the original free factors.

theorem scalarFree_corner_of_dihedral_word_density
    (D A C : StarSubalgebra ℂ P) (hf : ScalarFree G.trace D A) (hτ : G.trace 1 = 1)
    (d s : Pˣ) (hd : (d : P) ∈ D) (hs : (s : P) ∈ A)
    (hd0 : G.trace (d : P) = 0) (hs0 : G.trace (s : P) = 0)
    (hdi : d⁻¹ = d) (hsi : s⁻¹ = s)
    (hp : IsStarProjection (dihedralHalfProjection d))
    (hpC : dihedralHalfProjection d ∈ C)
    (hspan : ∀ x : CStarCorner (dihedralHalfProjection d) hp, (x : P) ∈ C →
      G.vector (x : P) ∈
        (Submodule.span ℂ (G.dihedralGroupWordVectors d (d * s))).topologicalClosure) :
    ScalarFree (CStarCorner.normalizedTrace (dihedralHalfProjection d) hp G.trace)
      (CStarCorner.subalgebra (dihedralHalfProjection d) hp D
…

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