Analysis of Boolean Functions in Lean

4.4. Håstad's Switching Lemma and the spectrum of DNFs🔗

Lemma4.4.1
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 4.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-4-4supportfidelity-exact-coordinate-restriction-extension-counting

Exercise 4.19 (Baby Switching Lemma with constant 3). Let \varphi=T_1\vee\cdots\vee T_s be a DNF of width w\ge1 and let (\boldsymbol J\mid\boldsymbol z) be a \delta-random restriction with \delta\le1/3. Call a restriction R=(J\mid z) bad when \varphi_{J\mid z} is non-constant. For each bad R, let T_i be the first restricted term that is neither constantly True nor constantly False, and let j be the first surviving variable in that term.

(a) There is a unique extension R'=(J\setminus\{j\}\mid z') that does not falsify T_i. (b) No R' is produced by more than w bad restrictions. (c) Their exact random-restriction weights satisfy \Pr[(\boldsymbol J\mid\boldsymbol z)=R] =\frac{2\delta}{1-\delta}\Pr[(\boldsymbol J\mid\boldsymbol z)=R']. (d) Consequently \Pr[(\boldsymbol J\mid\boldsymbol z)\text{ is bad}]\le3\delta w.

The first-compatible-term extension map has the required fiber bound and the exact ratio in (c); summing over its fibers gives (d) in either restriction model.

