GraphClipping.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Spectral clipping of a rescaled graph vector

The positive vector state can be applied to the two C*-order tail bounds. Adjoint compatibility gives the same cutoff on both graph coordinates. No traciality of the vector state is used.

theorem OAI.KadisonKastler.realVectorState_mono line 29
Source documentation
A positive vector functional is monotone in the C*-order.
```
theorem realVectorState_mono (Ω : H) {x y : H →L[ℂ] H} (hxy : x ≤ y) :
    realVectorState Ω x ≤ realVectorState Ω y := by
…
```
Mentions: OAI.KadisonKastler.realVectorState
theorem OAI.KadisonKastler.vectorState_spectralClip_right_le line 39
Source documentation
Right vector-state variance decreases under clipping.
```
theorem vectorState_spectralClip_right_le (Ω : H) {β : ℝ} (hβ : 0 < β)
    (x : H →L[ℂ] H) :
    ‖spectralClip β x Ω‖ ^ 2 ≤ ‖x Ω‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.vectorState_spectralClip_left_le line 46
Source documentation
The adjoint coordinate has the same variance decrease.
```
theorem vectorState_spectralClip_left_le (Ω : H) {β : ℝ} (hβ : 0 < β)
    (x : H →L[ℂ] H) :
    ‖star (spectralClip β x) Ω‖ ^ 2 ≤ ‖star x Ω‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.norm_rescaledGraph_spectralClip_sq_le_cost line 53
Source documentation
The clipped graph remains bounded by the sampled second and fourth moment cost.
```
theorem norm_rescaledGraph_spectralClip_sq_le_cost
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ) {β : ℝ} (hβ : 0 < β)
    (x : H →L[ℂ] H) :
    ‖rescaledGraphVector J Ω c (spectralClip β x)‖ ^ 2 ≤
      graphMomentCost Ω (c ^ 2) x := by
…
```
Mentions: OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.spectralClip, OAI.KadisonKastler.graphMomentCost
theorem OAI.KadisonKastler.vectorState_spectralClip_discard_right_le line 81
Source documentation
The right-coordinate clipping tail is controlled by the actual fourth moment of the original vector state.
```
theorem vectorState_spectralClip_discard_right_le (Ω : H) {β : ℝ} (hβ : 0 < β)
    (x : H →L[ℂ] H) :
    ‖(x - spectralClip β x) Ω‖ ^ 2 ≤
      realVectorState Ω ((star x * x) ^ 2) / β ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.spectralClip, OAI.KadisonKastler.realVectorState
theorem OAI.KadisonKastler.vectorState_spectralClip_discard_left_le line 90
Source documentation
The same tail estimate holds on the adjoint coordinate.
```
theorem vectorState_spectralClip_discard_left_le (Ω : H) {β : ℝ} (hβ : 0 < β)
    (x : H →L[ℂ] H) :
    ‖star (x - spectralClip β x) Ω‖ ^ 2 ≤
      realVectorState Ω ((x * star x) ^ 2) / β ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.spectralClip, OAI.KadisonKastler.realVectorState

theorem OAI.KadisonKastler.norm_rescaledGraph_spectralClip_discard_sq_le line 98

Source documentation

The weighted graph tail is controlled uniformly in the rescaling.

theorem norm_rescaledGraph_spectralClip_discard_sq_le
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ) {β : ℝ} (hβ : 0 < β)
    (x : H →L[ℂ] H) :
    ‖rescaledGraphVector J Ω c (x - spectralClip β x)‖ ^ 2 ≤
      (realVectorState Ω ((star x * x) ^ 2) +
        c ^ 2 * realVectorState Ω ((x * star x) ^ 2)) / β ^ 2 := by
…

Mentions: OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.spectralClip, OAI.KadisonKastler.realVectorState

theorem OAI.KadisonKastler.norm_rescaledGraph_spectralClip_discard_sq_le_cost line 111

Source documentation

The full cost also bounds the weighted fourth-moment tail.

theorem norm_rescaledGraph_spectralClip_discard_sq_le_cost
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ) {β : ℝ} (hβ : 0 < β)
    (x : H →L[ℂ] H) :
    ‖rescaledGraphVector J Ω c (x - spectralClip β x)‖ ^ 2 ≤
      graphMomentCost Ω (c ^ 2) x / β ^ 2 := by
…

Mentions: OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.spectralClip, OAI.KadisonKastler.graphMomentCost

theorem OAI.KadisonKastler.spectralClip_mem_vonNeumannAlgebra line 128
Source documentation
Clipping respects the actual concrete von Neumann algebra.
```
theorem spectralClip_mem_vonNeumannAlgebra (M : VonNeumannAlgebra H)
    (β : ℝ) {x : H →L[ℂ] H} (hx : x ∈ M) : spectralClip β x ∈ M :=
…
```
Mentions: OAI.KadisonKastler.spectralClip

theorem OAI.KadisonKastler.graphSignal_spectralClip_loss_le line 134

Source documentation

The signal lost in clipping is at most the operator norm times the graph-tail norm.

theorem graphSignal_spectralClip_loss_le
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
    (β : ℝ) (x : H →L[ℂ] H) :
    ‖T (rescaledGraphVector J Ω c x)‖ ≤
      ‖T (rescaledGraphVector J Ω c (spectralClip β x))‖ +
        ‖T‖ * ‖rescaledGraphVector J Ω c (x - spectralClip β x)‖ := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.spectralClip

theorem OAI.KadisonKastler.norm_rescaledGraph_spectralClip_128_discard_le line 154
Source documentation
The concrete cutoff 128 makes the graph-tail norm at most one eighth whenever the sampled graph cost is at most 240.
```
theorem norm_rescaledGraph_spectralClip_128_discard_le
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ) (x : H →L[ℂ] H)
    (hcost : graphMomentCost Ω (c ^ 2) x ≤ 240) :
    ‖rescaledGraphVector J Ω c (x - spectralClip 128 x)‖ ≤ 1 / 8 := by
…
```
Mentions: OAI.KadisonKastler.graphMomentCost, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.spectralClip

theorem OAI.KadisonKastler.graphSignal_spectralClip_128_lower_bound line 165

Source documentation

A sampled vector with the retained squared signal admits an actual bounded clipping that still retains a uniform fraction of that signal.

theorem graphSignal_spectralClip_128_lower_bound
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) (x : H →L[ℂ] H)
    (hcost : graphMomentCost Ω (c ^ 2) x ≤ 240)
    (hsignal : ‖T‖ ^ 2 / 8 ≤ ‖T (rescaledGraphVector J Ω c x)‖ ^ 2) :
    ‖T‖ / 8 ≤ ‖T (rescaledGraphVector J Ω c (spectralClip 128 x))‖ := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.graphMomentCost, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.spectralClip