ClippedCoefficients.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Spectrally clipped coefficient columns

The actual cutoff preserves the coefficient-column bound, right support, and the relevant quotient image. The final theorem substitutes that cutoff directly into the coefficient drift estimate.

theorem OAI.KadisonKastler.sum_spectralClip_star_mul_le line 27
theorem OAI.KadisonKastler.sum_discarded_star_mul_le line 32
theorem OAI.KadisonKastler.spectralClip_star_column_le_one line 37
theorem OAI.KadisonKastler.discarded_star_column_le_one line 42
def OAI.KadisonKastler.coefficientMatrixMap line 55
Source documentation
Entrywise application of a unital star homomorphism to square matrices.
```
def coefficientMatrixMap (π : A →⋆ₐ[ℂ] B) :
    CStarMatrix n n A →⋆ₐ[ℂ] CStarMatrix n n B where
…
```
theorem OAI.KadisonKastler.coefficientMatrixMap_apply line 76
theorem OAI.KadisonKastler.norm_apply_le_of_star_mul_self_le line 91
Source documentation
Operator star-square domination is pointwise domination of norms.
```
theorem norm_apply_le_of_star_mul_self_le (X Y : H →L[ℂ] H)
    (hXY : star X * X ≤ star Y * Y) (z : H) : ‖X z‖ ≤ ‖Y z‖ := by
…
```

theorem OAI.KadisonKastler.column_contract_of_star_mul_self_le line 105

Source documentation

A pointwise star-square bound preserves any vector-column bound.

theorem column_contract_of_star_mul_self_le {ω : Type*} [Fintype ω]
    (K L : ω → H →L[ℂ] H) (hLK : ∀ w, star (L w) * L w ≤ star (K w) * K w)
    (hK : ∀ z : H, ‖WithLp.toLp 2 (fun w => K w z)‖ ≤ ‖z‖) (z : H) :
    ‖WithLp.toLp 2 (fun w => L w z)‖ ≤ ‖z‖ := by
…

theorem OAI.KadisonKastler.coefficient_hilbertMatrixHom_apply line 118
def OAI.KadisonKastler.clippedCoefficients line 127
theorem OAI.KadisonKastler.clippedCoefficients_norm line 131
theorem OAI.KadisonKastler.clippedCoefficients_support line 136
theorem OAI.KadisonKastler.clippedCoefficients_column_contract line 142
theorem OAI.KadisonKastler.discardedCoefficients_column_contract line 155

theorem OAI.KadisonKastler.spectralClip_entry_mem line 180

Source documentation

Applying the spectral cutoff preserves entrywise membership in the original von Neumann algebra.

theorem spectralClip_entry_mem (M : VonNeumannAlgebra H)
    (K : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H)) (hK : ∀ i j, K i j ∈ M)
    {β : ℝ} (hβ : 0 < β) (i j : Fin n) : spectralClip β K i j ∈ M := by
…

Mentions: OAI.KadisonKastler.spectralClip

theorem OAI.KadisonKastler.clippedCoefficients_entry_mem line 192
theorem OAI.KadisonKastler.clippedCoefficients_quotient_error line 198
theorem OAI.KadisonKastler.spectralClipped_matrixCommutator_drift_le_sixty_six line 208
Source documentation
The drift theorem applied to the actual spectral cutoff of the original coefficient family, with its column and support bounds proved above.
```
theorem spectralClipped_matrixCommutator_drift_le_sixty_six {ω : Type*} [Fintype ω]
    {q : ℕ} (M : VonNeumannAlgebra H)
    (hPublished : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.Algebra