Add the monotone reduction and Russo's lemma for Boolean functions

FILE_TREE.md

@@ -4,7 +4,7 @@
 
 This document presents the public Lean source tree after the Mathlib-style subject
 refactor.
-`StatsMLlib/` contains 149 Lean modules under eight layer-one directories and
+`StatsMLlib/` contains 151 Lean modules under eight layer-one directories and
 no root-level Lean files. A filesystem path such as `StatsMLlib/Probability/Process/Dudley.lean`
 corresponds to the Lean module `StatsMLlib.Probability.Process.Dudley`.
 
@@ -15,10 +15,10 @@ corresponds to the Lean module `StatsMLlib.Probability.Process.Dudley`.
 | `LinearAlgebra` | 7 |
 | `MeasureTheory` | 4 |
 | `Order` | 1 |
-| `Probability` | 71 |
+| `Probability` | 73 |
 | `Statistics` | 22 |
 | `Topology` | 2 |
-| **Total** | **149** |
+| **Total** | **151** |
 
 ```text
 StatsMLlib/
@@ -100,7 +100,9 @@ StatsMLlib/
 │   ├── Concentration/
 │   │   ├── Influence/
 │   │   │   ├── Basic.lean
-│   │   │   └── Martingale.lean
+│   │   │   ├── Martingale.lean
+│   │   │   ├── Monotone.lean
+│   │   │   └── Threshold.lean
 │   │   ├── LogSobolev/
 │   │   │   ├── Bernoulli.lean
 │   │   │   ├── GaussianCompactSupport.lean

README.md

@@ -22,7 +22,7 @@ The public source contains 90 modules and no `sorry`, `axiom`, `admit`, or `nati
 | Topology | `StatsMLlib.Topology.*` | Covering and packing numbers, separable suprema |
 | Analysis | `StatsMLlib.Analysis.*` | Metric entropy, chaining, normed-space covering estimates |
 | Linear algebra | `StatsMLlib.LinearAlgebra.*` | Singular values, variational principles, matrix perturbation |
-| Probability | `StatsMLlib.Probability.*` | Concentration, entropy methods, influences and the KKL theorem, Gaussian analysis, random matrices |
+| Probability | `StatsMLlib.Probability.*` | Concentration, entropy methods, influences, the KKL theorem, monotone reduction and Russo's lemma, Gaussian analysis, random matrices |
 | Learning theory | `StatsMLlib.LearningTheory.*` | Empirical metrics, Rademacher complexity, uniform deviation |
 | Statistics | `StatsMLlib.Statistics.*` | Localized least squares, regression, kernel density estimation, and minimax guarantees |
 

StatsMLlib/Probability/Concentration/Influence/Basic.lean

@@ -51,7 +51,7 @@ def totalInfluence (f : (Fin n → Bool) → ℝ) : ℝ := ∑ i, influence f i
 lemma influence_nonneg (f : (Fin n → Bool) → ℝ) (i : Fin n) : 0 ≤ influence f i :=
   expect_nonneg fun x ↦ by split_ifs <;> norm_num
 
-/-! ### Lemma 9.3 -/
+/-! ### BLM Lemma 9.3 -/
 
 /-- The rescaled form of `a² log(1/(ac)) ≤ a/c - a²`. -/
 private lemma sq_mul_log_le (A m : ℝ) (hA : 0 < A) (hm : 0 < m) {t : ℝ} (ht : 0 ≤ t) :
