CyclicColumnPolar.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Contractive regularized polar columns inside the source algebra. These columns will supply dense cyclic vector tests with a varying unit vector.

theorem OAI.KadisonSimilarity.norm_column_le_of_starSquare line 16

Source documentation

A column is contractive when its positive column square is contractive.

theorem norm_column_le_of_starSquare {n : ℕ} (a : Fin n → A)
    (ha : ‖∑ i, star (a i) * a i‖ ≤ 1) :
    ‖CStarMatrix.ofMatrix (fun i (_ : Fin 1) => a i)‖ ≤ 1 := by
…

def OAI.KadisonSimilarity.cyclicColumnRoot line 47
Source documentation
The positive square root of a finite column square.
```
def cyclicColumnRoot {n : ℕ} (a : Fin n → A) : A :=
…
```
theorem OAI.KadisonSimilarity.cyclicColumnRoot_nonneg line 50
theorem OAI.KadisonSimilarity.cyclicColumnRoot_sq line 53
def OAI.KadisonSimilarity.cyclicPolarColumn line 58
Source documentation
The regularized polar column stays in the original algebra.
```
def cyclicPolarColumn {n : ℕ} (a : Fin n → A) (ε : ℝ) : Matrix (Fin n) (Fin 1) A :=
…
```
theorem OAI.KadisonSimilarity.cyclicPolarColumn_contract line 61
theorem OAI.KadisonSimilarity.cyclicPolarColumn_recover line 82
Source documentation
Multiplication by the shifted root recovers every original column entry.
```
theorem cyclicPolarColumn_recover {n : ℕ} (a : Fin n → A) {ε : ℝ} (hε : 0 < ε)
    (i : Fin n) : cyclicPolarColumn a ε i 0 * (cyclicColumnRoot a + ε • (1 : A)) = a i := by
…
```
Mentions: OAI.KadisonSimilarity.cyclicPolarColumn, OAI.KadisonSimilarity.cyclicColumnRoot