FiniteMomentSelection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous selection from second and fourth moments

This finite probability argument combines the graph-signal second and fourth moments with a first-moment bound for the clipping cost. All averages are over the actual nonempty finite probability space.

theorem OAI.KadisonKastler.exists_signal_and_cost_le line 19

Source documentation

A fourth-moment signal and a bounded mean cost have a simultaneous realization. These are the constants used before spectral clipping.

theorem exists_signal_and_cost_le
    {ι : Type*} [Fintype ι] [Nonempty ι]
    (Z B : ι → ℝ) {s : ℝ} (hs : 0 < s)
    (hZ : ∀ i, 0 ≤ Z i) (hB : ∀ i, 0 ≤ B i)
    (hmean : (𝔼 i, Z i) = s)
    (hfourth : (𝔼 i, Z i ^ 2) ≤ 3 * s ^ 2)
    (hcost : (𝔼 i, B i) ≤ 10) :
    ∃ i, s / 2 ≤ Z i ∧ B i ≤ 240 := by
…