GraphRowClipping.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A common spectral cutoff for a replicated graph row

The cutoff acts on the left square of the entire row. Its norm is bounded independently of the number of columns, while its normalized graph error is controlled by the two fourth-moment sums in graphRowCost.

theorem OAI.KadisonKastler.graphRowSquare_nonneg line 28
def OAI.KadisonKastler.graphRowClipFactor line 34
Source documentation
The common positive left multiplier used to clip the entire row.
```
def graphRowClipFactor (β : ℝ) (Y : I → H →L[ℂ] H) : H →L[ℂ] H :=
…
```
def OAI.KadisonKastler.clippedGraphRow line 38
Source documentation
Spectral clipping of a rectangular row on its left square.
```
def clippedGraphRow (β : ℝ) (Y : I → H →L[ℂ] H) (i : I) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.graphRowClipFactor_selfadjoint line 41
theorem OAI.KadisonKastler.rowSquare_clip line 45
theorem OAI.KadisonKastler.norm_operatorRow_sq line 51
theorem OAI.KadisonKastler.norm_clippedGraphRow_le line 64
Source documentation
The whole clipped row has norm at most the cutoff.
```
theorem norm_clippedGraphRow_le {β : ℝ} (hβ : 0 < β) (Y : I → H →L[ℂ] H) :
    ‖operatorRow (clippedGraphRow β Y)‖ ≤ β := by
…
```
Mentions: OAI.KadisonKastler.operatorRow, OAI.KadisonKastler.clippedGraphRow
theorem OAI.KadisonKastler.clipping_remainder_sq_le line 83
theorem OAI.KadisonKastler.rowClip_remainder_sq_le line 97
theorem OAI.KadisonKastler.rowClip_remainder_sandwich_le line 120
theorem OAI.KadisonKastler.clippedGraphRow_graph_error_le line 137
Source documentation
The squared normalized rescaled-graph error of the single row cutoff is at most its moment cost divided by the cutoff squared.
```
theorem clippedGraphRow_graph_error_le {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) {β : ℝ} (hβ : 0 < β)
    (Y : Fin k → H →L[ℂ] H) :
    (𝔼 i, ‖rescaledGraphVector J Ω (Real.sqrt (k : ℝ))
      (Y i - clippedGraphRow β Y i)‖ ^ 2) ≤ graphRowCost Ω Y / β ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.clippedGraphRow, OAI.KadisonKastler.graphRowCost