CyclicColumnTests.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Dense cyclic orbits give the bounded column tests needed for the matrix derivation estimate. The unit vector may vary with the test.

def OAI.KadisonSimilarity.cyclicOrbitColumn line 19
theorem OAI.KadisonSimilarity.cyclicOrbitColumn_apply line 24
theorem OAI.KadisonSimilarity.norm_cyclicColumnRoot_action line 28
Source documentation
A finite orbit column and its positive square root have the same vector norm.
```
theorem norm_cyclicColumnRoot_action (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
    {n : ℕ} (a : Fin n → A) :
    ‖σ (cyclicColumnRoot a) Ω‖ = ‖cyclicOrbitColumn σ Ω a‖ := by
…
```
Mentions: OAI.KadisonSimilarity.cyclicColumnRoot, OAI.KadisonSimilarity.cyclicOrbitColumn
def OAI.KadisonSimilarity.cyclicShiftVector line 53
Source documentation
The shifted square root is the single input vector for the regularized column.
```
def cyclicShiftVector (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
    {n : ℕ} (a : Fin n → A) (ε : ℝ) : K :=
…
```
theorem OAI.KadisonSimilarity.cyclicShiftVector_norm_le line 57
theorem OAI.KadisonSimilarity.cyclicPolarColumn_action_recover line 69
theorem OAI.KadisonSimilarity.cyclicOrbitColumn_dense line 81
Source documentation
Cyclicity supplies simultaneous approximation in every finite Hilbert sum.
```
theorem cyclicOrbitColumn_dense (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
    (hΩ : DenseRange (fun a : A => σ a Ω)) (n : ℕ) :
    DenseRange (cyclicOrbitColumn (n := n) σ Ω) := by
…
```
Mentions: OAI.KadisonSimilarity.cyclicOrbitColumn
def OAI.KadisonSimilarity.CyclicColumnTests line 90
Source documentation
The approximation needed by the matrix estimate; the input vector may vary.
```
def CyclicColumnTests (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) : Prop :=
…
```
theorem OAI.KadisonSimilarity.cyclicColumnTests_of_dense_orbit line 96
Source documentation
A dense cyclic orbit gives all the required bounded column tests.
```
theorem cyclicColumnTests_of_dense_orbit (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
    (hΩ : DenseRange (fun a : A => σ a Ω)) : CyclicColumnTests σ := by
…
```
Mentions: OAI.KadisonSimilarity.CyclicColumnTests

theorem OAI.KadisonSimilarity.rectangularDerivation_bound_of_cyclicColumnTests line 162

Source documentation

Bounded cyclic column tests suffice for the full matrix estimate.

theorem rectangularDerivation_bound_of_cyclicColumnTests
    {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    {c : ℝ} (hc : 0 ≤ c) (hcol : ColumnBound δ c)
    (htests : CyclicColumnTests σ) (n : ℕ) (X : Matrix (Fin n) (Fin n) A) :
    ‖rectangularMatrixOperator (X.map δ)‖ ≤ (4 * c) * ‖CStarMatrix.ofMatrix X‖ := by
…

Mentions: OAI.KadisonSimilarity.ColumnBound, OAI.KadisonSimilarity.CyclicColumnTests, OAI.KadisonSimilarity.rectangularMatrixOperator

theorem OAI.KadisonSimilarity.cyclic_derivation_implementation_of_column_tests line 191

Source documentation

A cyclic representation supplies the completely bounded derivation estimate directly.

theorem cyclic_derivation_implementation_of_column_tests
    {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    (htests : CyclicColumnTests σ)
    (paulsen : PaulsenSimilarityInput (normalizedRectangularRepresentation ρ σ δ hδ)) :
    ∃ V : K →L[ℂ] F, (∀ a, δ a = V.comp (σ a) - (ρ a).comp V) ∧
      ‖V‖ ≤ (1 + 4 * (4 * Real.sqrt 2)) ^ 2 * ‖δ‖ := by
…

Mentions: OAI.KadisonSimilarity.CyclicColumnTests, OAI.KadisonSimilarity.PaulsenSimilarityInput, OAI.KadisonSimilarity.normalizedRectangularRepresentation

theorem OAI.KadisonSimilarity.exists_corner_intertwiner_of_column_tests line 221

Source documentation

The corner correction needs only the direct cyclic column tests.

theorem exists_corner_intertwiner_of_column_tests
    {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (G : K →L[ℂ] F) {ε : ℝ} (hG : ‖cornerCommutator ρ σ G‖ ≤ ε)
    (htests : CyclicColumnTests σ)
    (paulsen : PaulsenSimilarityInput (normalizedRectangularRepresentation ρ σ
      (cornerCommutator ρ σ G) (cornerCommutator_leibniz ρ σ G))) :
    ∃ T : K →L[ℂ] F, (∀ a, T.comp (σ a) = (ρ a).comp T) ∧
      ‖G - T‖ ≤ (1 + 4 * (4 * Real.sqrt 2)) ^ 2 * ε := by
…

Mentions: OAI.KadisonSimilarity.cornerCommutator, OAI.KadisonSimilarity.CyclicColumnTests, OAI.KadisonSimilarity.PaulsenSimilarityInput, OAI.KadisonSimilarity.normalizedRectangularRepresentation, OAI.KadisonSimilarity.cornerCommutator_leibniz