The spectral coefficients in the weighted star inequality #
This file formalizes Proposition 5.3 of arXiv:2609.19123. The paper assigns each nonempty Fourier set to its largest coordinate in a fixed total order. The arguments below allow any fixed selector belonging to that set, a slightly stronger formulation which includes the paper's choice.
Proposition 5.3's coefficients λ_i: four times the nonconstant Fourier
mass assigned to coordinate i. The selector is fixed independently of the
weight or hereditary family under consideration.
Equations
- Chvatal.spectralWeights g select i = 4 * ∑ S ∈ Finset.univ.erase ∅, if select S = i then Chvatal.fourier g S ^ 2 else 0
Instances For
Nonnegativity of every coefficient in Proposition 5.3.
Regrouping Fourier sets according to their selected coordinate, the partition-of-mass step in Proposition 5.3.
The coefficients in Proposition 5.3 sum to one, by Parseval and the variance-one-quarter identity for an antipodal Boolean function.
A fixed total order gives the selector max_≺ S used in Proposition 5.3.
The value at the empty set is irrelevant because the coefficients omit it.
Equations
- Chvatal.orderedSelector S = if hS : S.Nonempty then S.max' hS else Classical.choice ⋯
Instances For
The ordered selector lies in each nonempty set, the property of the
paper's max_≺ used in the weighted argument.
The hereditary-family inequality in the proof of Proposition 5.3, deduced from the selected-coordinate spectral lower bound. This hypothesis is explicit so the counting reduction is independent of the analytic proof.
The fractional star function q(x) = ∑_i λ_i x_i from the proof of
Proposition 5.3.
Instances For
Counting the fractional star function on a family gives the corresponding weighted combination of its star cardinalities (Proposition 5.3).
Summing a family indicator over another family counts their intersection, the second counting step for the defect in Proposition 5.3.
The mean-zero defect in Proposition 5.3, summed on a hereditary family. The identity itself holds for every family.
The weighted form of the same defect, obtained by interchanging finite sums. This is the finite counterpart of the layer-cake calculation in (18).
Finite layer-cake lifting in Proposition 5.3: domination on every hereditary family implies domination for every nonnegative decreasing weight.
The selected-coordinate expression in Proposition 5.3 is bounded by the spectral expression in Theorem 1.2, because the selector belongs to its set.
The first inequality of Proposition 5.3 deduced from the antipodal spectral bound, keeping the analytic dependency explicit.
Proposition 5.3's first inequality, proved from the antipodal case of Theorem 1.2. It holds for any fixed selector belonging to each nonempty index.
A convex combination of star weights is at most their maximum, the second inequality in equation (18).
Proposition 5.3 in the paper's exact ordered-selector formulation: the spectral coefficients are nonnegative, sum to one, and satisfy both inequalities in equation (18). The total order represents the paper's fixed permutation.
The final conclusion of Proposition 5.3 for one intersecting family: its total nonnegative decreasing weight is bounded by some full-cube star.
The final maximum-attainment statement of Proposition 5.3: one star simultaneously dominates every intersecting family for a fixed nonnegative decreasing weight, and that star is itself intersecting.