HaarCornerLetters.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Normalized Haar powers in a tracial corner. Their adjoints give the orthonormal first-letter sequence used in the propagation argument.

def OAI.KadisonSimilarity.haarCornerPower line 15
Source documentation
Integer powers are taken in the unital corner, whose identity is q.
```
def haarCornerPower (z : unitary (CStarCorner q hq)) (k : ℤ) : P :=
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.haarCornerPower_zero line 18
theorem OAI.KadisonSimilarity.haarCornerPower_mul line 22
theorem OAI.KadisonSimilarity.star_haarCornerPower line 28
theorem OAI.KadisonSimilarity.mul_haarCornerPower line 34
theorem OAI.KadisonSimilarity.haarCornerPower_mul_support line 38
def OAI.KadisonSimilarity.haarCornerCoefficient line 43
Source documentation
The coefficient a⁻¹ᐟ², embedded in the complex scalars.
```
def haarCornerCoefficient (a : ℝ) : ℂ := ((Real.sqrt a)⁻¹ : ℝ)
```
theorem OAI.KadisonSimilarity.star_haarCornerCoefficient line 45
theorem OAI.KadisonSimilarity.haarCornerCoefficient_sq line 49
def OAI.KadisonSimilarity.haarCornerLetter line 57
Source documentation
Positive Haar powers, normalized in the ambient tracial Hilbert norm.
```
def haarCornerLetter (z : unitary (CStarCorner q hq)) (a : ℝ) (n : ℕ) : P :=
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.support_mul_haarCornerLetter line 60
theorem OAI.KadisonSimilarity.haarCornerLetter_mul_support line 64
theorem OAI.KadisonSimilarity.star_haarCornerLetter line 68
theorem OAI.KadisonSimilarity.star_haarCornerLetter_mul_self line 73
theorem OAI.KadisonSimilarity.haarCornerLetter_mul_star_self line 80
def OAI.KadisonSimilarity.HaarCornerMoments line 91
Source documentation
Haar moments for the corner trace τ(·)/a; the zero moment is supplied by τ q = a in the following lemmas.
```
def HaarCornerMoments (a : ℝ) : Prop :=
…
```
theorem OAI.KadisonSimilarity.haarCornerPower_trace line 95
Source documentation
Normalized Haar moments give the unnormalized ambient trace formula.
```
theorem haarCornerPower_trace (ha : 0 < a) (htrace : τ q = (a : ℂ))
    (hhaar : HaarCornerMoments τ z a) (k : ℤ) :
    τ (haarCornerPower z k) = if k = 0 then (a : ℂ) else 0 := by
…
```
Mentions: OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.haarCornerPower
theorem OAI.KadisonSimilarity.haarCornerLetter_trace_zero line 106
theorem OAI.KadisonSimilarity.haarCornerLetter_mul_star_trace line 114
Source documentation
The opposite-order products of the normalized powers have delta trace. This order is the one appearing in the inner products of adjoint letters.
```
theorem haarCornerLetter_mul_star_trace (ha : 0 < a) (htrace : τ q = (a : ℂ))
    (hhaar : HaarCornerMoments τ z a) (i j : ℕ) :
    τ (haarCornerLetter z a i * star (haarCornerLetter z a j)) =
      if i = j then 1 else 0 := by
…
```
Mentions: OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.haarCornerLetter
theorem OAI.KadisonSimilarity.TracialCornerGeometry.haarCornerLetter_left_scale line 136
Source documentation
The algebraic Haar normalization gives the exact operator identity used to scale the fixed propagation error.
```
theorem haarCornerLetter_left_scale (G : TracialCornerGeometry P H)
    (z : unitary (CStarCorner q hq)) {a : ℝ} (ha : 0 ≤ a) (n : ℕ) :
    (G.left (haarCornerLetter z a n)).adjoint.comp (G.left (haarCornerLetter z a n)) =
      ((a⁻¹ : ℝ) : ℂ) • G.left q := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.haarCornerLetter
theorem OAI.KadisonSimilarity.TracialCornerGeometry.haarCornerLetter_adjoint_orthonormal line 146
Source documentation
The adjoint Haar letters form the actual orthonormal Hilbert sequence required by the vacuum-slice propagation argument.
```
theorem haarCornerLetter_adjoint_orthonormal (G : TracialCornerGeometry P H)
    (z : unitary (CStarCorner q hq)) {a : ℝ} (ha : 0 < a)
    (htrace : G.trace q = (a : ℂ)) (hhaar : HaarCornerMoments G.trace z a) :
    Orthonormal ℂ (fun n : ℕ => G.vector (star (haarCornerLetter z a n))) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.haarCornerLetter