GraphSignalSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous graph signal and clipping-cost selection

The normalized sign sum is passed through an actual real-linear signal map. A constant orbit signal gives its exact second moment and the Hilbert fourth-moment bound. Finite selection then retains the signal and bounds the actual vector-state clipping cost in the same sample.

theorem OAI.KadisonKastler.map_normalizedFiniteSignSum line 27
Source documentation
A real-linear signal map commutes with the normalized sign sum.
Distinct definitions of this name: OAI/Analysis/KadisonKastler/FiniteSignFourthMoment.lean:364 (different declaration text). Qualify references as OAI.KadisonKastler.map_normalizedFiniteSignSum@path.
```
theorem map_normalizedFiniteSignSum (L : (H →L[ℂ] H) →ₗ[ℝ] V)
    (a : I → H →L[ℂ] H) (ε : I → Bool) :
    L (normalizedFiniteSignSum a ε) = normalizedHilbertSignSum (fun i => L (a i)) ε := by
…
```
Mentions: OAI.KadisonKastler.normalizedFiniteSignSum, OAI.KadisonKastler.normalizedHilbertSignSum

theorem OAI.KadisonKastler.sampled_sign_signal_second line 34

Source documentation

All sampled summands have the same signal variance.

theorem sampled_sign_signal_second (L : (H →L[ℂ] H) →ₗ[ℝ] V)
    (a : G → H →L[ℂ] H) (s : ℝ) (hsignal : ∀ g, ‖L (a g)‖ ^ 2 = s) :
    (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      ‖L (normalizedFiniteSignSum (fun i => a (ω i)) ε)‖ ^ 2) = s := by
…

Mentions: OAI.KadisonKastler.normalizedFiniteSignSum

theorem OAI.KadisonKastler.sampled_sign_signal_fourth line 45

Source documentation

The signal fourth moment is controlled independently of the number of matrix samples.

theorem sampled_sign_signal_fourth (L : (H →L[ℂ] H) →ₗ[ℝ] V)
    (a : G → H →L[ℂ] H) (s : ℝ) (hsignal : ∀ g, ‖L (a g)‖ ^ 2 = s) :
    (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      ‖L (normalizedFiniteSignSum (fun i => a (ω i)) ε)‖ ^ 4) ≤ 3 * s ^ 2 := by
…

Mentions: OAI.KadisonKastler.normalizedFiniteSignSum

theorem OAI.KadisonKastler.graphMomentCost_nonneg line 62
Source documentation
The clipping cost is nonnegative for a nonnegative graph scale.
```
theorem graphMomentCost_nonneg (Ω : H) {k : ℝ} (hk : 0 ≤ k) (x : H →L[ℂ] H) :
    0 ≤ graphMomentCost Ω k x := by
…
```
Mentions: OAI.KadisonKastler.graphMomentCost

theorem OAI.KadisonKastler.exists_sampled_sign_signal_and_cost line 77

Source documentation

One actual finite sample simultaneously retains half of the signal variance and has clipping cost at most 240.

theorem exists_sampled_sign_signal_and_cost
    (Ω : H) {k : ℝ} (hk : 0 ≤ k)
    (L : (H →L[ℂ] H) →ₗ[ℝ] V) (a : G → H →L[ℂ] H)
    {s : ℝ} (hs : 0 < s) (hsignal : ∀ g, ‖L (a g)‖ ^ 2 = s)
    (hcost : (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      graphMomentCost Ω k (normalizedFiniteSignSum (fun i => a (ω i)) ε)) ≤ 10) :
    ∃ ω : I → G, ∃ ε : I → Bool,
      s / 2 ≤ ‖L (normalizedFiniteSignSum (fun i => a (ω i)) ε)‖ ^ 2 ∧
      graphMomentCost Ω k (normalizedFiniteSignSum (fun i => a (ω i)) ε) ≤ 240 := by
…

Mentions: OAI.KadisonKastler.graphMomentCost, OAI.KadisonKastler.normalizedFiniteSignSum