From 632f9e171c688e60cf6772d262079987ee9a9032 Mon Sep 17 00:00:00 2001 From: Vincent Liew Date: Sat, 31 Oct 2026 20:46:59 -0700 Subject: [PATCH] doc(boolean-analysis): correct O'Donnell citation locators Point docstring citations of O'Donnell's Analysis of Boolean Functions at the items they actually formalize, found by the coverage audit in #2131: - FriedgutJunta: the junta-weight bound adapts the proof of Theorem 9.28 rather than stating it; the junta-closeness lemma is Proposition 3.31 with Exercise 3.28. - KahnKalaiLinial: the Var log(1/delta) <= 6 I bound is a weaker form of the book's KKL Edge-Isoperimetric Theorem; the derivative bound is Corollary 9.12. - LongCode: drop the Chapter 7 citation for mod-2 projection along maps, which the book does not treat. - Monotone: I <= sqrt n is Exercise 2.23, not Section 2.3. - Noise: NS <= delta I is Exercise 2.42. - BucketWeight: the sampling identity is from the proof of Proposition 3.40, which itself states the estimation algorithm. - KushilevitzMansour: write W^{S | J-bar}, matching the library's own convention and the book. Documentation only; no declarations change. Co-Authored-By: Claude Opus 5.5 --- .../BooleanAnalysis/BucketWeight.lean | 11 ++++++----- .../BooleanAnalysis/FriedgutJunta.lean | 5 +++-- .../BooleanAnalysis/KahnKalaiLinial.lean | 17 +++++++++-------- .../Foundations/BooleanAnalysis/LongCode.lean | 2 +- .../Foundations/BooleanAnalysis/Monotone.lean | 8 ++++---- .../Foundations/BooleanAnalysis/Noise.lean | 5 +++-- .../UniformLearning/KushilevitzMansour.lean | 4 ++-- 7 files changed, 28 insertions(+), 24 deletions(-) diff --git a/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean b/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean index e375bd678f..a42b25550e 100644 --- a/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean +++ b/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean @@ -25,7 +25,8 @@ The bucket weight is the expected squared coefficient of the restriction of `F` coordinates outside `J` at random (`BitString.expect_fourierCoeff_piecewise_sq`), hence the expectation of `F (x, z) χ_S(x) F (y, z) χ_S(y)` for independent uniform `x`, `y`, `z`, where `(x, z)` takes the coordinates in `J` from `x` and the others from `z` -(`BitString.bucketWeight_eq_expect_sample`) [O'Donnell, Proposition 3.40][ODonnell2014]. With query +(`BitString.bucketWeight_eq_expect_sample`), as in the proof of +[O'Donnell, Proposition 3.40][ODonnell2014]. With query access to a Boolean function this lets one estimate any bucket weight by sampling: the basis of the Goldreich–Levin and Kushilevitz–Mansour algorithms [GoldreichLevin1989] [KushilevitzMansour1993]. @@ -97,10 +98,10 @@ theorem bucketWeight_eq_expect (F : (ι → Bool) → ℝ) (J S : Finset ι) : bucketWeight F J S = 𝔼 z, fourierCoeff (fun x => F (J.piecewise x z)) S ^ 2 := (expect_fourierCoeff_piecewise_sq F J S).symm -/-- **Estimating a bucket weight by sampling** [O'Donnell, Proposition 3.40][ODonnell2014]: the -bucket weight of `S` in `J` is the expectation of `F (x, z) χ_S(x) F (y, z) χ_S(y)` for independent -uniform `x`, `y`, `z`, where `(x, z)` takes the coordinates in `J` from `x` and the others -from `z`. -/ +/-- **Estimating a bucket weight by sampling**: the bucket weight of `S` in `J` is the expectation +of `F (x, z) χ_S(x) F (y, z) χ_S(y)` for independent uniform `x`, `y`, `z`, where `(x, z)` takes +the coordinates in `J` from `x` and the others from `z`, as in the proof of +[O'Donnell, Proposition 3.40][ODonnell2014]. -/ theorem bucketWeight_eq_expect_sample (F : (ι → Bool) → ℝ) (J S : Finset ι) : bucketWeight F J S = 𝔼 p : (ι → Bool) × (ι → Bool) × (ι → Bool), F (J.piecewise p.1 p.2.2) * chi ℝ S p.1 * (F (J.piecewise p.2.1 p.2.2) * chi ℝ S p.2.1) := by diff --git a/Complexity/Foundations/BooleanAnalysis/FriedgutJunta.lean b/Complexity/Foundations/BooleanAnalysis/FriedgutJunta.lean index 89a441b989..e5476748d4 100644 --- a/Complexity/Foundations/BooleanAnalysis/FriedgutJunta.lean +++ b/Complexity/Foundations/BooleanAnalysis/FriedgutJunta.lean @@ -88,7 +88,8 @@ private theorem sq_signVal_sub_signVal_decide_div_four_le (a : Bool) (t : ℝ) : /-- **Spectral concentration gives a junta**: a Boolean function is at relative Hamming distance at most `∑_{S ⊄ J} F̂(S) ^ 2` from a Boolean function of the coordinates in `J`, the sign of its -average over the other coordinates [O'Donnell, Proposition 3.31][ODonnell2014]. -/ +average over the other coordinates +[O'Donnell, Proposition 3.31 and Exercise 3.28][ODonnell2014]. -/ theorem exists_dependsOn_hammingDist_div_le_sum_not_subset_fourierCoeff_sq (f : (ι → Bool) → Bool) (J : Finset ι) : ∃ g : (ι → Bool) → Bool, DependsOn g (J : Set ι) ∧ @@ -142,7 +143,7 @@ private theorem sum_card_sdiff_mul_one_third_pow_fourierCoeff_sq_le /-- **The Fourier weight outside the influential coordinates**: if every coordinate outside `J` has influence at most `τ` on a Boolean function read as signs `F`, then for every `A > 1`, -`∑_{S ⊄ J} F̂(S) ^ 2 ≤ log 3 / log A · I[F] + A / 3 · √τ · I[F]` +`∑_{S ⊄ J} F̂(S) ^ 2 ≤ log 3 / log A · I[F] + A / 3 · √τ · I[F]`, adapting the proof of [O'Donnell, Theorem 9.28][ODonnell2014]. -/ theorem sum_filter_not_subset_fourierCoeff_sq_le (f : (ι → Bool) → Bool) {J : Finset ι} {τ : ℝ} (hJ : ∀ i ∉ J, influence i (fun x => signVal (f x)) ≤ τ) {A : ℝ} (hA : 1 < A) : diff --git a/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean b/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean index ce971a7ea9..168f9d8e6b 100644 --- a/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean +++ b/Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean @@ -18,11 +18,12 @@ inequality the influences of `F` on its `n` coordinates average at least `Var[F] **Kahn–Kalai–Linial theorem** says that some coordinate has influence at least `c · Var[F] · log n / n`, for an absolute constant `c > 0` [KahnKalaiLinial1988]. We prove it with `c = 1 / 12` (`BitString.exists_expect_sub_expect_sq_mul_log_card_div_le_influence`), -through its edge-isoperimetric form in O'Donnell's exposition: if every coordinate has influence -at most `δ`, then the total influence is at least `1 / 6 · Var[F] · log (1 / δ)` -(`BitString.expect_sub_expect_sq_mul_log_inv_le_six_mul_totalInfluence`) -[O'Donnell, Section 9.6][ODonnell2014]. Here `Var[F]` is written -`𝔼 x, (F x - 𝔼 y, F y) ^ 2`, the Fourier weight of `F` on the nonempty sets. +through an edge-isoperimetric form: if every coordinate has influence at most `δ`, then the total +influence is at least `1 / 6 · Var[F] · log (1 / δ)` +(`BitString.expect_sub_expect_sq_mul_log_inv_le_six_mul_totalInfluence`). This is a weaker form +of the KKL Edge-Isoperimetric Theorem in O'Donnell's exposition, proved by the same use of +hypercontractivity on the derivatives [O'Donnell, Section 9.6][ODonnell2014]. Here `Var[F]` is +written `𝔼 x, (F x - 𝔼 y, F y) ^ 2`, the Fourier weight of `F` on the nonempty sets. The same argument, run separately on each coordinate, proves **Talagrand's inequality** `Var[F] ≤ 6 ∑ᵢ Infᵢ[F] / log (1 / Infᵢ[F])`, for functions whose influences are all less than @@ -82,7 +83,7 @@ variable {ι : Type*} [Fintype ι] [DecidableEq ι] /-- **Hypercontractivity bounds the low-degree weight on the sets containing a coordinate**: for a Boolean function read as signs, `∑_{S ∋ i} 3 ^ (-|S|) F̂(S) ^ 2 ≤ 1/3 · Infᵢ[F] ^ (3/2)`, by the `(4/3, 2)`-Hypercontractivity Theorem applied to the derivative in `i` -[O'Donnell, Section 9.6][ODonnell2014]. -/ +[O'Donnell, Corollary 9.12][ODonnell2014]. -/ theorem sum_filter_mem_one_third_pow_mul_fourierCoeff_sq_le (f : (ι → Bool) → Bool) (i : ι) : ∑ S with i ∈ S, (1 / 3 : ℝ) ^ #S * fourierCoeff (fun x => signVal (f x)) S ^ 2 ≤ influence i (fun x => signVal (f x)) * √(influence i fun x => signVal (f x)) / 3 := by @@ -252,8 +253,8 @@ private theorem sum_filter_mem_fourierCoeff_sq_div_card_mul_log_le (f : (ι → /-- **The Kahn–Kalai–Linial theorem, edge-isoperimetric form**: if every coordinate has influence at most `δ` on a Boolean function read as signs `F`, then `Var[F] · log (1 / δ) ≤ 6 I[F]`, that is, the total influence is at least `1/6 · Var[F] · log (1 / δ)` [KahnKalaiLinial1988] -[Talagrand1994] [O'Donnell, Section 9.6][ODonnell2014]. For `δ ≥ 1` the left side is at most -zero. -/ +[Talagrand1994]. This is a weaker form of the KKL Edge-Isoperimetric Theorem of +[O'Donnell, Section 9.6][ODonnell2014]. For `δ ≥ 1` the left side is at most zero. -/ theorem expect_sub_expect_sq_mul_log_inv_le_six_mul_totalInfluence (f : (ι → Bool) → Bool) {δ : ℝ} (hδ : ∀ i, influence i (fun x => signVal (f x)) ≤ δ) : (𝔼 x, (signVal (f x) - 𝔼 y, signVal (f y)) ^ 2) * log δ⁻¹ ≤ diff --git a/Complexity/Foundations/BooleanAnalysis/LongCode.lean b/Complexity/Foundations/BooleanAnalysis/LongCode.lean index 94bfcb94bc..dbd5a32a74 100644 --- a/Complexity/Foundations/BooleanAnalysis/LongCode.lean +++ b/Complexity/Foundations/BooleanAnalysis/LongCode.lean @@ -32,7 +32,7 @@ vanish on every set of even cardinality (`BitString.IsOdd.fourierCoeff_of_even`) For a map `π : β → γ`, the *mod-2 projection* `BitString.projectSet π T` of `T : Finset β` is the set of points of `γ` with an odd number of preimages in `T`. Pulling a character back along `π` projects its frequency set: `chi T (f ∘ π) = chi (projectSet π T) f` -(`BitString.chi_comp_eq_chi_projectSet`) [Håstad][Hastad2001], [O'Donnell, Chapter 7][ODonnell2014]. +(`BitString.chi_comp_eq_chi_projectSet`) [Håstad][Hastad2001]. ## Main definitions diff --git a/Complexity/Foundations/BooleanAnalysis/Monotone.lean b/Complexity/Foundations/BooleanAnalysis/Monotone.lean index 8ca3aeaf0d..3c59b2bd65 100644 --- a/Complexity/Foundations/BooleanAnalysis/Monotone.lean +++ b/Complexity/Foundations/BooleanAnalysis/Monotone.lean @@ -30,7 +30,7 @@ The degree-one coefficients carry at most the variance (`BitString.sum_fourierCoeff_singleton_sq_le`), so by the Cauchy–Schwarz inequality a monotone or antitone Boolean function on `n` coordinates with variance `σ²` has total influence at most `√(n σ²)` (`BitString.totalInfluence_le_sqrt_card_mul_of_monotone`), in particular at most `√n` -(`BitString.totalInfluence_le_sqrt_card_of_monotone`) [O'Donnell, Section 2.3][ODonnell2014]. +(`BitString.totalInfluence_le_sqrt_card_of_monotone`) [O'Donnell, Exercise 2.23][ODonnell2014]. ## Main results @@ -156,8 +156,8 @@ theorem sum_influence_sq_le_of_monotone (hf : Monotone f) : exact sum_fourierCoeff_singleton_sq_le _ /-- **Monotone functions have total influence at most `√(n σ²)`**: a monotone Boolean function on -`n` coordinates, read as signs with variance `σ²`, has total influence at most `√(n σ²)` -[O'Donnell, Section 2.3][ODonnell2014]. -/ +`n` coordinates, read as signs with variance `σ²`, has total influence at most `√(n σ²)`, +refining [O'Donnell, Exercise 2.23][ODonnell2014]. -/ theorem totalInfluence_le_sqrt_card_mul_of_monotone (hf : Monotone f) : totalInfluence (fun x => signVal (f x)) ≤ √(Fintype.card ι * 𝔼 x, (signVal (f x) - 𝔼 y, signVal (f y)) ^ 2) := by @@ -181,7 +181,7 @@ theorem totalInfluence_le_sqrt_card_mul_of_antitone (hf : Antitone f) : /-- **Monotone functions have total influence at most `√n`**: a monotone Boolean function on `n` coordinates, read as signs, has total influence at most `√n` -[O'Donnell, Section 2.3][ODonnell2014]. -/ +[O'Donnell, Exercise 2.23][ODonnell2014]. -/ theorem totalInfluence_le_sqrt_card_of_monotone (hf : Monotone f) : totalInfluence (fun x => signVal (f x)) ≤ √(Fintype.card ι) := (totalInfluence_le_sqrt_card_mul_of_monotone hf).trans <| Real.sqrt_le_sqrt <| diff --git a/Complexity/Foundations/BooleanAnalysis/Noise.lean b/Complexity/Foundations/BooleanAnalysis/Noise.lean index b4bdea4831..23eb832bca 100644 --- a/Complexity/Foundations/BooleanAnalysis/Noise.lean +++ b/Complexity/Foundations/BooleanAnalysis/Noise.lean @@ -34,8 +34,9 @@ probability that `f x ≠ f y` when `y` flips each bit of a uniform `x` independ probability `δ`. Reading `f` as the function `F = (-1) ^ f` with values `±1`, it is `NS_δ[f] = 1 / 2 - 1 / 2 Stab_{1 - 2 δ}[F]` (`BitString.noiseSensitivity_eq_noiseStability`), hence `NS_δ[f] = ∑_S (1 - (1 - 2 δ) ^ |S|) / 2 F̂(S) ^ 2` (`BitString.noiseSensitivity_eq_sum`) -and `NS_δ[f] ≤ δ I[F]`, at most `δ` times the total influence -(`BitString.noiseSensitivity_le_mul_totalInfluence`) [O'Donnell, Section 2.4][ODonnell2014]. +[O'Donnell, Section 2.4][ODonnell2014], and `NS_δ[f] ≤ δ I[F]`, at most `δ` times the total +influence (`BitString.noiseSensitivity_le_mul_totalInfluence`) +[O'Donnell, Exercise 2.42][ODonnell2014]. The noised string is `x + P`, the coordinatewise exclusive or of `x` with a random mask `P` of `BitString.bernoulliAverage`, bit strings adding in Mathlib's Boolean ring structure on diff --git a/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean b/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean index 6f0703524a..1e1bc202f3 100644 --- a/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean +++ b/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean @@ -142,7 +142,7 @@ theorem toFinset_mem_searchLevels (l : List ι) : l.toFinset ∈ searchLevels l | cons i l => simp [searchLevels] /-- **The bucket search** of Goldreich–Levin and Kushilevitz–Mansour over the list `l` of -coordinates, given estimates `est J S` of the bucket weights `W^{S | J}` and a threshold `τ`. +coordinates, given estimates `est J S` of the bucket weights `W^{S | J̄}` and a threshold `τ`. Starting from the bucket of all sets, it adds the coordinates of `l` from the last to the first, splits each surviving bucket `S` of `J` into the buckets `S` and `insert i S` of `insert i J`, and keeps the buckets whose estimated weight is at least `τ`. -/ @@ -232,7 +232,7 @@ variable (ι) in def decisionTreeClass (L : ℕ) : ConceptClass (ι → Bool) Bool := {f | ∃ t : DecisionTree ι Bool, t.Computes f ∧ t.leafCount ≤ L} -/-- The empirical estimate of the bucket weight `W^{S | J}` of `g`, read as signs, from the +/-- The empirical estimate of the bucket weight `W^{S | J̄}` of `g`, read as signs, from the samples `ω j = (x, y, z)`: the average of `g (x, z) χ_S(x) g (y, z) χ_S(y)`, where `(x, z)` takes the coordinates in `J` from `x` and the others from `z`. -/ noncomputable def bucketEstimate (g : (ι → Bool) → Bool)