@@ -69,7 +69,7 @@ private lemma sq_mul_log_le (A m : ℝ) (hA : 0 < A) (hm : 0 < m) {t : ℝ} (ht
     field_simp
   linarith
 
-/-- Lemma 9.3: for `f ≥ 0`, `E[f²] log(E[f²] / (E f)²) ≤ 2 𝓔(f)`. -/
+/-- BLM Lemma 9.3: for `f ≥ 0`, `E[f²] log(E[f²] / (E f)²) ≤ 2 𝓔(f)`. -/
 theorem sq_expect_mul_log_le_dirichletForm (f : (Fin n → Bool) → ℝ) (hf : ∀ x, 0 ≤ f x) :
     expect (fun x ↦ f x ^ 2) * log (expect (fun x ↦ f x ^ 2) / expect f ^ 2) ≤
       2 * dirichletForm f f := by
@@ -101,7 +101,7 @@ theorem sq_expect_mul_log_le_dirichletForm (f : (Fin n → Bool) → ℝ) (hf :
   push_cast
   linarith
 
-/-! ### Theorem 9.4 -/
+/-! ### BLM Theorem 9.4 -/
 
 /-- L2: taking absolute values decreases the Dirichlet form. -/
 lemma dirichletForm_abs_le (u : (Fin n → Bool) → ℝ) :
@@ -158,7 +158,7 @@ lemma sum_sq_expect_abs_martingaleDiff_pos (f : (Fin n → Bool) → ℝ) (hV :
   exact pow_eq_zero_iff two_ne_zero |>.mp <|
     (Finset.sum_eq_zero_iff_of_nonneg fun j _ ↦ sq_nonneg _).mp h.symm i hi
 
-/-- Theorem 9.4: `Var f · log(Var f / ∑ᵢ (E|Δᵢ|)²) ≤ 2 𝓔(f)`. -/
+/-- BLM Theorem 9.4: `Var f · log(Var f / ∑ᵢ (E|Δᵢ|)²) ≤ 2 𝓔(f)`. -/
 theorem variance_mul_log_le_dirichletForm (f : (Fin n → Bool) → ℝ) (hV : 0 < variance f) :
     variance f * log (variance f / ∑ i : Fin n, expect (fun x ↦ |martingaleDiff f i x|) ^ 2) ≤
       2 * dirichletForm f f := by
@@ -268,7 +268,7 @@ lemma log_pow_four_le {x : ℝ} (hx1 : 1 ≤ x) : log x ^ 4 ≤ 256 * x := by
   calc log x ^ 4 ≤ (x ^ (1 / 4 : ℝ) / (1 / 4)) ^ 4 := pow_le_pow_left₀ (log_nonneg hx1) h 4
     _ = 256 * x := by rw [div_pow, hpow]; norm_num; ring
 
-/-- Theorem 9.5: for Boolean `f` and `n ≥ 2`, `Var(f)² (log n)² / n ≤ ∑ᵢ Iᵢ(f)²`. -/
+/-- BLM Theorem 9.5: for Boolean `f` and `n ≥ 2`, `Var(f)² (log n)² / n ≤ ∑ᵢ Iᵢ(f)²`. -/
 theorem sum_influence_sq_ge (hn : 2 ≤ n) (hf : ∀ x, f x = 0 ∨ f x = 1) :
     variance f ^ 2 * log n ^ 2 / n ≤ ∑ i, influence f i ^ 2 := by
   have hsum0 : 0 ≤ ∑ i, influence f i ^ 2 := Finset.sum_nonneg fun i _ ↦ sq_nonneg _

StatsMLlib/Probability/Concentration/Influence/Monotone.lean

@@ -0,0 +1,248 @@
+/-
+Copyright (c) 2026 Kei Tsukamoto. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kei Tsukamoto
+-/
+import StatsMLlib.Probability.Concentration.Influence.Basic
+
+/-!
+# Reduction to monotone Boolean functions
+
+On the uniform hypercube `{±1}^n`, encoded as `Fin n → Bool`, the shift operator `Sᵢ` pushes
+the mass of a Boolean function towards `xᵢ = 1`: on each pair `{x, flipᵢ x}` it puts the larger
+value on the point with `xᵢ = 1`. It preserves the expectation and does not increase the total
+influence. A maximal-potential argument then shows that every Boolean function can be replaced by
+a monotone one with the same expectation and no larger total influence.
+
+## Main definitions
+
+* `Influence.boolToReal b`: the embedding `false ↦ 0`, `true ↦ 1` of `Bool` into `ℝ`.
+* `Influence.shift i g`: the shift operator `Sᵢ` on Boolean functions.
+
+## Main results
+
+* `Influence.expect_shift`: `E[Sᵢ g] = E[g]`.
+* `Influence.totalInfluence_shift_le`: `I(Sᵢ g) ≤ I(g)`.
+* `Influence.exists_monotone` (BLM Theorem 9.10): for every Boolean `f` there is a monotone Boolean
+  `g` with `E[g] = E[f]` and `I(g) ≤ I(f)`.
+
+## Implementation notes
+
+Instead of iterating the shifts until the function becomes monotone, we take a function of
+maximal potential `φ(g) = E[g(x) ‖x‖]` among those with the right expectation and total
+influence; a non-monotone function would be improved by some shift.
+-/
+
+open BernoulliLSI
+
+noncomputable section
+
+namespace Influence
+
+variable {n : ℕ}
+
+/-! ### The embedding of `Bool` into `ℝ` -/
+
+/-- The embedding `false ↦ 0`, `true ↦ 1`. -/
+def boolToReal (b : Bool) : ℝ := if b then 1 else 0
+
+@[simp] lemma boolToReal_true : boolToReal true = 1 := rfl
+
+@[simp] lemma boolToReal_false : boolToReal false = 0 := rfl
+
+@[simp] lemma boolToReal_inj {a b : Bool} : boolToReal a = boolToReal b ↔ a = b := by
+  cases a <;> cases b <;> simp
+
+lemma monotone_boolToReal : Monotone boolToReal := by
+  intro a b hab
+  cases a <;> cases b <;> simp_all [Bool.le_iff_imp]
+
+/-! ### Symmetrization over a flip -/
+
+/-- Comparing two averages pair by pair over `{x, flipᵢ x}`. -/
+lemma expect_le_of_pair (i : Fin n) {h k : (Fin n → Bool) → ℝ}
+    (hhk : ∀ x, h x + h (flipCoord i x) ≤ k x + k (flipCoord i x)) : expect h ≤ expect k := by
+  have H := expect_mono hhk
+  rw [expect_add, expect_add, expect_comp_flipCoord, expect_comp_flipCoord] at H
+  linarith
+
+lemma expect_eq_of_pair (i : Fin n) {h k : (Fin n → Bool) → ℝ}
+    (hhk : ∀ x, h x + h (flipCoord i x) = k x + k (flipCoord i x)) : expect h = expect k :=
+  le_antisymm (expect_le_of_pair i fun x ↦ (hhk x).le)
+    (expect_le_of_pair i fun x ↦ (hhk x).ge)
+
+lemma expect_lt_of_pair (i : Fin n) {h k : (Fin n → Bool) → ℝ}
+    (hhk : ∀ x, h x + h (flipCoord i x) ≤ k x + k (flipCoord i x))
+    {x₀ : Fin n → Bool} (hx₀ : h x₀ + h (flipCoord i x₀) < k x₀ + k (flipCoord i x₀)) :
+    expect h < expect k := by
+  have H : expect (fun x ↦ h x + h (flipCoord i x)) <
+      expect (fun x ↦ k x + k (flipCoord i x)) := by
+    simp only [expect]
+    exact mul_lt_mul_of_pos_left (Finset.sum_lt_sum (fun x _ ↦ hhk x)
+      ⟨x₀, Finset.mem_univ _, hx₀⟩) (by positivity)
+  rw [expect_add, expect_add, expect_comp_flipCoord, expect_comp_flipCoord] at H
+  linarith
+
+/-! ### The shift operator -/
+
+/-- The shift `Sᵢ g`: on each pair `{x, flipᵢ x}`, the point with `xᵢ = true` receives
+`g x ∨ g (flipᵢ x)` and the other one receives `g x ∧ g (flipᵢ x)`. -/
+def shift (i : Fin n) (g : (Fin n → Bool) → Bool) (x : Fin n → Bool) : Bool :=
+  if x i then g x || g (flipCoord i x) else g x && g (flipCoord i x)
+
+lemma shift_flipCoord (i : Fin n) (g : (Fin n → Bool) → Bool) (x : Fin n → Bool) :
+    shift i g (flipCoord i x) =
+      if x i then g (flipCoord i x) && g x else g (flipCoord i x) || g x := by
+  cases hx : x i <;> simp [shift, hx]
+
+/-- The shift preserves the expectation. -/
+lemma expect_shift (i : Fin n) (g : (Fin n → Bool) → Bool) :
+    expect (fun x ↦ boolToReal (shift i g x)) = expect (fun x ↦ boolToReal (g x)) := by
+  refine expect_eq_of_pair i fun x ↦ ?_
+  rw [shift_flipCoord]
+  unfold shift
+  cases x i <;> cases g x <;> cases g (flipCoord i x) <;> simp
+
+/-- The shift preserves the influence of its own coordinate. -/
+lemma influence_shift_self (i : Fin n) (g : (Fin n → Bool) → Bool) :
+    influence (fun x ↦ boolToReal (shift i g x)) i = influence (fun x ↦ boolToReal (g x)) i := by
+  refine expect_congr fun x ↦ ?_
+  simp only [boolToReal_inj]
+  rw [shift_flipCoord]
+  unfold shift
+  cases x i <;> cases g x <;> cases g (flipCoord i x) <;> simp
+
+/-- The shift does not increase the influence of the other coordinates. -/
+lemma influence_shift_le {i j : Fin n} (hij : i ≠ j) (g : (Fin n → Bool) → Bool) :
+    influence (fun x ↦ boolToReal (shift i g x)) j ≤ influence (fun x ↦ boolToReal (g x)) j := by
+  refine expect_le_of_pair i fun x ↦ ?_
+  simp only [boolToReal_inj]
+  rw [shift_flipCoord, flipCoord_comm hij.symm, shift_flipCoord]
+  unfold shift
+  rw [flipCoord_noteq j i x hij, flipCoord_comm hij]
+  cases x i <;> cases g x <;> cases g (flipCoord i x) <;> cases g (flipCoord j x) <;>
+    cases g (flipCoord j (flipCoord i x)) <;> norm_num
+
+/-- The shift does not increase the total influence. -/
+lemma totalInfluence_shift_le (i : Fin n) (g : (Fin n → Bool) → Bool) :
+    totalInfluence (fun x ↦ boolToReal (shift i g x)) ≤
+      totalInfluence (fun x ↦ boolToReal (g x)) := by
+  unfold totalInfluence
+  refine Finset.sum_le_sum fun j _ ↦ ?_
+  by_cases hij : i = j
+  · subst hij
+    exact (influence_shift_self i g).le
+  · exact influence_shift_le hij g
+
+/-! ### The potential -/
+
+/-- The number of coordinates equal to `true`. -/
+def weight (x : Fin n → Bool) : ℝ := ∑ k, boolToReal (x k)
+
+lemma weight_eq_weight_flipCoord_add_one {i : Fin n} {x : Fin n → Bool} (hx : x i = true) :
+    weight x = weight (flipCoord i x) + 1 := by
+  have h : weight x - weight (flipCoord i x) = 1 := by
+    rw [weight, weight, ← Finset.sum_sub_distrib, Finset.sum_eq_single i]
+    · simp [hx]
+    · intro k _ hk
+      rw [flipCoord_noteq i k x hk, sub_self]
+    · simp
+  linarith
+
+/-- The potential `φ(g) = E[g(x) ‖x‖]`, which strictly increases under a shift that changes `g`. -/
+def potential (g : (Fin n → Bool) → Bool) : ℝ := expect (fun x ↦ boolToReal (g x) * weight x)
+
+lemma potential_lt_potential_shift (i : Fin n) (g : (Fin n → Bool) → Bool)
+    {x₀ : Fin n → Bool} (hx₀ : x₀ i = true) (hg₀ : g x₀ = false)
+    (hg₁ : g (flipCoord i x₀) = true) : potential g < potential (shift i g) := by
+  refine expect_lt_of_pair i (fun x ↦ ?_) (x₀ := x₀) ?_
+  · rw [shift_flipCoord]
+    unfold shift
+    cases hx : x i
+    · have hw := weight_eq_weight_flipCoord_add_one (i := i) (x := flipCoord i x) (by simp [hx])
+      rw [flipCoord_flipCoord] at hw
+      rw [hw]
+      cases g x <;> cases g (flipCoord i x) <;> simp
+    · rw [weight_eq_weight_flipCoord_add_one hx]
+      cases g x <;> cases g (flipCoord i x) <;> simp
+  · rw [shift_flipCoord]
+    unfold shift
+    rw [weight_eq_weight_flipCoord_add_one hx₀, hx₀, hg₀, hg₁]
+    simp
+
+/-! ### Coordinatewise monotonicity -/
+
+/-- A Boolean function that never decreases when a coordinate is switched from `false` to `true`
+is monotone. -/
+lemma monotone_of_forall_flipCoord {g : (Fin n → Bool) → Bool}
+    (hg : ∀ i x, x i = true → g (flipCoord i x) ≤ g x) : Monotone g := by
+  intro x y hxy
+  have key : ∀ j ≤ n, g x ≤ g (mix j y x) := by
+    intro j
+    induction j with
+    | zero =>
+      intro _
+      have : mix 0 y x = x := funext fun k ↦ by simp [mix]
+      rw [this]
+    | succ j ih =>
+      intro hj
+      refine (ih (by omega)).trans ?_
+      set i : Fin n := ⟨j, by omega⟩
+      have hsucc : mix (j + 1) y x = Function.update (mix j y x) i (y i) := mix_succ i y x
+      by_cases hxyi : x i = y i
+      · rw [hsucc, ← hxyi, ← mix_apply_self i y x, Function.update_eq_self]
+      · have hxi : x i = false := by
+          have := hxy i
+          cases hx : x i <;> cases hy : y i <;> simp_all [Bool.le_iff_imp]
+        have hyi : y i = true := by
+          cases hy : y i <;> simp_all
+        have hflip : flipCoord i (mix (j + 1) y x) = mix j y x := by
+          rw [hsucc, flipCoord]
+          simp only [Function.update_self, Function.update_idem, hyi, Bool.not_true]
+          rw [← hxi, ← mix_apply_self i y x, Function.update_eq_self]
+        have := hg i (mix (j + 1) y x) (by rw [hsucc, Function.update_self, hyi])
+        rwa [hflip] at this
+  have hy : mix n y x = y := funext fun k ↦ by simp [mix]
+  simpa [hy] using key n le_rfl
+
+/-! ### BLM Theorem 9.10 -/
+
+private lemma exists_monotone_bool (f : (Fin n → Bool) → Bool) :
+    ∃ g : (Fin n → Bool) → Bool, Monotone g ∧
+      expect (fun x ↦ boolToReal (g x)) = expect (fun x ↦ boolToReal (f x)) ∧
+      totalInfluence (fun x ↦ boolToReal (g x)) ≤ totalInfluence (fun x ↦ boolToReal (f x)) := by
+  classical
+  set C : Finset ((Fin n → Bool) → Bool) := Finset.univ.filter fun g ↦
+    expect (fun x ↦ boolToReal (g x)) = expect (fun x ↦ boolToReal (f x)) ∧
+      totalInfluence (fun x ↦ boolToReal (g x)) ≤ totalInfluence (fun x ↦ boolToReal (f x))
+  have hf : f ∈ C := by simp [C]
+  obtain ⟨g, hgC, hmax⟩ := C.exists_max_image potential ⟨f, hf⟩
+  have hg := (Finset.mem_filter.mp hgC).2
+  refine ⟨g, monotone_of_forall_flipCoord fun i x hx ↦ ?_, hg⟩
+  by_contra hlt
+  have hg₀ : g x = false := by cases h : g x <;> simp_all
+  have hg₁ : g (flipCoord i x) = true := by cases h : g (flipCoord i x) <;> simp_all
+  have hS : shift i g ∈ C := by
+    simp only [C, Finset.mem_filter, Finset.mem_univ, true_and]
+    exact ⟨(expect_shift i g).trans hg.1, (totalInfluence_shift_le i g).trans hg.2⟩
+  exact (hmax _ hS).not_gt (potential_lt_potential_shift i g hx hg₀ hg₁)
+
+/-- **BLM Theorem 9.10.** Every Boolean function on the hypercube can be replaced by a monotone
+Boolean function with the same expectation and no larger total influence. -/
+theorem exists_monotone {f : (Fin n → Bool) → ℝ} (hf : ∀ x, f x = 0 ∨ f x = 1) :
+    ∃ g : (Fin n → Bool) → ℝ, (∀ x, g x = 0 ∨ g x = 1) ∧ Monotone g ∧
+      expect g = expect f ∧ totalInfluence g ≤ totalInfluence f := by
+  have hfb : (fun x ↦ boolToReal (decide (f x = 1))) = f := by
+    funext x
+    rcases hf x with h | h <;> simp [h]
+  obtain ⟨g, hmono, hexp, hinf⟩ := exists_monotone_bool fun x ↦ decide (f x = 1)
+  rw [hfb] at hexp hinf
+  refine ⟨fun x ↦ boolToReal (g x), fun x ↦ ?_, monotone_boolToReal.comp hmono, hexp, hinf⟩
+  cases h : g x <;> simp [h]
+
+example (f : (Fin 3 → Bool) → ℝ) (hf : ∀ x, f x = 0 ∨ f x = 1) :
+    ∃ g : (Fin 3 → Bool) → ℝ, (∀ x, g x = 0 ∨ g x = 1) ∧ Monotone g ∧
+      expect g = expect f ∧ totalInfluence g ≤ totalInfluence f :=
+  exists_monotone hf
+
+end Influence