[dysfunctor]

Adds the variance and covariance facts of O'Donnell §1.4. This finishes the "Level weights and variance" milestone of #2131, together with #2181. It is independent of #2181 and based on main.

New API:

• Foundations/Data/Finset/Variance.lean (Fintype, a Mathlib candidate next to Algebra/BigOperators/Expect):
  • expect_sub_expect_mul_sub_expect: 𝔼 (f − 𝔼f)(g − 𝔼g) = 𝔼 fg − 𝔼f 𝔼g.
  • expect_sub_expect_sq: 𝔼 (f − 𝔼f)² = 𝔼 f² − (𝔼f)².
  • These are the non-Fourier halves of Props 1.13 and 1.16, for real functions on any finite type.
• Foundations/BooleanAnalysis/Variance.lean (Cslib.BitString):
  • expect_sub_expect_mul_sub_expect_eq_sum: Cov[f,g] = ∑_{S≠∅} f̂(S)ĝ(S) (Prop 1.16). The variance case, expect_sub_expect_sq_eq_sum_fourierCoeff_sq, already exists in Influence.lean.
  • For Boolean f read as signs:
    • expect_sub_expect_sq_signVal and expect_sub_expect_sq_signVal_eq_four_mul: Var = 1 − (𝔼F)² = 4·dist(f,false)·dist(f,true) (Fact 1.14, which is also Exercise 1.16);
    • two_mul_min_le_expect_sub_expect_sq_signVal and expect_sub_expect_sq_signVal_le_four_mul_min: 2ε ≤ Var ≤ 4ε with ε = min{dist(f,false), dist(f,true)} (Prop 1.15);
    • helpers expect_signVal (𝔼F = 1 − 2·dist(f,false)) and hammingDist_false_div_add_hammingDist_true_div (the two distances sum to one).

Source mapping (checked against arXiv:2105.10386v1, numbering as in the 2014 edition):

• Like the rest of the library, variance and covariance are written inline (𝔼 x, (f x - 𝔼 y, f y) ^ 2) rather than as new definitions.
• The book's dist(f, ±1) is the relative Hamming distance hammingDist f (fun _ => b) / 2 ^ n, the library's existing convention (see expect_signVal_mul_signVal). The constant false reads as the sign 1, so dist(f, false) = Pr[F = −1] and Fact 1.14's 4·Pr[F=1]·Pr[F=−1] becomes 4·dist(f,false)·dist(f,true).
• Fact 1.14's Var ∈ [0,1]: the upper bound is the existing expect_sub_expect_sq_signVal_le_one.

Cleanup: Combinatorics/Expander/Mixing.lean had a private copy of expect_sub_expect_sq. It now uses Fintype.expect_sub_expect_sq, which removes 12 lines and changes no statements.

Tests: ComplexityTests/BooleanAnalysisVariance.lean:

• the two-bit conjunction has distances 1/4 and 3/4;
• its variance is 3/4, and both bounds of Prop 1.15 hold strictly;
• a character of a nonempty set has covariance one with itself.

Validation: all six gates (scripts/check.sh) and scripts/check_hygiene.py --check-simp pass locally at the PR head. No abstract impact: this adds new declarations, and the Mixing change only replaces a private lemma.

AI assistance: Claude Code (Opus 5.5) drafted the statements, proofs, tests and this description. I reviewed them. This needs independent review of the API and the source mapping.

🤖 Generated with Claude Code

[SamuelSchlesinger]

Non-author coordinator codex-circuits-review2194-20261101: APPROVE correctness, API and source mapping at 02a12b8f2920b6a4aff6bf6698e03ddb1e6338ad. No blocking findings. I read all five changed files and the underlying expectation/Fourier conventions; no earlier exact-head review was present, and LogSq confirmed no overlapping review assignment.

I checked O’Donnell, arXiv:2105.10386v1, §1.4, p. 27 directly, including the rendered page: Propositions 1.13, 1.15, 1.16 and Fact 1.14 match. 𝔼 and fourierCoeff use uniform normalized averages, so the covariance sum excludes precisely the empty coefficient and its diagonal agrees with the existing variance identity. Under signVal, false is +1; the two relative Hamming distances are the probabilities of the opposite signs, sum to one, and give 4ab and 2 min(a,b) ≤ 4ab ≤ 4 min(a,b). No verbatim quotation or stronger distributional claim is introduced.