Lean code for Lemma4.4.1●13 declarations
  • defdefined in FABL/Chapter04/Switching.lean
    complete
    def FABL.DNFTerm.Compatible {n : ℕ} (T : FABL.DNFTerm n)
  (ρ : Fin n → FABL.CoordRestriction) : Prop
    def FABL.DNFTerm.Compatible {n : ℕ}
  (T : FABL.DNFTerm n)
  (ρ : Fin n → FABL.CoordRestriction) :
  Prop
    A term is compatible with a partial restriction when some completion satisfies it.
  • defdefined in FABL/Chapter04/Switching.lean
    complete
    def FABL.DNFFormula.IsBadRestriction {n : ℕ} (φ : FABL.DNFFormula n)
  (ρ : Fin n → FABL.CoordRestriction) : Prop
    def FABL.DNFFormula.IsBadRestriction {n : ℕ}
  (φ : FABL.DNFFormula n)
  (ρ : Fin n → FABL.CoordRestriction) :
  Prop
    A restricted DNF is bad when its computed function is not constant.
  • defdefined in FABL/Chapter04/Switching.lean
    complete
    def FABL.DNFFormula.badRestrictions {n : ℕ} (φ : FABL.DNFFormula n) :
  Finset (Fin n → FABL.CoordRestriction)
    def FABL.DNFFormula.badRestrictions {n : ℕ}
  (φ : FABL.DNFFormula n) :
  Finset (Fin n → FABL.CoordRestriction)
    Bad restrictions as a finite set.
  • defdefined in FABL/Chapter04/Switching.lean
    complete
    def FABL.DNFFormula.badExtension {n : ℕ} (φ : FABL.DNFFormula n)
  (ρ : Fin n → FABL.CoordRestriction) (hbad : φ.IsBadRestriction ρ) :
  Fin n → FABL.CoordRestriction
    def FABL.DNFFormula.badExtension {n : ℕ}
  (φ : FABL.DNFFormula n)
  (ρ : Fin n → FABL.CoordRestriction)
  (hbad : φ.IsBadRestriction ρ) :
  Fin n → FABL.CoordRestriction
    Exercise 4.19(a)'s extension `R'`.
  • defdefined in FABL/Chapter04/Switching.lean
    complete
    def FABL.DNFFormula.badExtensionMap {n : ℕ} (φ : FABL.DNFFormula n) :
  { ρ // φ.IsBadRestriction ρ } → Fin n → FABL.CoordRestriction
    def FABL.DNFFormula.badExtensionMap {n : ℕ}
  (φ : FABL.DNFFormula n) :
  { ρ // φ.IsBadRestriction ρ } →
    Fin n → FABL.CoordRestriction
    Exercise 4.19's encoding map, defined on the bad-restriction subtype.
  • defdefined in FABL/Chapter04/Switching.lean
    complete
    def FABL.DNFFormula.badExtensionFiber {n : ℕ} (φ : FABL.DNFFormula n)
  (η : Fin n → FABL.CoordRestriction) :
  Finset { ρ // φ.IsBadRestriction ρ }
    def FABL.DNFFormula.badExtensionFiber {n : ℕ}
  (φ : FABL.DNFFormula n)
  (η : Fin n → FABL.CoordRestriction) :
  Finset { ρ // φ.IsBadRestriction ρ }
    Fiber of the Exercise 4.19 encoding over a fixed extended restriction.
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.DNFFormula.badExtensionFiber_card_le_width {n : ℕ}
  (φ : FABL.DNFFormula n) {w : ℕ} (hw : φ.width ≤ w)
  (η : Fin n → FABL.CoordRestriction) : (φ.badExtensionFiber η).card ≤ w
    theorem FABL.DNFFormula.badExtensionFiber_card_le_width
  {n : ℕ} (φ : FABL.DNFFormula n) {w : ℕ}
  (hw : φ.width ≤ w)
  (η : Fin n → FABL.CoordRestriction) :
  (φ.badExtensionFiber η).card ≤ w
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.DNFFormula.restrictionAssignmentWeightAt_badExtension_eq {n : ℕ}
  (φ : FABL.DNFFormula n) (δ : ℝ) (hδ : δ ≠ 1)
  (ρ : Fin n → FABL.CoordRestriction) (hbad : φ.IsBadRestriction ρ) :
  FABL.restrictionAssignmentWeightAt δ ρ =
    2 * δ / (1 - δ) *
      FABL.restrictionAssignmentWeightAt δ (φ.badExtension ρ hbad)
    theorem FABL.DNFFormula.restrictionAssignmentWeightAt_badExtension_eq
  {n : ℕ} (φ : FABL.DNFFormula n) (δ : ℝ)
  (hδ : δ ≠ 1)
  (ρ : Fin n → FABL.CoordRestriction)
  (hbad : φ.IsBadRestriction ρ) :
  FABL.restrictionAssignmentWeightAt δ ρ =
    2 * δ / (1 - δ) *
      FABL.restrictionAssignmentWeightAt δ
        (φ.badExtension ρ hbad)
    Exercise 4.19(c): exact weight ratio between a bad restriction and its one-coordinate
extension.
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.DNFFormula.restrictionAssignmentWeightAt_badExtension_le {n : ℕ}
  (φ : FABL.DNFFormula n) (δ : ℝ) (hδ0 : 0 ≤ δ) (hδ : δ ≤ 1 / 3)
  (ρ : Fin n → FABL.CoordRestriction) (hbad : φ.IsBadRestriction ρ) :
  FABL.restrictionAssignmentWeightAt δ ρ ≤
    3 * δ * FABL.restrictionAssignmentWeightAt δ (φ.badExtension ρ hbad)
    theorem FABL.DNFFormula.restrictionAssignmentWeightAt_badExtension_le
  {n : ℕ} (φ : FABL.DNFFormula n) (δ : ℝ)
  (hδ0 : 0 ≤ δ) (hδ : δ ≤ 1 / 3)
  (ρ : Fin n → FABL.CoordRestriction)
  (hbad : φ.IsBadRestriction ρ) :
  FABL.restrictionAssignmentWeightAt δ ρ ≤
    3 * δ *
      FABL.restrictionAssignmentWeightAt δ
        (φ.badExtension ρ hbad)
  • defdefined in FABL/Chapter04/Switching.lean
    complete
    def FABL.DNFFormula.badRestrictionWeight {n : ℕ} (φ : FABL.DNFFormula n)
  (δ : ℝ) : ℝ
    def FABL.DNFFormula.badRestrictionWeight
  {n : ℕ} (φ : FABL.DNFFormula n)
  (δ : ℝ) : ℝ
    Total weight of bad restrictions in the independent-coordinate model.
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.exercise4_19 {n : ℕ} (φ : FABL.DNFFormula n) {w : ℕ}
  (hw : φ.width ≤ w) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ : δ ≤ 1 / 3) :
  φ.badRestrictionWeight δ ≤ 3 * δ * ↑w
    theorem FABL.exercise4_19 {n : ℕ}
  (φ : FABL.DNFFormula n) {w : ℕ}
  (hw : φ.width ≤ w) {δ : ℝ} (hδ0 : 0 ≤ δ)
  (hδ : δ ≤ 1 / 3) :
  φ.badRestrictionWeight δ ≤ 3 * δ * ↑w
    Exercise 4.19(d): the Baby Switching bound with constant `3`, independent of DNF size.
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.DNFFormula.badRestrictionWeight_eq_coordSwitchingFailureProbability
  {n : ℕ} (φ : FABL.DNFFormula n) (δ : ℝ) :
  φ.badRestrictionWeight δ =
    FABL.coordSwitchingFailureProbability φ.toBooleanFunction δ 1
    theorem FABL.DNFFormula.badRestrictionWeight_eq_coordSwitchingFailureProbability
  {n : ℕ} (φ : FABL.DNFFormula n)
  (δ : ℝ) :
  φ.badRestrictionWeight δ =
    FABL.coordSwitchingFailureProbability
      φ.toBooleanFunction δ 1
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.exercise4_19_switchingFailureProbability {n : ℕ}
  (φ : FABL.DNFFormula n) {w : ℕ} (hw : φ.width ≤ w) {δ : ℝ}
  (hδ0 : 0 ≤ δ) (hδ : δ ≤ 1 / 3) :
  FABL.switchingFailureProbability φ.toBooleanFunction δ 1 ≤ 3 * δ * ↑w
    theorem FABL.exercise4_19_switchingFailureProbability
  {n : ℕ} (φ : FABL.DNFFormula n) {w : ℕ}
  (hw : φ.width ≤ w) {δ : ℝ} (hδ0 : 0 ≤ δ)
  (hδ : δ ≤ 1 / 3) :
  FABL.switchingFailureProbability
      φ.toBooleanFunction δ 1 ≤
    3 * δ * ↑w
    Exercise 4.19 in the canonical switching-probability presentation.
Theorem4.4.2
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Definition 4.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-4-4fidelity-exact

Baby Switching Lemma. Let f:\{-1,1\}^n\to\{-1,1\} be computable by a DNF or CNF of width at most w and let (\boldsymbol J\mid\boldsymbol z) be a \delta-random restriction. Then \Pr\bigl[f_{\boldsymbol J\mid\boldsymbol z}\text{ is not a constant function}\bigr] \le 5\delta w. This is the k=1 case of Håstad's Switching Lemma. The same size-independent constant 5 holds for DNFs and, by Boolean duality, for CNFs.

Lean code for Theorem4.4.2●3 theorems
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.babySwitchingLemma_dnf {n : ℕ} (φ : FABL.DNFFormula n) {w : ℕ}
  (hw : φ.width ≤ w) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) :
  FABL.switchingFailureProbability φ.toBooleanFunction δ 1 ≤ 5 * δ * ↑w
    theorem FABL.babySwitchingLemma_dnf {n : ℕ}
  (φ : FABL.DNFFormula n) {w : ℕ}
  (hw : φ.width ≤ w) {δ : ℝ} (hδ0 : 0 ≤ δ)
  (hδ1 : δ ≤ 1) :
  FABL.switchingFailureProbability
      φ.toBooleanFunction δ 1 ≤
    5 * δ * ↑w
    The exact size-independent Baby Switching bound for a width-bounded DNF.
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.switchingFailureProbability_booleanDual {n : ℕ}
  (f : FABL.BooleanFunction n) (δ : ℝ) (k : ℕ) :
  FABL.switchingFailureProbability (FABL.CNFFormula.booleanDual f) δ k =
    FABL.switchingFailureProbability f δ k
    theorem FABL.switchingFailureProbability_booleanDual
  {n : ℕ} (f : FABL.BooleanFunction n)
  (δ : ℝ) (k : ℕ) :
  FABL.switchingFailureProbability
      (FABL.CNFFormula.booleanDual f) δ
      k =
    FABL.switchingFailureProbability f δ k
  • theoremdefined in FABL/Chapter04/Switching.lean
    complete
    theorem FABL.babySwitchingLemma {n : ℕ} {f : FABL.BooleanFunction n} {w : ℕ}
  {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
  (hf : FABL.HasDNFWidthLE f w ∨ FABL.HasCNFWidthLE f w) :
  FABL.switchingFailureProbability f δ 1 ≤ 5 * δ * ↑w
    theorem FABL.babySwitchingLemma {n : ℕ}
  {f : FABL.BooleanFunction n} {w : ℕ}
  {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
  (hf :
    FABL.HasDNFWidthLE f w ∨
      FABL.HasCNFWidthLE f w) :
  FABL.switchingFailureProbability f δ 1 ≤
    5 * δ * ↑w
    The exact Baby Switching Lemma, for either a DNF or a CNF of width at most `w`.
Theorem4.4.3
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Definition 3.2.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 4.4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-4-4fidelity-exact

Håstad's Switching Lemma. Let f:\{-1,1\}^n\to\{-1,1\} be computable by a DNF or CNF of width at most w and let (\boldsymbol J\mid\boldsymbol z) be a \delta-random restriction. Then for every k\in\mathbb N, \Pr\bigl[\operatorname{DT}(f_{\boldsymbol J\mid\boldsymbol z})\ge k\bigr] \le(5\delta w)^k, where \operatorname{DT}(g) denotes the decision-tree depth of g. The bound has no dependence on the DNF size or on n.

Lean code for Theorem4.4.3●2 theorems
  • theoremdefined in FABL/Chapter04/HastadSwitching.lean
    complete
    theorem FABL.hastadSwitchingLemma_dnf {n : ℕ} (φ : FABL.DNFFormula n) {w k : ℕ}
  (hw : φ.width ≤ w) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) :
  FABL.switchingFailureProbability φ.toBooleanFunction δ k ≤
    (5 * δ * ↑w) ^ k
    theorem FABL.hastadSwitchingLemma_dnf {n : ℕ}
  (φ : FABL.DNFFormula n) {w k : ℕ}
  (hw : φ.width ≤ w) {δ : ℝ} (hδ0 : 0 ≤ δ)
  (hδ1 : δ ≤ 1) :
  FABL.switchingFailureProbability
      φ.toBooleanFunction δ k ≤
    (5 * δ * ↑w) ^ k
    Håstad's Switching Lemma for a width-bounded DNF.
  • theoremdefined in FABL/Chapter04/HastadSwitching.lean
    complete
    theorem FABL.hastadSwitchingLemma {n : ℕ} {f : FABL.BooleanFunction n} {w k : ℕ}
  {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
  (hf : FABL.HasDNFWidthLE f w ∨ FABL.HasCNFWidthLE f w) :
  FABL.switchingFailureProbability f δ k ≤ (5 * δ * ↑w) ^ k
    theorem FABL.hastadSwitchingLemma {n : ℕ}
  {f : FABL.BooleanFunction n} {w k : ℕ}
  {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
  (hf :
    FABL.HasDNFWidthLE f w ∨
      FABL.HasCNFWidthLE f w) :
  FABL.switchingFailureProbability f δ k ≤
    (5 * δ * ↑w) ^ k
    Håstad's Switching Lemma, for either a DNF or a CNF of width at most `w`.
Lemma4.4.4
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Definition 3.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 4.4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-4-4fidelity-exact

Lemma 4.21. Let f:\{-1,1\}^n\to\{-1,1\} and let (\boldsymbol J\mid\boldsymbol z) be a \delta-random restriction with \delta>0. Fix k\in\mathbb N^+ and write \epsilon=\Pr[\operatorname{DT}(f_{\boldsymbol J\mid\boldsymbol z})\ge k]. Then the Fourier spectrum of f is 3\epsilon-concentrated on degree up to 3k/\delta.

Here \epsilon is the exact failure probability and 3k/\delta is the exact real cutoff, with 0<\delta\le1.

Lean code for Lemma4.4.4●1 theorem
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.lemma4_21 {n : ℕ} (f : FABL.BooleanFunction n) {δ : ℝ}
  (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) {k : ℕ} (hk : 0 < k) :
  FABL.IsFourierSpectrumConcentratedUpTo f.toReal
    (3 * FABL.switchingFailureProbability f δ k) (3 * ↑k / δ)
    theorem FABL.lemma4_21 {n : ℕ}
  (f : FABL.BooleanFunction n) {δ : ℝ}
  (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) {k : ℕ}
  (hk : 0 < k) :
  FABL.IsFourierSpectrumConcentratedUpTo
    f.toReal
    (3 *
      FABL.switchingFailureProbability f δ
        k)
    (3 * ↑k / δ)
    O'Donnell, Lemma 4.21: if a `δ`-random restriction has decision-tree depth at least
`k` with probability `ε`, then the Fourier spectrum is `3ε`-concentrated through the exact
real cutoff `3k / δ`.
Theorem4.4.5
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 4.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 4.4.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-4-4fidelity-finite-explicit-asymptotic-bridge

Theorem 4.22. Suppose f:\{-1,1\}^n\to\{-1,1\} is computable by a DNF of width w. Then the Fourier spectrum of f is \epsilon-concentrated on degree up to O\bigl(w\log(1/\epsilon)\bigr).

One may take the explicit cutoff 30w\lceil\log_2(3/\epsilon)\rceil for 0<\epsilon\le1, including the w=0 constant-function endpoint.

Lean code for Theorem4.4.5●2 declarations
  • defdefined in FABL/Chapter04/DNFFourier.lean
    complete
    def FABL.dnfSwitchingDepth (ε : ℝ) : ℕ
    def FABL.dnfSwitchingDepth (ε : ℝ) : ℕ
    Decision-tree threshold used in the explicit form of Theorem 4.22.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.theorem4_22 {n : ℕ} (f : FABL.BooleanFunction n) {w : ℕ}
  (hf : FABL.HasDNFWidthLE f w) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1) :
  FABL.IsFourierSpectrumConcentratedUpTo f.toReal ε
    (30 * ↑w * ↑(FABL.dnfSwitchingDepth ε))
    theorem FABL.theorem4_22 {n : ℕ}
  (f : FABL.BooleanFunction n) {w : ℕ}
  (hf : FABL.HasDNFWidthLE f w) {ε : ℝ}
  (hε0 : 0 < ε) (hε1 : ε ≤ 1) :
  FABL.IsFourierSpectrumConcentratedUpTo
    f.toReal ε
    (30 * ↑w *
      ↑(FABL.dnfSwitchingDepth ε))
    O'Donnell, Theorem 4.22, with an explicit natural degree cutoff and the constant
width-zero endpoint included.
Lemma4.4.6
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Proposition 3.2.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-4-4supportfidelity-exact

Exercise 4.11. Prove Lemma 4.23.

Combine the restriction identity for Fourier coefficients with \|\widehat g\|_1\le2^{\operatorname{DT}(g)} for each restricted Boolean function.

Lean code for Lemma4.4.6●4 theorems
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.fourierCoeff_extendedSignRestriction_liftFree {n : ℕ}
  (f : FABL.SignCube n → ℝ) (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) (S : Finset ↥J) :
  FABL.fourierCoeff (FABL.extendedSignRestriction f J z)
      (FABL.liftFreeFrequency S) =
    FABL.restrictionFourierCoeff f J S z
    theorem FABL.fourierCoeff_extendedSignRestriction_liftFree
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J)
  (S : Finset ↥J) :
  FABL.fourierCoeff
      (FABL.extendedSignRestriction f J z)
      (FABL.liftFreeFrequency S) =
    FABL.restrictionFourierCoeff f J S z
    Extending a restricted function by dummy fixed coordinates preserves every Fourier
coefficient supported on the free coordinates.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.fourierCoeff_extendedSignRestriction {n : ℕ}
  (f : FABL.SignCube n → ℝ) (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) (S : Finset (Fin n)) :
  FABL.fourierCoeff (FABL.extendedSignRestriction f J z) S =
    FABL.ambientRestrictionFourierCoeff f J S z
    theorem FABL.fourierCoeff_extendedSignRestriction
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff
      (FABL.extendedSignRestriction f J z)
      S =
    FABL.ambientRestrictionFourierCoeff f
      J S z
    The ambient coefficient convention agrees with the ordinary coefficient of the extended
restricted function.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.sum_abs_ambientRestrictionFourierCoeff {n : ℕ}
  (f : FABL.SignCube n → ℝ) (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  ∑ S, |FABL.ambientRestrictionFourierCoeff f J S z| =
    FABL.fourierOneNorm (FABL.extendedSignRestriction f J z)
    theorem FABL.sum_abs_ambientRestrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  ∑ S,
      |FABL.ambientRestrictionFourierCoeff
          f J S z| =
    FABL.fourierOneNorm
      (FABL.extendedSignRestriction f J z)
    Summing ambient restriction coefficients is exactly the Fourier one-norm of the extended
restriction.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.exercise4_11_restriction {n : ℕ} (f : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (z : FABL.FixedSignCube J) :
  FABL.fourierOneNorm (FABL.extendedSignRestriction f.toReal J z) ≤
    ↑(2 ^ FABL.restrictedDecisionTreeDepth f J z)
    theorem FABL.exercise4_11_restriction {n : ℕ}
  (f : FABL.BooleanFunction n)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  FABL.fourierOneNorm
      (FABL.extendedSignRestriction
        f.toReal J z) ≤
    ↑(2 ^
        FABL.restrictedDecisionTreeDepth f
          J z)
    O'Donnell, Exercise 4.11: the Fourier one-norm of a Boolean function is at most two to
the minimum decision-tree depth. Applied here to the Boolean function induced by a restriction.
Lemma4.4.7
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 4.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-4-4fidelity-exact

Lemma 4.23. Let f:\{-1,1\}^n\to\{-1,1\} and let (\boldsymbol J\mid\boldsymbol z) be a \delta-random restriction. Then \sum_{U\subseteq[n]}\delta^{|U|}\,\bigl|\widehat f(U)\bigr| \le \mathbb E_{(\boldsymbol J\mid\boldsymbol z)} \Bigl[2^{\operatorname{DT}(f_{\boldsymbol J\mid\boldsymbol z})}\Bigr].

Lean code for Lemma4.4.7●4 theorems
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.abs_expectRandomRestriction_le_expect_abs {n : ℕ} {δ : ℝ}
  (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
  (g : (J : Finset (Fin n)) → FABL.FixedSignCube J → ℝ) :
  |FABL.expectRandomRestriction n δ g| ≤
    FABL.expectRandomRestriction n δ fun J z => |g J z|
    theorem FABL.abs_expectRandomRestriction_le_expect_abs
  {n : ℕ} {δ : ℝ} (hδ0 : 0 ≤ δ)
  (hδ1 : δ ≤ 1)
  (g :
    (J : Finset (Fin n)) →
      FABL.FixedSignCube J → ℝ) :
  |FABL.expectRandomRestriction n δ g| ≤
    FABL.expectRandomRestriction n δ
      fun J z => |g J z|
    Triangle inequality for the finite random-restriction expectation.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.sum_expectRandomRestriction.{u_1} {n : ℕ} {ι : Type u_1}
  [Fintype ι] (δ : ℝ)
  (g : ι → (J : Finset (Fin n)) → FABL.FixedSignCube J → ℝ) :
  ∑ a, FABL.expectRandomRestriction n δ (g a) =
    FABL.expectRandomRestriction n δ fun J z => ∑ a, g a J z
    theorem FABL.sum_expectRandomRestriction.{u_1}
  {n : ℕ} {ι : Type u_1} [Fintype ι]
  (δ : ℝ)
  (g :
    ι →
      (J : Finset (Fin n)) →
        FABL.FixedSignCube J → ℝ) :
  ∑ a,
      FABL.expectRandomRestriction n δ
        (g a) =
    FABL.expectRandomRestriction n δ
      fun J z => ∑ a, g a J z
    Finite sums commute with the random-restriction expectation.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.expectRandomRestriction_mono {n : ℕ} {δ : ℝ} (hδ0 : 0 ≤ δ)
  (hδ1 : δ ≤ 1) {g h : (J : Finset (Fin n)) → FABL.FixedSignCube J → ℝ}
  (hgh :
    ∀ (J : Finset (Fin n)) (z : FABL.FixedSignCube J), g J z ≤ h J z) :
  FABL.expectRandomRestriction n δ g ≤
    FABL.expectRandomRestriction n δ h
    theorem FABL.expectRandomRestriction_mono {n : ℕ}
  {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
  {g h :
    (J : Finset (Fin n)) →
      FABL.FixedSignCube J → ℝ}
  (hgh :
    ∀ (J : Finset (Fin n))
      (z : FABL.FixedSignCube J),
      g J z ≤ h J z) :
  FABL.expectRandomRestriction n δ g ≤
    FABL.expectRandomRestriction n δ h
    Monotonicity of random-restriction expectation for genuine probability parameters.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.lemma4_23 {n : ℕ} (f : FABL.BooleanFunction n) {δ : ℝ}
  (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) :
  ∑ S, δ ^ S.card * |FABL.fourierCoeff f.toReal S| ≤
    FABL.expectRandomRestriction n δ fun J z =>
      ↑(2 ^ FABL.restrictedDecisionTreeDepth f J z)
    theorem FABL.lemma4_23 {n : ℕ}
  (f : FABL.BooleanFunction n) {δ : ℝ}
  (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) :
  ∑ S,
      δ ^ S.card *
        |FABL.fourierCoeff f.toReal S| ≤
    FABL.expectRandomRestriction n δ
      fun J z =>
      ↑(2 ^
          FABL.restrictedDecisionTreeDepth
            f J z)
    O'Donnell, Lemma 4.23: the weighted Fourier one-norm is bounded by the expected
`2 ^ DT-depth` of a random restriction.
Theorem4.4.8
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 4.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-4-4fidelity-book-endpoint-corrected

Theorem 4.24. Suppose f:\{-1,1\}^n\to\{-1,1\} is computable by a DNF of width w. Then for every k, \sum_{|U|\le k}\bigl|\widehat f(U)\bigr| \le 2\cdot(20w)^k.

The printed statement requires the endpoint condition w\ge1: for w=0 and k>0, a constant function has |\widehat f(\varnothing)|=1 while the displayed right-hand side is zero. Thus the statement is understood with w\ge1; the constant is unchanged.

Lean code for Theorem4.4.8●3 theorems
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.lowDegreeFourierOneNorm_le_two_mul_inv_pow_of_expected_two_pow_le
  {n : ℕ} (f : FABL.BooleanFunction n) {δ : ℝ} (hδ0 : 0 < δ)
  (hδ1 : δ ≤ 1) (k : ℕ)
  (hmoment :
    (FABL.expectRandomRestriction n δ fun J z =>
        ↑(2 ^ FABL.restrictedDecisionTreeDepth f J z)) ≤
      2) :
  ∑ S with S.card ≤ k, |FABL.fourierCoeff f.toReal S| ≤ 2 * δ⁻¹ ^ k
    theorem FABL.lowDegreeFourierOneNorm_le_two_mul_inv_pow_of_expected_two_pow_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1)
  (k : ℕ)
  (hmoment :
    (FABL.expectRandomRestriction n δ
        fun J z =>
        ↑(2 ^
            FABL.restrictedDecisionTreeDepth
              f J z)) ≤
      2) :
  ∑ S with S.card ≤ k,
      |FABL.fourierCoeff f.toReal S| ≤
    2 * δ⁻¹ ^ k
    Lemma 4.23 converts an upper bound on the expected restricted `2 ^ DT` into a low-degree
Fourier one-norm bound.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.theorem4_24_of_switchingFailureProbability_le_quarter {n : ℕ}
  (f : FABL.BooleanFunction n) {w : ℕ} (hw : 0 < w) (k : ℕ)
  (hfailure :
    ∀ (d : ℕ),
      FABL.switchingFailureProbability f (1 / (20 * ↑w)) d ≤
        (1 / 4) ^ d) :
  ∑ S with S.card ≤ k, |FABL.fourierCoeff f.toReal S| ≤
    2 * (20 * ↑w) ^ k
    theorem FABL.theorem4_24_of_switchingFailureProbability_le_quarter
  {n : ℕ} (f : FABL.BooleanFunction n)
  {w : ℕ} (hw : 0 < w) (k : ℕ)
  (hfailure :
    ∀ (d : ℕ),
      FABL.switchingFailureProbability f
          (1 / (20 * ↑w)) d ≤
        (1 / 4) ^ d) :
  ∑ S with S.card ≤ k,
      |FABL.fourierCoeff f.toReal S| ≤
    2 * (20 * ↑w) ^ k
    Exact quantitative implication behind Theorem 4.24. The positive-width hypothesis is
necessary at the endpoint: the printed formula is false for `w = 0` and `k > 0`.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.theorem4_24 {n : ℕ} (f : FABL.BooleanFunction n) {w : ℕ}
  (hw : 0 < w) (hf : FABL.HasDNFWidthLE f w) (k : ℕ) :
  ∑ S with S.card ≤ k, |FABL.fourierCoeff f.toReal S| ≤
    2 * (20 * ↑w) ^ k
    theorem FABL.theorem4_24 {n : ℕ}
  (f : FABL.BooleanFunction n) {w : ℕ}
  (hw : 0 < w)
  (hf : FABL.HasDNFWidthLE f w) (k : ℕ) :
  ∑ S with S.card ≤ k,
      |FABL.fourierCoeff f.toReal S| ≤
    2 * (20 * ↑w) ^ k
    O'Donnell, Theorem 4.24, with the necessary endpoint condition `w > 0`.
Theorem4.4.9
Group: Chapter 4: DNF formulas and small-depth circuits (44)
Group member previews
Preview
Definition 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Lemma 3.5.9
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-4-4fidelity-finite-explicit-asymptotic-bridge

Theorem 4.25. Let f:\{-1,1\}^n\to\{-1,1\} be computable by a DNF of width w\ge2. Then for every \epsilon\in(0,1/2], the Fourier spectrum of f is \epsilon-concentrated on a collection \mathcal F with |\mathcal F|\le w^{O\bigl(w\log(1/\epsilon)\bigr)}. In particular, width-O(\log n) DNFs with constant \epsilon are concentrated on a collection of cardinality n^{O(\log\log n)}. Combined with Proposition 4.9 and Exercise 3.17, size-s DNFs are \epsilon-concentrated on a collection of cardinality at most (s/\epsilon)^{O(\log\log(s/\epsilon)\cdot\log(1/\epsilon))}. More precisely, one may take the finite degree 30w\lceil\log_2(12/\epsilon)\rceil and the explicit concentrating-family bound obtained from its low-degree Fourier one-norm estimate.

Lean code for Theorem4.4.9●3 declarations
  • defdefined in FABL/Chapter04/DNFFourier.lean
    complete
    def FABL.dnfSpectralConcentrationDegree (w : ℕ) (ε : ℝ) : ℕ
    def FABL.dnfSpectralConcentrationDegree
  (w : ℕ) (ε : ℝ) : ℕ
    Explicit natural degree used in the quantitative form of Theorem 4.25.
  • defdefined in FABL/Chapter04/DNFFourier.lean
    complete
    def FABL.dnfSpectralFamilySizeBound (w : ℕ) (ε : ℝ) : ℝ
    def FABL.dnfSpectralFamilySizeBound (w : ℕ)
  (ε : ℝ) : ℝ
    Explicit cardinality bound furnished by the proof of Theorem 4.25.
  • theoremdefined in FABL/Chapter04/DNFFourier.lean
    complete
    theorem FABL.theorem4_25 {n : ℕ} (f : FABL.BooleanFunction n) {w : ℕ}
  (hw : 2 ≤ w) (hf : FABL.HasDNFWidthLE f w) {ε : ℝ} (hε0 : 0 < ε)
  (hε1 : ε ≤ 1 / 2) :
  ∃ 𝓕,
    FABL.IsFourierSpectrumConcentratedOn f.toReal ε ↑𝓕 ∧
      ↑𝓕.card ≤ FABL.dnfSpectralFamilySizeBound w ε
    theorem FABL.theorem4_25 {n : ℕ}
  (f : FABL.BooleanFunction n) {w : ℕ}
  (hw : 2 ≤ w)
  (hf : FABL.HasDNFWidthLE f w) {ε : ℝ}
  (hε0 : 0 < ε) (hε1 : ε ≤ 1 / 2) :
  ∃ 𝓕,
    FABL.IsFourierSpectrumConcentratedOn
        f.toReal ε ↑𝓕 ∧
      ↑𝓕.card ≤
        FABL.dnfSpectralFamilySizeBound w
          ε
    O'Donnell, Theorem 4.25, with the proof's finite concentrating family and explicit
cardinality bound.