feat: Formalize Degree-1 Fourier Weight Conjecture (O'Donnell)

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

FormalConjectures/Books/AnalysisOfBooleanFunctions/Degree1Weight.lean

@@ -0,0 +1,50 @@
+/-
+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.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+/-
+# 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).
+
+*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
+
+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 42]
+theorem degree_1_weight_conjecture (n : ℕ) (f : BooleanFunction n)
+    (hf_bool : IsBooleanValued f)
+    (h_ltf : IsLTF f) :
+    𝐖_≤ f 1 ≥ 2 / Real.pi := by
+  sorry
+
+end Books.AnalysisOfBooleanFunctions

FormalConjecturesForMathlib/Analysis/BooleanFunction.lean

@@ -0,0 +1,106 @@
+/-
+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.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+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
+
+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).
+-/
+
+@[expose] public section
+
+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