From c7dc89c541749aa11195c8966d32d6401a133047 Mon Sep 17 00:00:00 2001 From: Vincent Liew Date: Sun, 1 Nov 2026 12:41:42 -0800 Subject: [PATCH] feat(boolean-analysis): coordinate operators and stable influences MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add O'Donnell's coordinate expectation Eᵢ, coordinate Laplacian Lᵢ and Laplacian L (Defs 2.23, 2.25, 2.36) with their Fourier coefficients, Lᵢ f = χ_{i} Dᵢ f, ⟨f, Lᵢ f⟩ = Infᵢ[f] and ⟨f, L f⟩ = I[f] (Props 2.24, 2.26, 2.37). Add ρ-stable influences Stab_ρ[Dᵢ f] and their total (Def 2.52), their Fourier formulas, δ·I^{(1−δ)}[f] ≤ 1 for Boolean f (Exercise 2.45), and that at most 1/(δε) coordinates have (1−δ)-stable influence at least ε (Prop 2.54). Part of #2131. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../BooleanAnalysis/CoordinateOperators.lean | 139 +++++++++++++ .../BooleanAnalysis/StableInfluence.lean | 184 ++++++++++++++++++ .../BooleanAnalysisStableInfluence.lean | 52 +++++ 4 files changed, 377 insertions(+) create mode 100644 Complexity/Foundations/BooleanAnalysis/CoordinateOperators.lean create mode 100644 Complexity/Foundations/BooleanAnalysis/StableInfluence.lean create mode 100644 ComplexityTests/BooleanAnalysisStableInfluence.lean diff --git a/Complexity.lean b/Complexity.lean index b90ba2e793..db52be408c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2872,6 +2872,7 @@ public import Complexity.Foundations.BooleanAnalysis.Bernoulli public import Complexity.Foundations.BooleanAnalysis.Bonami public import Complexity.Foundations.BooleanAnalysis.BucketWeight public import Complexity.Foundations.BooleanAnalysis.Convolution +public import Complexity.Foundations.BooleanAnalysis.CoordinateOperators public import Complexity.Foundations.BooleanAnalysis.CoordinateSampling public import Complexity.Foundations.BooleanAnalysis.Decomposition public import Complexity.Foundations.BooleanAnalysis.Degree @@ -2919,6 +2920,7 @@ public import Complexity.Foundations.BooleanAnalysis.SparseEquations.Degree public import Complexity.Foundations.BooleanAnalysis.SparseHermiteRecovery public import Complexity.Foundations.BooleanAnalysis.SparseIncidence public import Complexity.Foundations.BooleanAnalysis.SparseReplacementDesign +public import Complexity.Foundations.BooleanAnalysis.StableInfluence public import Complexity.Foundations.BooleanAnalysis.Symmetrization public import Complexity.Foundations.BooleanAnalysis.Tribes public import Complexity.Foundations.Combinatorics.Additive.SumsetCover diff --git a/Complexity/Foundations/BooleanAnalysis/CoordinateOperators.lean b/Complexity/Foundations/BooleanAnalysis/CoordinateOperators.lean new file mode 100644 index 0000000000..3f3f5bdf2e --- /dev/null +++ b/Complexity/Foundations/BooleanAnalysis/CoordinateOperators.lean @@ -0,0 +1,139 @@ +/- +Copyright (c) 2026 Vincent Liew. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Liew +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.BooleanAnalysis.Influence +import Complexity.Foundations.BooleanAnalysis.Decomposition +import Complexity.Foundations.Data.Finset.SymmDiff +import Mathlib.Tactic.Ring + +/-! +# Coordinate expectations and Laplacians + +The *expectation over coordinate `i`* of a real function on the cube is its average over bit `i`, +`Eᵢ f x = (f (x with xᵢ = false) + f (x with xᵢ = true)) / 2` (`BitString.coordExpect`), and the +*coordinate Laplacian* is `Lᵢ f = f - Eᵢ f` (`BitString.coordLaplacian`) +[O'Donnell, Definitions 2.23 and 2.25][ODonnell2014]. The Laplacian is `χ_{i}` times the +derivative in `i` (`BitString.coordLaplacian_eq_chi_mul_derivative`); in Fourier terms `Eᵢ` +keeps the coefficients on the sets avoiding `i` and `Lᵢ` those on the sets containing `i` +(`BitString.fourierCoeff_coordExpect`, `BitString.fourierCoeff_coordLaplacian`), and +`⟨f, Lᵢ f⟩ = Infᵢ[f]` (`BitString.expect_mul_coordLaplacian`); averaging over `i` preserves the +expectation (`BitString.expect_coordExpect`) +[O'Donnell, Propositions 2.24 and 2.26][ODonnell2014]. + +The *Laplacian* `L = ∑ᵢ Lᵢ` (`BitString.laplacian`) multiplies the coefficient on `S` by `|S|` +(`BitString.fourierCoeff_laplacian`), so `⟨f, L f⟩ = I[f]` (`BitString.expect_mul_laplacian`) +[O'Donnell, Definition 2.36 and Proposition 2.37][ODonnell2014]. + +## Main definitions + +* `Cslib.BitString.coordExpect`, `Cslib.BitString.coordLaplacian`: the expectation and the + Laplacian along one coordinate. +* `Cslib.BitString.laplacian`: the Laplacian. + +## Main results + +* `Cslib.BitString.coordLaplacian_eq_chi_mul_derivative`: `Lᵢ f = χ_{i} Dᵢ f`. +* `Cslib.BitString.fourierCoeff_coordExpect`, `Cslib.BitString.fourierCoeff_coordLaplacian`, + `Cslib.BitString.fourierCoeff_laplacian`: the Fourier coefficients of the three operators. +* `Cslib.BitString.expect_mul_coordLaplacian`, `Cslib.BitString.expect_mul_laplacian`: + `⟨f, Lᵢ f⟩ = Infᵢ[f]` and `⟨f, L f⟩ = I[f]`. + +## References + +* [R. O'Donnell, *Analysis of Boolean Functions*][ODonnell2014] +-/ + +public section + +namespace Cslib.BitString + +open Finset Function +open scoped BigOperators + +variable {ι : Type*} [DecidableEq ι] + +/-- The expectation `Eᵢ f` of `f` over coordinate `i`: its average over bit `i` +[O'Donnell, Definition 2.23][ODonnell2014]. -/ +@[expose] noncomputable def coordExpect (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ := + (f (update x i false) + f (update x i true)) / 2 + +/-- The coordinate Laplacian `Lᵢ f = f - Eᵢ f` [O'Donnell, Definition 2.25][ODonnell2014]. -/ +@[expose] noncomputable def coordLaplacian (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ := + f x - coordExpect i f x + +/-- **The coordinate Laplacian is `χ_{i}` times the derivative**: `Lᵢ f = χ_{i} Dᵢ f` +[O'Donnell, Proposition 2.26][ODonnell2014]. -/ +theorem coordLaplacian_eq_chi_mul_derivative (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) : + coordLaplacian i f x = chi ℝ {i} x * derivative i f x := + sub_eq_of_eq_add' (eq_add_chi_mul_derivative i f x) + +/-- A function is the sum of its coordinate expectation and its coordinate Laplacian. -/ +theorem coordExpect_add_coordLaplacian (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) : + coordExpect i f x + coordLaplacian i f x = f x := + add_sub_cancel _ _ + +variable [Fintype ι] + +/-- **The Fourier coefficients of a coordinate Laplacian**: `Lᵢ f` keeps the coefficients of `f` +on the sets containing `i` [O'Donnell, Proposition 2.26][ODonnell2014]. -/ +theorem fourierCoeff_coordLaplacian (i : ι) (f : (ι → Bool) → ℝ) (S : Finset ι) : + fourierCoeff (coordLaplacian i f) S = if i ∈ S then fourierCoeff f S else 0 := by + rw [funext (coordLaplacian_eq_chi_mul_derivative i f), fourierCoeff_chi_mul, + fourierCoeff_derivative, symmDiff_comm, symmDiff_singleton_eq] + by_cases hi : i ∈ S <;> simp [hi] + +/-- **The Fourier coefficients of a coordinate expectation**: `Eᵢ f` keeps the coefficients of `f` +on the sets avoiding `i` [O'Donnell, Proposition 2.24][ODonnell2014]. -/ +theorem fourierCoeff_coordExpect (i : ι) (f : (ι → Bool) → ℝ) (S : Finset ι) : + fourierCoeff (coordExpect i f) S = if i ∈ S then 0 else fourierCoeff f S := by + have h : coordExpect i f = fun x => f x - coordLaplacian i f x := + funext fun x => by rw [coordLaplacian]; ring + rw [h, fourierCoeff_sub, fourierCoeff_coordLaplacian] + split_ifs <;> ring + +/-- Averaging over coordinate `i` preserves the expectation: `𝔼 Eᵢ f = 𝔼 f`. -/ +theorem expect_coordExpect (i : ι) (f : (ι → Bool) → ℝ) : + 𝔼 x, coordExpect i f x = 𝔼 x, f x := by + simp only [coordExpect, div_eq_mul_inv, ← expect_mul, expect_update_false_add_update_true] + ring + +/-- **The coordinate Laplacian and the influence**: `⟨f, Lᵢ f⟩ = Infᵢ[f]` +[O'Donnell, Proposition 2.26][ODonnell2014]. -/ +theorem expect_mul_coordLaplacian (i : ι) (f : (ι → Bool) → ℝ) : + 𝔼 x, f x * coordLaplacian i f x = influence i f := by + rw [expect_mul_eq_sum_fourierCoeff_mul, influence_eq_sum_fourierCoeff_sq, sum_filter] + refine sum_congr rfl fun S _ => ?_ + rw [fourierCoeff_coordLaplacian] + split_ifs <;> ring + +/-- The Laplacian `L f = ∑ᵢ Lᵢ f` [O'Donnell, Definition 2.36][ODonnell2014]. -/ +@[expose] noncomputable def laplacian (f : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ := + ∑ i, coordLaplacian i f x + +/-- **The Fourier coefficients of the Laplacian**: `L f` multiplies the coefficient of `f` on `S` +by `|S|` [O'Donnell, Proposition 2.37][ODonnell2014]. -/ +theorem fourierCoeff_laplacian (f : (ι → Bool) → ℝ) (S : Finset ι) : + fourierCoeff (laplacian f) S = #S * fourierCoeff f S := by + have h : fourierCoeff (laplacian f) S = ∑ i, fourierCoeff (coordLaplacian i f) S := by + simp only [laplacian, fourierCoeff, sum_mul] + rw [expect_sum_comm] + rw [h] + simp only [fourierCoeff_coordLaplacian] + rw [sum_ite_mem, univ_inter, sum_const, nsmul_eq_mul] + +/-- **The Laplacian and the total influence**: `⟨f, L f⟩ = I[f]` +[O'Donnell, Proposition 2.37][ODonnell2014]. -/ +theorem expect_mul_laplacian (f : (ι → Bool) → ℝ) : + 𝔼 x, f x * laplacian f x = totalInfluence f := by + rw [expect_mul_eq_sum_fourierCoeff_mul, totalInfluence_eq_sum_card_mul_fourierCoeff_sq] + refine sum_congr rfl fun S _ => ?_ + rw [fourierCoeff_laplacian] + ring + +end Cslib.BitString diff --git a/Complexity/Foundations/BooleanAnalysis/StableInfluence.lean b/Complexity/Foundations/BooleanAnalysis/StableInfluence.lean new file mode 100644 index 0000000000..557af36873 --- /dev/null +++ b/Complexity/Foundations/BooleanAnalysis/StableInfluence.lean @@ -0,0 +1,184 @@ +/- +Copyright (c) 2026 Vincent Liew. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Liew +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.BooleanAnalysis.Noise +import Complexity.Foundations.Data.Finset.Expect +import Complexity.Foundations.Data.Finset.Markov +import Mathlib.Algebra.Ring.GeomSum +import Mathlib.Tactic.Linarith + +/-! +# Stable influences + +The `ρ`-*stable influence* of coordinate `i` on a real function `f` is the noise stability of its +derivative, `Infᵢ^{(ρ)}[f] = Stab_ρ[Dᵢ f]` (`BitString.stableInfluence`), and the total +`ρ`-stable influence is their sum (`BitString.totalStableInfluence`) +[O'Donnell, Definition 2.52][ODonnell2014]. In Fourier terms, +`Infᵢ^{(ρ)}[f] = ∑_{S ∋ i} ρ ^ (|S| - 1) f̂(S) ^ 2` (`BitString.stableInfluence_eq_sum`) and +`I^{(ρ)}[f] = ∑_S |S| ρ ^ (|S| - 1) f̂(S) ^ 2` (`BitString.totalStableInfluence_eq_sum`) +[O'Donnell, Fact 2.53][ODonnell2014], so at `ρ = 1` they are the influence and the total +influence (`BitString.stableInfluence_one`, `BitString.totalStableInfluence_one`). + +Damping the high degrees caps the total: since `k δ (1 - δ) ^ (k - 1) ≤ 1` for every `k` +[O'Donnell, Exercise 2.45][ODonnell2014], `δ I^{(1 - δ)}[f] ≤ Var[f]` for `0 ≤ δ ≤ 1` +(`BitString.mul_totalStableInfluence_le`). Hence `δ ε N ≤ Var[f]`, where `N` counts the +coordinates of `(1 - δ)`-stable influence at least `ε` +(`BitString.mul_card_filter_le_stableInfluence_le`); for a function of variance at most one, such +as a Boolean function read as signs, at most `1 / (δ ε)` coordinates have `(1 - δ)`-stable +influence at least `ε` [O'Donnell, Proposition 2.54][ODonnell2014], in contrast with ordinary +influences, which can all be large at once. + +## Main definitions + +* `Cslib.BitString.stableInfluence`, `Cslib.BitString.totalStableInfluence`: the stable + influences. + +## Main results + +* `Cslib.BitString.stableInfluence_eq_sum`, `Cslib.BitString.totalStableInfluence_eq_sum`: their + Fourier formulas. +* `Cslib.BitString.stableInfluence_one`, `Cslib.BitString.totalStableInfluence_one`: at `ρ = 1` + they are the influence and the total influence. +* `Cslib.BitString.mul_totalStableInfluence_le`, + `Cslib.BitString.mul_totalStableInfluence_signVal_le_one`: `δ I^{(1 - δ)}[f] ≤ Var[f]`, which is + at most one for Boolean `f`. +* `Cslib.BitString.mul_card_filter_le_stableInfluence_le`, + `Cslib.BitString.mul_card_filter_le_stableInfluence_signVal_le_one`: few coordinates have large + stable influence. + +## References + +* [R. O'Donnell, *Analysis of Boolean Functions*][ODonnell2014] +-/ + +public section + +namespace Cslib.BitString + +open Finset +open scoped BigOperators + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- The `ρ`-stable influence `Infᵢ^{(ρ)}[f] = Stab_ρ[Dᵢ f]` of coordinate `i` on `f` +[O'Donnell, Definition 2.52][ODonnell2014]. -/ +noncomputable def stableInfluence (ρ : ℝ) (i : ι) (f : (ι → Bool) → ℝ) : ℝ := + noiseStability ρ (derivative i f) + +/-- The total `ρ`-stable influence `I^{(ρ)}[f] = ∑ᵢ Infᵢ^{(ρ)}[f]` +[O'Donnell, Definition 2.52][ODonnell2014]. -/ +noncomputable def totalStableInfluence (ρ : ℝ) (f : (ι → Bool) → ℝ) : ℝ := + ∑ i, stableInfluence ρ i f + +/-- **The Fourier formula for the stable influence**: +`Infᵢ^{(ρ)}[f] = ∑_{S ∋ i} ρ ^ (|S| - 1) f̂(S) ^ 2` [O'Donnell, Definition 2.52][ODonnell2014]. -/ +theorem stableInfluence_eq_sum (ρ : ℝ) (i : ι) (f : (ι → Bool) → ℝ) : + stableInfluence ρ i f = ∑ S with i ∈ S, ρ ^ (#S - 1) * fourierCoeff f S ^ 2 := by + rw [stableInfluence, noiseStability_eq_sum, sum_filter_mem_eq_sum_filter_notMem i, sum_filter] + refine sum_congr rfl fun T _ => ?_ + rw [fourierCoeff_derivative] + split_ifs with hT + · simp + · rw [card_insert_of_notMem hT, Nat.add_sub_cancel] + +/-- At `ρ = 1` the stable influence is the influence. -/ +theorem stableInfluence_one (i : ι) (f : (ι → Bool) → ℝ) : + stableInfluence 1 i f = influence i f := by + rw [stableInfluence, noiseStability_one, influence] + +/-- Stable influences at a nonnegative rate are nonnegative. -/ +theorem stableInfluence_nonneg {ρ : ℝ} (hρ : 0 ≤ ρ) (i : ι) (f : (ι → Bool) → ℝ) : + 0 ≤ stableInfluence ρ i f := by + rw [stableInfluence_eq_sum] + exact sum_nonneg fun _ _ => mul_nonneg (pow_nonneg hρ _) (sq_nonneg _) + +/-- At `ρ = 1` the total stable influence is the total influence. -/ +theorem totalStableInfluence_one (f : (ι → Bool) → ℝ) : + totalStableInfluence 1 f = totalInfluence f := by + simp only [totalStableInfluence, stableInfluence_one, totalInfluence] + +/-- The total stable influence at a nonnegative rate is nonnegative. -/ +theorem totalStableInfluence_nonneg {ρ : ℝ} (hρ : 0 ≤ ρ) (f : (ι → Bool) → ℝ) : + 0 ≤ totalStableInfluence ρ f := + sum_nonneg fun i _ => stableInfluence_nonneg hρ i f + +/-- **The Fourier formula for the total stable influence**: +`I^{(ρ)}[f] = ∑_S |S| ρ ^ (|S| - 1) f̂(S) ^ 2`, the second equality of +[O'Donnell, Fact 2.53][ODonnell2014] written per set rather than per degree. -/ +theorem totalStableInfluence_eq_sum (ρ : ℝ) (f : (ι → Bool) → ℝ) : + totalStableInfluence ρ f = ∑ S, (#S : ℝ) * ρ ^ (#S - 1) * fourierCoeff f S ^ 2 := by + simp only [totalStableInfluence, stableInfluence_eq_sum, sum_filter] + rw [sum_comm] + refine sum_congr rfl fun S _ => ?_ + rw [sum_ite_mem, univ_inter, sum_const, nsmul_eq_mul] + ring + +/-- `k δ (1 - δ) ^ (k - 1) ≤ 1` for `0 ≤ δ ≤ 1` [O'Donnell, Exercise 2.45][ODonnell2014]: the +`k` terms of the geometric sum `δ ∑_{j < k} (1 - δ) ^ j = 1 - (1 - δ) ^ k` are each at least +`δ (1 - δ) ^ (k - 1)`. -/ +private theorem natCast_mul_mul_pow_le_one {δ : ℝ} (h₀ : 0 ≤ δ) (h₁ : δ ≤ 1) (k : ℕ) : + k * δ * (1 - δ) ^ (k - 1) ≤ 1 := by + rcases k with _ | k + · simp + have hgeom : (∑ j ∈ range (k + 1), (1 - δ) ^ j) * δ = 1 - (1 - δ) ^ (k + 1) := by + simpa only [sub_sub_cancel] using geom_sum_mul_neg (1 - δ) (k + 1) + have hsum : ((k + 1 : ℕ) : ℝ) * (1 - δ) ^ k ≤ ∑ j ∈ range (k + 1), (1 - δ) ^ j := by + have := sum_le_sum fun j (hj : j ∈ range (k + 1)) => + pow_le_pow_of_le_one (by linarith : (0 : ℝ) ≤ 1 - δ) (by linarith) + (Nat.lt_succ_iff.1 (mem_range.1 hj)) + simpa only [sum_const, card_range, nsmul_eq_mul] using this + have hpow : 0 ≤ (1 - δ) ^ (k + 1) := pow_nonneg (by linarith) _ + rw [Nat.add_sub_cancel] + nlinarith [mul_le_mul_of_nonneg_right hsum h₀] + +/-- **Damping caps the total stable influence**: for `0 ≤ δ ≤ 1`, `δ I^{(1 - δ)}[f]` is at most the +variance of `f` [O'Donnell, proof of Proposition 2.54][ODonnell2014]. -/ +theorem mul_totalStableInfluence_le {δ : ℝ} (h₀ : 0 ≤ δ) (h₁ : δ ≤ 1) (f : (ι → Bool) → ℝ) : + δ * totalStableInfluence (1 - δ) f ≤ 𝔼 x, (f x - 𝔼 y, f y) ^ 2 := by + rw [totalStableInfluence_eq_sum, mul_sum, expect_sub_expect_sq_eq_sum_fourierCoeff_sq, sum_filter] + refine sum_le_sum fun S _ => ?_ + by_cases hS : S = ∅ + · simp [hS] + · simp only [hS, ne_eq, not_false_eq_true, ↓reduceIte] + calc δ * (#S * (1 - δ) ^ (#S - 1) * fourierCoeff f S ^ 2) + = #S * δ * (1 - δ) ^ (#S - 1) * fourierCoeff f S ^ 2 := by ring + _ ≤ fourierCoeff f S ^ 2 := + mul_le_of_le_one_left (sq_nonneg _) (natCast_mul_mul_pow_le_one h₀ h₁ _) + +/-- **Damping caps the total stable influence of a Boolean function**: read as signs, with +`0 ≤ δ ≤ 1`, `δ I^{(1 - δ)}[f] ≤ 1` [O'Donnell, proof of Proposition 2.54][ODonnell2014]. -/ +theorem mul_totalStableInfluence_signVal_le_one {δ : ℝ} (h₀ : 0 ≤ δ) (h₁ : δ ≤ 1) + (f : (ι → Bool) → Bool) : + δ * totalStableInfluence (1 - δ) (fun x => signVal (f x)) ≤ 1 := + (mul_totalStableInfluence_le h₀ h₁ _).trans (expect_sub_expect_sq_signVal_le_one f) + +/-- **Few coordinates have large stable influence**: for `0 ≤ δ ≤ 1` and any `ε`, the number `N` +of coordinates of `(1 - δ)`-stable influence at least `ε` satisfies `δ ε N ≤ Var[f]`. For +`δ, ε > 0` and `Var[f] ≤ 1` this is [O'Donnell, Proposition 2.54][ODonnell2014], `N ≤ 1 / (δ ε)`, +under weaker hypotheses on `δ` and `ε`. -/ +theorem mul_card_filter_le_stableInfluence_le {δ : ℝ} (h₀ : 0 ≤ δ) (h₁ : δ ≤ 1) (ε : ℝ) + (f : (ι → Bool) → ℝ) : + δ * ε * #{i | ε ≤ stableInfluence (1 - δ) i f} ≤ 𝔼 x, (f x - 𝔼 y, f y) ^ 2 := by + have hcount : (#{i | ε ≤ stableInfluence (1 - δ) i f} : ℝ) * ε ≤ totalStableInfluence (1 - δ) f := + card_filter_mul_le_sum _ _ _ (fun i _ => stableInfluence_nonneg (sub_nonneg.2 h₁) i f) + fun _ _ h => h + calc δ * ε * #{i | ε ≤ stableInfluence (1 - δ) i f} + = δ * (#{i | ε ≤ stableInfluence (1 - δ) i f} * ε) := by ring + _ ≤ δ * totalStableInfluence (1 - δ) f := mul_le_mul_of_nonneg_left hcount h₀ + _ ≤ 𝔼 x, (f x - 𝔼 y, f y) ^ 2 := mul_totalStableInfluence_le h₀ h₁ f + +/-- **Few coordinates have large stable influence on a Boolean function**: read as signs, with +`0 ≤ δ ≤ 1`, the number `N` of coordinates of `(1 - δ)`-stable influence at least `ε` satisfies +`δ ε N ≤ 1`, so `N ≤ 1 / (δ ε)` for `δ, ε > 0` [O'Donnell, Proposition 2.54][ODonnell2014]. -/ +theorem mul_card_filter_le_stableInfluence_signVal_le_one {δ : ℝ} (h₀ : 0 ≤ δ) (h₁ : δ ≤ 1) + (ε : ℝ) (f : (ι → Bool) → Bool) : + δ * ε * #{i | ε ≤ stableInfluence (1 - δ) i (fun x => signVal (f x))} ≤ 1 := + (mul_card_filter_le_stableInfluence_le h₀ h₁ ε _).trans (expect_sub_expect_sq_signVal_le_one f) + +end Cslib.BitString diff --git a/ComplexityTests/BooleanAnalysisStableInfluence.lean b/ComplexityTests/BooleanAnalysisStableInfluence.lean new file mode 100644 index 0000000000..2c4a41e9aa --- /dev/null +++ b/ComplexityTests/BooleanAnalysisStableInfluence.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2026 Vincent Liew. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Liew +-/ + +import Complexity.Foundations.BooleanAnalysis.CoordinateOperators +import Complexity.Foundations.BooleanAnalysis.StableInfluence + +/-! # Coordinate operators and stable influences on small cubes + +The character `χ_{0,1}` of two of three coordinates is killed by the expectation over coordinate +`0` and kept by the coordinate Laplacian, and the Laplacian scales it by two, so +`⟨χ, L χ⟩ = I[χ] = 2`. Its `ρ`-stable influence at coordinate `0` is `ρ`, interpolating between +zero at `ρ = 0` and its influence one at `ρ = 1`. Proposition 2.54 applies to a dictator at +`δ = ε = 1 / 2`. +-/ + +namespace ComplexityTests.BooleanAnalysisStableInfluence + +open Cslib Cslib.BitString Finset +open scoped BigOperators + +/-- The character of the first two of three coordinates. -/ +noncomputable abbrev χ₀₁ : (Fin 3 → Bool) → ℝ := chi ℝ ({0, 1} : Finset (Fin 3)) + +-- `E₀` kills `χ_{0,1}` and `L₀` keeps it. +example : fourierCoeff (coordExpect 0 χ₀₁) {0, 1} = 0 ∧ + fourierCoeff (coordLaplacian 0 χ₀₁) {0, 1} = 1 := by + rw [fourierCoeff_coordExpect, fourierCoeff_coordLaplacian, fourierCoeff_chi] + simp + +-- `⟨χ, L χ⟩` is the total influence `2` of the character. +example : 𝔼 x, χ₀₁ x * laplacian χ₀₁ x = 2 := by + rw [expect_mul_laplacian, totalInfluence_chi] + rfl + +-- The `ρ`-stable influence of coordinate `0` on `χ_{0,1}` is `ρ`. +example (ρ : ℝ) : stableInfluence ρ 0 χ₀₁ = ρ := by + rw [stableInfluence_eq_sum] + simp only [fourierCoeff_chi, ite_pow, one_pow, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, + zero_pow, mul_ite, mul_one, mul_zero] + rw [sum_ite_eq] + simp + +-- Proposition 2.54 for a dictator at `δ = ε = 1 / 2`. +example : (1 / 2 : ℝ) * (1 / 2) * + #{i | (1 / 2 : ℝ) ≤ stableInfluence (1 - 1 / 2) i (fun x : Fin 3 → Bool => signVal (x 0))} ≤ + 1 := + mul_card_filter_le_stableInfluence_signVal_le_one (by norm_num) (by norm_num) _ _ + +end ComplexityTests.BooleanAnalysisStableInfluence