The counting reduction in Section 4 #
The indicator-function identities in this file translate between set families and the cube's uniform probability measure. They are the elementary counting steps in Section 4 of arXiv:2609.19123.
Evaluating the Section 4 indicator at a member of its family.
Evaluating the Section 4 indicator outside its family.
The expectation of a family indicator is its density in the Boolean cube, the normalization used in both counting formulas in Section 4.
An increasing family has an increasing indicator, as used for g = 𝟙_B
in Section 4.
For a hereditary family, the function f = 1 - 𝟙_D in Section 4 is
increasing.
The indicator of an antipodal family is self-dual, giving the antipodality
hypothesis for g in the application of Corollary 1.3.
Family duality and Boolean-function duality agree under indicators, as used when translating the families in Sections 3 and 4.
An antipodal family has uniform density one half, the input to Section 4's covariance calculation.
The first counting identity in Section 4: for f = 1 - 𝟙_D and
g = 𝟙_B, with B antipodal, covariance is
(|D| / 2 - |D ∩ B|) / 2^n. Heredity is unnecessary for this identity.
The converse indicator bridge in Section 4: a self-dual family indicator comes from an antipodal family.
Taking the indicator of a Boolean function's support recovers the function, as required in Section 4's converse construction.
The complement of an increasing family is hereditary, used for
D = supp (1 - f) in Section 4's converse.
A family indicator is Boolean-valued, as required when invoking Corollary 1.3 in Section 4.
The complement indicator 1 - 𝟙_D used in Section 4 is Boolean-valued.
Each coordinate sign has uniform mean zero, the cancellation used to count influences in Section 4.
The second counting identity in Section 4: the influence of 1 - 𝟙_D
is twice the number of boundary edges in coordinate i, divided by 2^n.
The numerator is |D| - 2 |D_i|.
The coordinatewise form of equation (17) in Section 4. Taking the minimum influence and the maximum star size yields the displayed equation in the paper.
Equation (17) of Section 4, with its finite minimum of influences and maximum of star cardinalities. A nonempty coordinate type makes the minimum well-defined.
Equation (17) turns a coordinate's influence bound into the corresponding star bound, in either direction.
The star property asserted for each hereditary family in Theorem 1.1: every intersecting subfamily is no larger than some star.
Equations
- D.HasStarProperty = ∀ A ⊆ D, A.IsIntersecting → ∃ (i : ι), Finset.card A ≤ Finset.card (D.star i)
Instances For
The antipodal correlation assertion of Corollary 1.3, expressed with a
coordinate attaining a bound instead of a finite minimum. On a nonempty ground
type this is exactly Cov(f,g) ≥ (1/4) min_i Inf_i[f]. This is a proposition,
not an assumption introduced into the logical environment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Theorem 1.1 deduced from Corollary 1.3, exactly as in Section 4. The analytic correlation theorem is an explicit hypothesis: this declaration does not claim to prove that analytic assertion.
Section 4's converse: a star bound for every hereditary family implies the
antipodal correlation bound, using D = supp(1-f) and B = supp(g).
The equivalence recalled in Section 4 between Chvátal's star assertion and Corollary 1.3's antipodal correlation assertion. Both sides remain explicit propositions; no direction relies on an unproved result.