DihedralWordIsometries.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Normalized dihedral word inclusions on actual tracial Hilbert spaces.

def OAI.KadisonSimilarity.dihedralWordMap line 16

Source documentation

The unnormalized algebraic word inclusion.

def dihedralWordMap (Q : StarSubalgebra ℂ R) (V : R →ₗ[ℂ] E) (e d s : R)
    (k : ℕ) : Q →ₗ[ℂ] E where
…

theorem OAI.KadisonSimilarity.inner_dihedralWordMap line 40
Source documentation
The projection and selfadjointness hypotheses turn the tracial sandwich formula into the actual Hilbert inner products of the word maps.
```
theorem inner_dihedralWordMap (k j : ℕ) (a b : Q) :
    inner ℂ (dihedralWordMap Q V e d s k a) (dihedralWordMap Q V e d s j b) =
      if k = j then τ e * τ (star (a : R) * (b : R)) else 0 := by
…
```
Mentions: OAI.KadisonSimilarity.dihedralWordMap
def OAI.KadisonSimilarity.dihedralNormalization line 57
Source documentation
The actual normalization factor t⁻¹ᐟ².
```
def dihedralNormalization (t : ℝ) : ℂ := ((Real.sqrt t)⁻¹ : ℝ)
```
theorem OAI.KadisonSimilarity.dihedralNormalization_identity line 59
def OAI.KadisonSimilarity.normalizedDihedralWordMap line 75
Source documentation
The normalized algebraic word map whose Hilbert extension is isometric.
```
def normalizedDihedralWordMap (t : ℝ) (k : ℕ) : Q →ₗ[ℂ] E :=
…
```
theorem OAI.KadisonSimilarity.inner_normalizedDihedralWordMap line 84
theorem OAI.KadisonSimilarity.norm_normalizedDihedralWordMap line 105
def OAI.KadisonSimilarity.dihedralWordIsometry line 116
Source documentation
Isometric inclusion of the completed tracial base space as the k-th actual dihedral word space.
```
def dihedralWordIsometry (hdense : DenseRange VA) (k : ℕ) : K →ₗᵢ[ℂ] E :=
…
```
theorem OAI.KadisonSimilarity.dihedralWordIsometry_apply line 121

theorem OAI.KadisonSimilarity.inner_dihedralWordIsometry line 131

Source documentation

Distinct actual dihedral word inclusions have orthogonal ranges on the completed tracial Hilbert space.

theorem inner_dihedralWordIsometry (hdense : DenseRange VA) (k j : ℕ) (x y : K) :
    inner ℂ
      (dihedralWordIsometry τ hτ htr V hinner P Q hf d s e hd hs he hd0 hs0 hdd hss
        hdstar hsstar hestar hee VA hA t ht hte hdense k x)
      (dihedralWordIsometry τ hτ htr V hinner P Q hf d s e hd hs he hd0 hs0 hdd hss
        hdstar hsstar hestar hee VA hA t ht hte hdense j y) =
      if k = j then inner ℂ x y else 0 := by
…

Mentions: OAI.KadisonSimilarity.dihedralWordIsometry