doc(boolean-analysis): correct O'Donnell citation locators

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

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) :

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 δ⁻¹ ≤

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
 

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 <|

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

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)