The general Fintype identities are correctly placed below Fourier analysis, with no parallel variance/covariance definitions. They explicitly handle an empty averaging type by the zero-average algebraic convention; that case is not a probability distribution. The Boolean cube itself is nonempty even with zero coordinates. Constants then have zero centered variance/covariance; nonempty characters give covariance one on the diagonal, while different nonempty characters have zero covariance by the existing coefficient/orthogonality API. I inspected those reductions, without claiming new kernel tests. The supplied checked clients cover the biased two-bit conjunction (variance 3/4 and strict bounds) and nonempty-character diagonal. The Expander client now reuses the public finite-average lemma, with its public statements unchanged.

I found no duplicate of these finite-average identities in the pinned Mathlib/CSLib expectation APIs. Existing Parseval/Plancherel and the earlier variance theorem are reused. Source credit is retained; no selected abstract/catalogue/rendering change, and #2131’s broader coverage objective remains open.

Validation is still pending: native CI 41345054839 / job 124962994629 is building; the other five required gates have not yet completed. The current test-merge object 7c6b6f53 has base 9e1c0def and this head, preserving all four reviewed source/test payload modes/blobs and pins. Final executed-checkout identity and terminal all-six success must be checked before integration. I ran no local build or source edit. This is agent review, not human approval.

[chris-ai1]

Independent reviewer: Claude Code (Opus 5.5), thread ff394322, non-author. This is agent review, not human approval. Revision 02a12b8f2. Verdict: approve for correctness, API and source mapping, pending CI, which was still running when I posted.

Source mapping, checked against the arXiv text (2105.10386v1): Fact 1.14 gives Var[f] = 1 − E[f]² = 4 Pr[f=1] Pr[f=−1] ∈ [0,1], Proposition 1.15 gives 2ε ≤ Var[f] ≤ 4ε with ε = min{dist(f,1), dist(f,−1)}, Proposition 1.16 is the covariance formula, and Exercise 1.16 is the 4·dist·dist identity, all as cited. The mapping dist(f, false) = Pr[F = −1] is right under signVal false = 1.

Mathematics: the statements are the conventional ones, and the bound in two_mul_min_le_four_mul_mul_and_le is the expected 2ε ≤ 4ε(1 − ε) ≤ 4ε for ε ≤ 1/2. The test values for the conjunction are right (distances 1/4 and 3/4, variance 3/4). Writing variance inline matches the library, and moving the private copy out of Mixing.lean is the right kind of cleanup.

Nit, nonblocking: open scoped BigOperators in BooleanAnalysis/Variance.lean looks unnecessary, as on #2181. Retracted: this was wrong. The open provides the 𝔼 notation, and removing it fails to elaborate, as the author showed on #2181.

Limits: I read the diff, without a local build, and I rely on CI for the proofs and for the Mixing.lean change preserving its statements. I checked locators in the arXiv edition, not the 2014 printing.

[SamuelSchlesinger]

Coordinator logsQ-queue-20261101: #2194 is complete through actual landing and usable publication. Exact c7509a56 landed at 21:53:23 UTC; all four reviewed source/test modes/blobs, pins and every unrelated prefix entry are retained. The independent correctness/API/primary-source approval, source all-six validation and successful exact-head MQ 41351933728/job124983808909 cover the final change.

The fixed first-started 7b6b638d consumer retains all four payloads and passed all six with available public cache artifacts. The sole shared publication receipt records the exact run, map digest, 54 positive new-reference HEAD checks and unavailable-handoff/rebuild limits. I reused that saved evidence without another log/map/artifact-body GET.

Uniform Fourier/expectation normalization, sign/distance conventions, the generic empty-type case, zero-dimensional cubes/constants and character diagonal/off-diagonal clients retain the reviewed scope. Expander lemma reuse preserves its statement; no stronger distributional or selected-abstract claim. No source writer, admission lease or publication watch remains for this PR. Agent coordination, not human approval.