A second-moment support bound

The Paley–Zygmund style inequality behind Dinur's powering estimate: a nonnegative random variable is nonzero on a set at least as large as the square of its mean over its second moment. Written with sums rather than expectations, so that the normalising cardinality cancels on its own:

(∑ N) ^ 2 ≤ |support N| · ∑ N ^ 2

In the powering analysis N counts how many faulty edges a random walk traverses. The first moment is proportional to the gap, the second moment is controlled by the expander mixing lemma, and this inequality converts the two into a lower bound on the probability that the walk meets a faulty edge at all — which is what the powered constraint detects.

Main results

• sq_sum_le_card_support_mul_sum_sq — the inequality above
• sq_sum_div_sum_sq_le_card_support — its ratio form
• card_ge_of_moments — Paley–Zygmund in counting form

theorem Complexity.sq_sum_le_card_support_mul_sum_sq {ι : Type u_1} [Fintype ι] (N : ι → ℝ) : (∑ i : ι, N i) ^ 2 ≤ ↑{i : ι | N i ≠ 0}.card * ∑ i : ι, N i ^ 2

Second-moment support bound. The square of a sum is at most the size of the summand's support times the sum of squares.

theorem Complexity.sq_sum_div_sum_sq_le_card_support {ι : Type u_1} [Fintype ι] (N : ι → ℝ) (h : 0 < ∑ i : ι, N i ^ 2) : (∑ i : ι, N i) ^ 2 / ∑ i : ι, N i ^ 2 ≤ ↑{i : ι | N i ≠ 0}.card

The ratio form: the support is at least the mean-square ratio.

theorem Complexity.card_ge_of_moments {ι : Type u_1} [Fintype ι] (N : ι → ℝ) (S : Finset ι) (hsupp : ∀ (i : ι), N i ≠ 0 → i ∈ S) {A B : ℝ} (hA0 : 0 ≤ A) (hA : A ≤ ∑ i : ι, N i) (hB : ∑ i : ι, N i ^ 2 ≤ B) (hB0 : 0 < B) : A ^ 2 / B ≤ ↑S.card

Paley–Zygmund, in counting form. If a nonnegative count has first moment at least A and second moment at most B, then at least A ^ 2 / B of the indices carry a nonzero count. Any S containing the support inherits the bound — in the powering argument S is the set of unsatisfied constraints and the count is the number of crossings that break one.