From f74c511f4bc5e7e086d826b98c2de5c5a30bc08a Mon Sep 17 00:00:00 2001 From: AlexeyMilovanov Date: Mon, 20 Apr 2026 18:25:05 +0100 Subject: [PATCH 1/5] feat(AnalysisOfBooleanFunctions): formalize O'Donnell's Degree-1 Fourier Weight Conjecture --- .../Degree1Weight.lean | 42 ++++++++ .../Analysis/BooleanFunction.lean | 100 ++++++++++++++++++ 2 files changed, 142 insertions(+) create mode 100644 FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean create mode 100644 FormalConjecturesForMathlib/Analysis/BooleanFunction.lean diff --git a/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean b/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean new file mode 100644 index 0000000000..79b8892522 --- /dev/null +++ b/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean @@ -0,0 +1,42 @@ +/- +Copyright 2026 The Formal Conjectures Authors. +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + https://www.apache.org/licenses/LICENSE-2.0 +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ +import FormalConjecturesForMathlib.Analysis.BooleanFunction +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic +import FormalConjectures.Util.Attributes.Basic +import FormalConjectures.Util.Attributes.AMS + +/-! +# Degree-1 Fourier Weight Conjecture + +Author: Alexey Milovanov + +This file states the Degree-1 Fourier Weight Conjecture (Conjecture 5.3) +from Ryan O'Donnell's "Analysis of Boolean Functions" (2014). + +The conjecture asserts that for any unbiased Linear Threshold Function (LTF), +the Fourier weight at degree at most 1 is at least $2/\pi$. +This lower bound is asymptotically tight and is achieved by the +Majority function as $n \to \infty$. +-/ + +open Finset BooleanAnalysis + +/-- English version: "If `f : 𝔽₂ⁿ β†’ {-1, 1}` is an unbiased linear threshold function, +then its Fourier weight at degree at most 1 is at least `2/Ο€`." -/ +@[category research open, AMS 68, AMS 42] +theorem degree_1_weight_conjecture (n : β„•) (f : BooleanFunction n) + (hf_bool : IsBooleanValued f) + (h_ltf : IsLTF f) + (h_unbiased : IsUnbiased f) : + 𝐖_≀ f 1 β‰₯ 2 / Real.pi := by + sorry diff --git a/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean b/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean new file mode 100644 index 0000000000..875a7d4bd5 --- /dev/null +++ b/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean @@ -0,0 +1,100 @@ +/- +Copyright 2026 The Formal Conjectures Authors. +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + https://www.apache.org/licenses/LICENSE-2.0 +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ +import Mathlib.Algebra.BigOperators.Expect +import Mathlib.Data.ZMod.Basic +import Mathlib.Data.Real.Basic +import Mathlib.Algebra.Algebra.Pi + +/-! +# Analysis of Boolean Functions: Basic Definitions + +Author: Alexey Milovanov + +This module provides the foundational definitions for the analysis of Boolean functions, +following the conventions of Ryan O'Donnell's book "Analysis of Boolean Functions". +It includes the definition of the Hamming cube, Fourier expansion basics, and +linear threshold functions (LTFs). +-/ + +open Finset BigOperators + +namespace BooleanAnalysis + +variable {n : β„•} + +/-! ### Basic types and algebraic structure -/ + +/-- The Hamming cube `{0, 1}^n`, represented as functions from `Fin n` to `ZMod 2`. -/ +abbrev Cube (n : β„•) := Fin n β†’ ZMod 2 + +/-- A real-valued Boolean function on the Hamming cube. -/ +def BooleanFunction (n : β„•) := Cube n β†’ ℝ + +instance : CommRing (BooleanFunction n) := inferInstanceAs (CommRing (Cube n β†’ ℝ)) +instance : Algebra ℝ (BooleanFunction n) := inferInstanceAs (Algebra ℝ (Cube n β†’ ℝ)) + +instance : FunLike (BooleanFunction n) (Cube n) ℝ where + coe f := f + coe_injective' _ _ h := h + +/-! ### Encoding and parity functions -/ + +/-- A Boolean function is considered Boolean-valued if its range is `{-1, 1}`. -/ +def IsBooleanValued (f : BooleanFunction n) : Prop := βˆ€ x, f x = 1 ∨ f x = -1 + +/-- The standard character encoding mapping `0 ↦ 1` and `1 ↦ -1`. -/ +def chi : ZMod 2 β†’ ℝ := fun b => if b = 0 then 1 else -1 + +/-- The parity function `Ο‡_S(x) = ∏_{i ∈ S} Ο‡(x_i)`. -/ +noncomputable def parityFun (S : Finset (Fin n)) : BooleanFunction n := + fun x => ∏ i ∈ S, chi (x i) + +scoped prefix:max "Ο‡" => parityFun + +/-! ### Expectation -/ + +/-- The uniform expectation of a Boolean function over the Hamming cube. -/ +noncomputable def expect (f : BooleanFunction n) : ℝ := Finset.univ.expect f + +scoped notation "𝔼[" f "]" => expect f + +/-- A Boolean function is unbiased if its expected value is exactly zero. -/ +def IsUnbiased (f : BooleanFunction n) : Prop := 𝔼[f] = 0 + +/-! ### Fourier coefficients and weights -/ + +/-- The Fourier coefficient of `f` on the set `S`, defined directly as `𝔼[f Β· Ο‡_S]`. -/ +noncomputable def fourierCoeff (f : BooleanFunction n) (S : Finset (Fin n)) : ℝ := + 𝔼[fun x => f x * (Ο‡ S) x] + +scoped notation "𝓕" => fourierCoeff + +/-- The Fourier weight of `f` on the set `S`, defined as the squared Fourier coefficient. -/ +noncomputable def fourierWeight (f : BooleanFunction n) (S : Finset (Fin n)) : ℝ := + 𝓕 f S ^ 2 + +/-- The cumulative Fourier weight of `f` up to degree `k`, denoted as `W^{≀k}[f]`. -/ +noncomputable def fourierWeightUpToDegree (f : BooleanFunction n) (k : β„•) : ℝ := + βˆ‘ S ∈ Finset.univ.filter (fun S : Finset (Fin n) => S.card ≀ k), fourierWeight f S + +scoped notation "𝐖_≀" => fourierWeightUpToDegree + +/-! ### Linear threshold functions -/ + +/-- A function is a Linear Threshold Function (LTF) if it can be represented +as the sign of a degree-1 polynomial over the reals. -/ +def IsLTF (f : BooleanFunction n) : Prop := + βˆƒ (w : Fin n β†’ ℝ) (ΞΈ : ℝ), βˆ€ x : Cube n, + f x = if (βˆ‘ i, w i * chi (x i)) β‰₯ ΞΈ then 1 else -1 + +end BooleanAnalysis From 74f7cc589d460dd7fbadaebc416f9f632f1557e1 Mon Sep 17 00:00:00 2001 From: AlexeyMilovanov Date: Mon, 20 Apr 2026 18:29:39 +0100 Subject: [PATCH 2/5] docs: add Alexey Milovanov to AUTHORS --- AUTHORS | 1 + 1 file changed, 1 insertion(+) diff --git a/AUTHORS b/AUTHORS index ee97b877c3..2c326db0c7 100644 --- a/AUTHORS +++ b/AUTHORS @@ -9,6 +9,7 @@ Google LLC # Please keep the list sorted alphabetically Abel DoΓ±ate Aditya Ramabadran +Alexey Milovanov Amogh Parab Anirudh Rao Anthony Wang From 47e296a00b3d2e3a720993298d471e5177aaf9e6 Mon Sep 17 00:00:00 2001 From: AlexeyMilovanov Date: Mon, 4 May 2026 21:28:04 +0100 Subject: [PATCH 3/5] fix: match exact copyright header format and year from existing files --- .../Books/AnalysisOfBooleanFunctions/Degree1Weight.lean | 5 ++++- FormalConjecturesForMathlib/Analysis/BooleanFunction.lean | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean b/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean index 79b8892522..3442dbda59 100644 --- a/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean +++ b/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean @@ -1,9 +1,12 @@ /- -Copyright 2026 The Formal Conjectures Authors. +Copyright 2025 The Formal Conjectures Authors. + Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at + https://www.apache.org/licenses/LICENSE-2.0 + Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. diff --git a/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean b/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean index 875a7d4bd5..43ae9e0abb 100644 --- a/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean +++ b/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean @@ -1,9 +1,12 @@ /- -Copyright 2026 The Formal Conjectures Authors. +Copyright 2025 The Formal Conjectures Authors. + Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at + https://www.apache.org/licenses/LICENSE-2.0 + Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. From 1154b4d2d6b015fae5ab51046bbadae381d968dc Mon Sep 17 00:00:00 2001 From: AlexeyMilovanov Date: Sun, 10 May 2026 00:43:24 +0100 Subject: [PATCH 4/5] fix: add module declaration, public imports, and expose section --- .../Analysis/BooleanFunction.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean b/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean index 43ae9e0abb..87cdcf9ceb 100644 --- a/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean +++ b/FormalConjecturesForMathlib/Analysis/BooleanFunction.lean @@ -13,11 +13,12 @@ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ -import Mathlib.Algebra.BigOperators.Expect -import Mathlib.Data.ZMod.Basic -import Mathlib.Data.Real.Basic -import Mathlib.Algebra.Algebra.Pi +module +public import Mathlib.Algebra.BigOperators.Expect +public import Mathlib.Data.ZMod.Basic +public import Mathlib.Data.Real.Basic +public import Mathlib.Algebra.Algebra.Pi /-! # Analysis of Boolean Functions: Basic Definitions @@ -29,6 +30,8 @@ It includes the definition of the Hamming cube, Fourier expansion basics, and linear threshold functions (LTFs). -/ +@[expose] public section + open Finset BigOperators namespace BooleanAnalysis From 16410d78cf094c1bc2e82e8a16e2f0af02c466e5 Mon Sep 17 00:00:00 2001 From: AlexeyMilovanov Date: Sun, 10 May 2026 01:15:07 +0100 Subject: [PATCH 5/5] chore: fix linter warnings (namespace, AMS tags, docstring) --- .../Degree1Weight.lean | 25 +++++++++++-------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean b/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean index 3442dbda59..753690ad00 100644 --- a/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean +++ b/FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean @@ -13,12 +13,8 @@ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ -import FormalConjecturesForMathlib.Analysis.BooleanFunction -import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import FormalConjectures.Util.Attributes.Basic -import FormalConjectures.Util.Attributes.AMS -/-! +/- # Degree-1 Fourier Weight Conjecture Author: Alexey Milovanov @@ -26,20 +22,29 @@ Author: Alexey Milovanov This file states the Degree-1 Fourier Weight Conjecture (Conjecture 5.3) from Ryan O'Donnell's "Analysis of Boolean Functions" (2014). -The conjecture asserts that for any unbiased Linear Threshold Function (LTF), +*Reference:* R. O'Donnell, [Analysis of Boolean Functions](https://doi.org/10.1017/CBO9781139814782) (2014), Conjecture 5.3. + +The conjecture asserts that for any Linear Threshold Function (LTF), the Fourier weight at degree at most 1 is at least $2/\pi$. This lower bound is asymptotically tight and is achieved by the Majority function as $n \to \infty$. -/ +module + +import FormalConjectures.Util.ProblemImports + open Finset BooleanAnalysis -/-- English version: "If `f : 𝔽₂ⁿ β†’ {-1, 1}` is an unbiased linear threshold function, +namespace Books.AnalysisOfBooleanFunctions + +/-- English version: "If `f : 𝔽₂ⁿ β†’ {-1, 1}` is a linear threshold function, then its Fourier weight at degree at most 1 is at least `2/Ο€`." -/ -@[category research open, AMS 68, AMS 42] +@ [category research open, AMS 68 42] theorem degree_1_weight_conjecture (n : β„•) (f : BooleanFunction n) (hf_bool : IsBooleanValued f) - (h_ltf : IsLTF f) - (h_unbiased : IsUnbiased f) : + (h_ltf : IsLTF f) : 𝐖_≀ f 1 β‰₯ 2 / Real.pi := by sorry + +end Books.AnalysisOfBooleanFunctions