Moment bounds for counting

TheoremBound on the weight of pairs sharing an endpoint with a fixed pair#✓fully proved

Pairs sharing an endpoint with a fixed pair have total weight at most 4 * P. Loops are permitted. Symmetry bounds the two column fibers by the same row bound.

theorem sum_weights_shared_endpoint_le (c : Matrix ι ι R) (P : R)
    (hc : ∀ a b, 0 ≤ c a b) (hs : ∀ a b, c a b = c b a)
    (hP : ∀ a, ∑ b, c a b ≤ P) (p : ι × ι) :
    (∑ q ∈ (univ.filter fun q : ι × ι =>
      q.1 = p.1 ∨ q.1 = p.2 ∨ q.2 = p.1 ∨ q.2 = p.2), c q.1 q.2) ≤ 4 * P

Used by 1

Used byWeighted quadratic sum bound for a shared-endpoint kernel

TheoremWeighted quadratic sum bound for a shared-endpoint kernel#✓fully proved

A kernel vanishing on pairs with no common endpoint has weighted quadratic sum at most 4 * P * totalWeight * m. Neither nonnegativity nor symmetry of the kernel is required; diagonal weights are permitted, and no separate nonnegativity assumption on P is needed.

theorem sum_mul_mul_kernel_le (c : Matrix ι ι R) (P : R)
    (hc : ∀ a b, 0 ≤ c a b) (hs : ∀ a b, c a b = c b a)
    (hP : ∀ a, ∑ b, c a b ≤ P) (κ : Matrix (ι × ι) (ι × ι) R)
    (m : R) (hm : 0 ≤ m) (h1 : ∀ p q, κ p q ≤ m)
    (h0 : ∀ p q, q.1 ≠ p.1 → q.1 ≠ p.2 → q.2 ≠ p.1 → q.2 ≠ p.2 → κ p q = 0) :
    (∑ p : ι × ι, ∑ q : ι × ι, c p.1 p.2 * c q.1 q.2 * κ p q) ≤
      4 * P * (∑ a, ∑ b, c a b) * m

Uses 1 · Used by 1

Proof usesBound on the weight of pairs sharing an endpoint with a fixed pair

Used byShared-endpoint kernel bound with hypotheses on distinct pairs

TheoremShared-endpoint kernel bound with hypotheses on distinct pairs#✓fully proved

The Variance.StHence bound with the kernel hypothesis restricted to distinct pairs: natural weights on Fin g, integer kernel, and row sums over erased diagonals. Diagonal weights and kernel entries outside the distinct-pair domain are arbitrary. The four inequalities in h0 are precisely the negation of the source Meets disjunction. The proof zeroes diagonal weights and masks the kernel outside the distinct-pair domain; it does not extend a signed sum by adding unmasked terms.

theorem sum_ordered_nat_int_kernel_le (g P : ℕ) (c : Matrix (Fin g) (Fin g) ℕ)
    (hs : ∀ a b, c a b = c b a) (hP : ∀ a, ∑ b ∈ univ.erase a, c a b ≤ P)
    (κ : Matrix (Fin g × Fin g) (Fin g × Fin g) ℤ) (m : ℤ) (hm : 0 ≤ m)
    (h0 : ∀ p ∈ (univ.filter fun p : Fin g × Fin g => p.1 ≠ p.2),
      ∀ q ∈ (univ.filter fun q : Fin g × Fin g => q.1 ≠ q.2),
        q.1 ≠ p.1 → q.1 ≠ p.2 → q.2 ≠ p.1 → q.2 ≠ p.2 → κ p q = 0)
    (h1 : ∀ p ∈ (univ.filter fun p : Fin g × Fin g => p.1 ≠ p.2),
      ∀ q ∈ (univ.filter fun q : Fin g × Fin g => q.1 ≠ q.2), κ p q ≤ m) :
    (∑ p ∈ (univ.filter fun p : Fin g × Fin g => p.1 ≠ p.2),
      ∑ q ∈ (univ.filter fun q : Fin g × Fin g => q.1 ≠ q.2),
        (c p.1 p.2 : ℤ) * (c q.1 q.2 : ℤ) * κ p q) ≤
      ((4 * P * (∑ a, ∑ b ∈ univ.erase a, c a b) : ℕ) : ℤ) * m

Uses 1

Proof usesWeighted quadratic sum bound for a shared-endpoint kernel

TheoremChebyshev-type count bound from the sum of squares#✓fully proved

The number of points where a function is at least a nonnegative threshold, times the threshold squared, is at most the sum of squares.

theorem card_filter_mul_sq_le_sum_sq {Ω : Type*} (S : Finset Ω) (f : Ω → ℤ)
    (s : ℤ) (hs : 0 ≤ s) :
    ((S.filter fun x => s ≤ f x).card : ℤ) * s ^ 2 ≤ ∑ x ∈ S, f x ^ 2

Used by 2

Used byCount bound from first and second moments · Sum-of-squares count bound over the whole type

TheoremCount bound from first and second moments#✓fully proved

A denominator-cleared finite count bound from first and second moments.

Neither the finite set nor A, t, or s is required to be nonzero.

theorem card_filter_mul_sq_le_of_moments {Ω : Type*} (S : Finset Ω) (Y : Ω → ℕ)
    (A m V t s : ℕ)
    (S1 : (∑ x ∈ S, Y x) * A = S.card * m)
    (S2 : (∑ x ∈ S, Y x ^ 2) * A ^ 2 ≤ S.card * m ^ 2 + V) :
    (S.filter fun x => t * m + s ≤ t * (A * Y x)).card * s ^ 2 ≤ t ^ 2 * V

Uses 1 · Used by 1

Proof usesChebyshev-type count bound from the sum of squares

Used byMoment count bound over the whole type

TheoremSum-of-squares count bound over the whole type#✓fully proved

card_filter_mul_sq_le_sum_sq specialized to the universal finset.

theorem card_filter_mul_sq_le_sum_sq_univ {Ω : Type*} [Fintype Ω]
    (f : Ω → ℤ) (s : ℤ) (hs : 0 ≤ s) :
    (#{x : Ω | s ≤ f x} : ℤ) * s ^ 2 ≤ ∑ x, f x ^ 2

Uses 1

Proof usesChebyshev-type count bound from the sum of squares

TheoremMoment count bound over the whole type#✓fully proved

card_filter_mul_sq_le_of_moments specialized to the universal finset.

theorem card_filter_mul_sq_le_of_moments_univ {Ω : Type*} [Fintype Ω]
    (Y : Ω → ℕ) (A m V t s : ℕ)
    (S1 : (∑ x, Y x) * A = Fintype.card Ω * m)
    (S2 : (∑ x, Y x ^ 2) * A ^ 2 ≤ Fintype.card Ω * m ^ 2 + V) :
    #{x : Ω | t * m + s ≤ t * (A * Y x)} * s ^ 2 ≤ t ^ 2 * V

Uses 1 · Used by 1

Proof usesCount bound from first and second moments

Used byBalanced coloring of a weighted symmetric matrix

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.