Analysis of Boolean Functions in Lean

4.5. Highlight: LMN's work on constant-depth circuits🔗

Definition4.5.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.
uses 0
Used by 4
Reverse dependency previews
Preview
Definition 4.5.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-4-5fidelity-exact-intrinsic-layered-model

Definition 4.26. For an integer d\ge2, a depth-d circuit over Boolean variables x_1,\ldots,x_n is a directed acyclic graph whose nodes (“gates”) are arranged in d+1 layers, with every wire going from layer j-1 to layer j for some j\in[d]. Layer 0 has exactly 2n nodes labelled by the 2n literals, and layer d has exactly one output node. Nodes in layers 1,3,5,\ldots share one of the labels \wedge or \vee, and nodes in layers 2,4,6,\ldots share the other label. Each node computes a function \{-1,1\}^n\to\{-1,1\}: literals compute themselves, and \wedge (respectively \vee) nodes compute the logical AND (respectively OR) of their incoming functions. The circuit computes the function computed by its output node. In particular, DNFs and CNFs are depth-2 circuits.

Lean code for Definition4.5.1●28 declarations
  • inductive(2 constructors)defined in FABL/Chapter04/Circuits.lean
    complete
    inductive FABL.CircuitGate : Type
    inductive FABL.CircuitGate : Type
    Gate label at an internal layer: AND or OR.

    Constructors

    FABL.CircuitGate.and : FABL.CircuitGate
    Logical $\mathsf{AND}$ gate. 
    FABL.CircuitGate.or : FABL.CircuitGate
    Logical $\mathsf{OR}$ gate.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.CircuitGate.dual : FABL.CircuitGate → FABL.CircuitGate
    def FABL.CircuitGate.dual :
  FABL.CircuitGate → FABL.CircuitGate
    The other gate label. Adjacent non-input layers have dual labels.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.CircuitGate.evalTerm {n : ℕ} (gate : FABL.CircuitGate)
  (term : FABL.DNFTerm n) (x : FABL.SignCube n) : FABL.Sign
    def FABL.CircuitGate.evalTerm {n : ℕ}
  (gate : FABL.CircuitGate)
  (term : FABL.DNFTerm n)
  (x : FABL.SignCube n) : FABL.Sign
    Evaluate a layer-one gate whose inputs are literals.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.CircuitGate.evalFinset {m : ℕ} (gate : FABL.CircuitGate)
  (values : Fin m → FABL.Sign) (inputs : Finset (Fin m)) : FABL.Sign
    def FABL.CircuitGate.evalFinset {m : ℕ}
  (gate : FABL.CircuitGate)
  (values : Fin m → FABL.Sign)
  (inputs : Finset (Fin m)) : FABL.Sign
    Evaluate a gate whose incoming wires form a finite set of nodes in the previous layer.
  • inductive(2 constructors, 1 parameter)defined in FABL/Chapter04/Circuits.lean
    complete
    inductive FABL.CircuitTail : ℕ → Type
    inductive FABL.CircuitTail : ℕ → Type
    The non-input layers above layer one of a circuit.

`CircuitTail m` consumes a layer containing exactly `m` nodes. An `output` tail adds the
singleton output layer. A `layer` tail adds an ordinary layer and then continues. The `Fin m`
wire endpoints make out-of-range wires unrepresentable; `Finset` makes parallel duplicate wires
unrepresentable. Gate labels are not stored per node, because Definition 4.26 requires a uniform
label on each layer and alternation between adjacent layers.

    Constructors

    FABL.CircuitTail.output {m : ℕ} (inputs : Finset (Fin m)) :
  FABL.CircuitTail m
    The singleton output layer, represented by its incoming wires. 
    FABL.CircuitTail.layer {m : ℕ}
  (gates : List (Finset (Fin m)))
  (rest : FABL.CircuitTail gates.length) :
  FABL.CircuitTail m
    One non-output layer followed by the remaining layers.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.CircuitTail.layerCount {m : ℕ} : FABL.CircuitTail m → ℕ
    def FABL.CircuitTail.layerCount {m : ℕ} :
  FABL.CircuitTail m → ℕ
    Number of layers represented by the tail, including its output layer.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.CircuitTail.eq_output_of_layerCount_eq_one {m : ℕ}
  (tail : FABL.CircuitTail m) (hcount : tail.layerCount = 1) :
  ∃ inputs, tail = FABL.CircuitTail.output inputs
    theorem FABL.CircuitTail.eq_output_of_layerCount_eq_one
  {m : ℕ} (tail : FABL.CircuitTail m)
  (hcount : tail.layerCount = 1) :
  ∃ inputs,
    tail = FABL.CircuitTail.output inputs
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.CircuitTail.eval {m : ℕ} :
  FABL.CircuitTail m →
    FABL.CircuitGate → (Fin m → FABL.Sign) → FABL.Sign
    def FABL.CircuitTail.eval {m : ℕ} :
  FABL.CircuitTail m →
    FABL.CircuitGate →
      (Fin m → FABL.Sign) → FABL.Sign
    Evaluate all layers in a tail. The supplied label is the label of the first tail layer.
  • structure(3 fields)defined in FABL/Chapter04/Circuits.lean
    complete
    structure FABL.DepthCircuit (n : ℕ) : Type
    structure FABL.DepthCircuit (n : ℕ) : Type
    O'Donnell, Definition 4.26: a layered alternating depth-`d` circuit.

Layer zero is the canonical collection of the `2n` literals. Layer one is a list of gates over
those literals; `DNFTerm.nodupIndices` enforces the book's convention that a layer-one gate does
not use both a variable and its negation and does not repeat a variable. Higher-layer wires are
typed by their source layer, and `CircuitTail` ends in exactly one output gate.

    Fields

    layer1Gate : FABL.CircuitGate
    Uniform label of the layer-one gates. 
    layer1 : List (FABL.DNFTerm n)
    Layer-one gates, represented by their literal inputs. 
    tail : FABL.CircuitTail self.layer1.length
    Layers two through the singleton output layer.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.depth {n : ℕ} (C : FABL.DepthCircuit n) : ℕ
    def FABL.DepthCircuit.depth {n : ℕ}
  (C : FABL.DepthCircuit n) : ℕ
    Circuit depth, i.e. the number of non-input layers.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.depth_ge_two {n : ℕ} (C : FABL.DepthCircuit n) :
  2 ≤ C.depth
    theorem FABL.DepthCircuit.depth_ge_two {n : ℕ}
  (C : FABL.DepthCircuit n) : 2 ≤ C.depth
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.evalLayer1 {n : ℕ} (C : FABL.DepthCircuit n)
  (x : FABL.SignCube n) : Fin C.layer1.length → FABL.Sign
    def FABL.DepthCircuit.evalLayer1 {n : ℕ}
  (C : FABL.DepthCircuit n)
  (x : FABL.SignCube n) :
  Fin C.layer1.length → FABL.Sign
    Evaluate layer one on an input.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.selectedLayer1Terms {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs : Finset (Fin C.layer1.length)) : List (FABL.DNFTerm n)
    def FABL.DepthCircuit.selectedLayer1Terms
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs :
    Finset (Fin C.layer1.length)) :
  List (FABL.DNFTerm n)
    The layer-one gates selected by the incoming wires of a layer-two gate.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.selectedLayer1DNF {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs : Finset (Fin C.layer1.length)) : FABL.DNFFormula n
    def FABL.DepthCircuit.selectedLayer1DNF
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs :
    Finset (Fin C.layer1.length)) :
  FABL.DNFFormula n
    DNF syntax for a layer-two OR gate over layer-one AND gates.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.selectedLayer1CNF {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs : Finset (Fin C.layer1.length)) : FABL.CNFFormula n
    def FABL.DepthCircuit.selectedLayer1CNF
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs :
    Finset (Fin C.layer1.length)) :
  FABL.CNFFormula n
    CNF syntax for a layer-two AND gate over layer-one OR gates.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.layer2GateFunction {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs : Finset (Fin C.layer1.length)) : FABL.BooleanFunction n
    def FABL.DepthCircuit.layer2GateFunction
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs :
    Finset (Fin C.layer1.length)) :
  FABL.BooleanFunction n
    Function computed by one gate at layer two.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.selectedLayer1DNF_toBooleanFunction {n : ℕ}
  (C : FABL.DepthCircuit n)
  (hgate : C.layer1Gate = FABL.CircuitGate.and)
  (inputs : Finset (Fin C.layer1.length)) :
  (C.selectedLayer1DNF inputs).toBooleanFunction =
    C.layer2GateFunction inputs
    theorem FABL.DepthCircuit.selectedLayer1DNF_toBooleanFunction
  {n : ℕ} (C : FABL.DepthCircuit n)
  (hgate :
    C.layer1Gate = FABL.CircuitGate.and)
  (inputs :
    Finset (Fin C.layer1.length)) :
  (C.selectedLayer1DNF
        inputs).toBooleanFunction =
    C.layer2GateFunction inputs
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.selectedLayer1CNF_toBooleanFunction {n : ℕ}
  (C : FABL.DepthCircuit n) (hgate : C.layer1Gate = FABL.CircuitGate.or)
  (inputs : Finset (Fin C.layer1.length)) :
  (C.selectedLayer1CNF inputs).toBooleanFunction =
    C.layer2GateFunction inputs
    theorem FABL.DepthCircuit.selectedLayer1CNF_toBooleanFunction
  {n : ℕ} (C : FABL.DepthCircuit n)
  (hgate :
    C.layer1Gate = FABL.CircuitGate.or)
  (inputs :
    Finset (Fin C.layer1.length)) :
  (C.selectedLayer1CNF
        inputs).toBooleanFunction =
    C.layer2GateFunction inputs
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.eval {n : ℕ} (C : FABL.DepthCircuit n)
  (x : FABL.SignCube n) : FABL.Sign
    def FABL.DepthCircuit.eval {n : ℕ}
  (C : FABL.DepthCircuit n)
  (x : FABL.SignCube n) : FABL.Sign
    O'Donnell, Definition 4.26: the Boolean function computed by the output gate.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.toBooleanFunction {n : ℕ} (C : FABL.DepthCircuit n) :
  FABL.BooleanFunction n
    def FABL.DepthCircuit.toBooleanFunction
  {n : ℕ} (C : FABL.DepthCircuit n) :
  FABL.BooleanFunction n
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.ofDNF {n : ℕ} (formula : FABL.DNFFormula n) :
  FABL.DepthCircuit n
    def FABL.DepthCircuit.ofDNF {n : ℕ}
  (formula : FABL.DNFFormula n) :
  FABL.DepthCircuit n
    Every DNF is a depth-two circuit (OR of AND terms).
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.depth_ofDNF {n : ℕ} (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF formula).depth = 2
    theorem FABL.DepthCircuit.depth_ofDNF {n : ℕ}
  (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF
        formula).depth =
    2
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.eval_ofDNF {n : ℕ} (formula : FABL.DNFFormula n)
  (x : FABL.SignCube n) :
  (FABL.DepthCircuit.ofDNF formula).eval x = formula.eval x
    theorem FABL.DepthCircuit.eval_ofDNF {n : ℕ}
  (formula : FABL.DNFFormula n)
  (x : FABL.SignCube n) :
  (FABL.DepthCircuit.ofDNF formula).eval
      x =
    formula.eval x
    The depth-two embedding computes the original DNF.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.toBooleanFunction_ofDNF {n : ℕ}
  (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF formula).toBooleanFunction =
    formula.toBooleanFunction
    theorem FABL.DepthCircuit.toBooleanFunction_ofDNF
  {n : ℕ} (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF
        formula).toBooleanFunction =
    formula.toBooleanFunction
    The Boolean function of the depth-two embedding is the DNF's Boolean function.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.ofCNF {n : ℕ} (formula : FABL.CNFFormula n) :
  FABL.DepthCircuit n
    def FABL.DepthCircuit.ofCNF {n : ℕ}
  (formula : FABL.CNFFormula n) :
  FABL.DepthCircuit n
    Every CNF is a depth-two circuit (AND of OR clauses).
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.depth_ofCNF {n : ℕ} (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF formula).depth = 2
    theorem FABL.DepthCircuit.depth_ofCNF {n : ℕ}
  (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF
        formula).depth =
    2
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.eval_ofCNF {n : ℕ} (formula : FABL.CNFFormula n)
  (x : FABL.SignCube n) :
  (FABL.DepthCircuit.ofCNF formula).eval x = formula.eval x
    theorem FABL.DepthCircuit.eval_ofCNF {n : ℕ}
  (formula : FABL.CNFFormula n)
  (x : FABL.SignCube n) :
  (FABL.DepthCircuit.ofCNF formula).eval
      x =
    formula.eval x
    The depth-two embedding computes the original CNF.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.toBooleanFunction_ofCNF {n : ℕ}
  (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF formula).toBooleanFunction =
    formula.toBooleanFunction
    theorem FABL.DepthCircuit.toBooleanFunction_ofCNF
  {n : ℕ} (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF
        formula).toBooleanFunction =
    formula.toBooleanFunction
    The Boolean function of the depth-two embedding is the CNF's Boolean function.
Definition4.5.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.
uses 1
Used by 3
Reverse dependency previews
Preview
Lemma 4.5.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-4-5fidelity-exact

Definition 4.27. The size of a depth-d circuit is the number of nodes in layers 1 through d-1. Its width is the maximum in-degree of any node at layer 1. As with DNFs and CNFs, no layer-1 node is connected to a variable or its negation more than once.

Lean code for Definition4.5.2●15 declarations
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.CircuitTail.internalNodeCount {m : ℕ} : FABL.CircuitTail m → ℕ
    def FABL.CircuitTail.internalNodeCount
  {m : ℕ} : FABL.CircuitTail m → ℕ
    Number of non-output nodes represented by the tail.
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.size {n : ℕ} (C : FABL.DepthCircuit n) : ℕ
    def FABL.DepthCircuit.size {n : ℕ}
  (C : FABL.DepthCircuit n) : ℕ
    Size: number of nodes in layers `1` through `depth - 1` (book Definition 4.27).
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.width {n : ℕ} (C : FABL.DepthCircuit n) : ℕ
    def FABL.DepthCircuit.width {n : ℕ}
  (C : FABL.DepthCircuit n) : ℕ
    Width: maximum fan-in of any layer-one gate (book Definition 4.27).
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.width_selectedLayer1DNF_le {n : ℕ}
  (C : FABL.DepthCircuit n) (inputs : Finset (Fin C.layer1.length)) :
  (C.selectedLayer1DNF inputs).width ≤ C.width
    theorem FABL.DepthCircuit.width_selectedLayer1DNF_le
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs :
    Finset (Fin C.layer1.length)) :
  (C.selectedLayer1DNF inputs).width ≤
    C.width
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.width_selectedLayer1CNF_le {n : ℕ}
  (C : FABL.DepthCircuit n) (inputs : Finset (Fin C.layer1.length)) :
  (C.selectedLayer1CNF inputs).width ≤ C.width
    theorem FABL.DepthCircuit.width_selectedLayer1CNF_le
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs :
    Finset (Fin C.layer1.length)) :
  (C.selectedLayer1CNF inputs).width ≤
    C.width
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.layer2GateFunction_hasDNFWidthLE_or_hasCNFWidthLE
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs : Finset (Fin C.layer1.length)) :
  FABL.HasDNFWidthLE (C.layer2GateFunction inputs) C.width ∨
    FABL.HasCNFWidthLE (C.layer2GateFunction inputs) C.width
    theorem FABL.DepthCircuit.layer2GateFunction_hasDNFWidthLE_or_hasCNFWidthLE
  {n : ℕ} (C : FABL.DepthCircuit n)
  (inputs :
    Finset (Fin C.layer1.length)) :
  FABL.HasDNFWidthLE
      (C.layer2GateFunction inputs)
      C.width ∨
    FABL.HasCNFWidthLE
      (C.layer2GateFunction inputs)
      C.width
    Every layer-two gate has the DNF/CNF width premise required by Håstad's Switching Lemma.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.toBooleanFunction_hasDNFWidthLE_or_hasCNFWidthLE_of_depth_eq_two
  {n : ℕ} (C : FABL.DepthCircuit n) (hdepth : C.depth = 2) :
  FABL.HasDNFWidthLE C.toBooleanFunction C.width ∨
    FABL.HasCNFWidthLE C.toBooleanFunction C.width
    theorem FABL.DepthCircuit.toBooleanFunction_hasDNFWidthLE_or_hasCNFWidthLE_of_depth_eq_two
  {n : ℕ} (C : FABL.DepthCircuit n)
  (hdepth : C.depth = 2) :
  FABL.HasDNFWidthLE C.toBooleanFunction
      C.width ∨
    FABL.HasCNFWidthLE C.toBooleanFunction
      C.width
    The depth-two case of the structural premise for Håstad's Switching Lemma.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.size_ofDNF {n : ℕ} (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF formula).size = formula.size
    theorem FABL.DepthCircuit.size_ofDNF {n : ℕ}
  (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF formula).size =
    formula.size
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.width_ofDNF {n : ℕ} (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF formula).width = formula.width
    theorem FABL.DepthCircuit.width_ofDNF {n : ℕ}
  (formula : FABL.DNFFormula n) :
  (FABL.DepthCircuit.ofDNF
        formula).width =
    formula.width
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.size_ofCNF {n : ℕ} (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF formula).size = formula.size
    theorem FABL.DepthCircuit.size_ofCNF {n : ℕ}
  (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF formula).size =
    formula.size
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.width_ofCNF {n : ℕ} (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF formula).width = formula.width
    theorem FABL.DepthCircuit.width_ofCNF {n : ℕ}
  (formula : FABL.CNFFormula n) :
  (FABL.DepthCircuit.ofCNF
        formula).width =
    formula.width
  • defdefined in FABL/Chapter04/Circuits.lean
    complete
    def FABL.DepthCircuit.HasDepthCircuit {n : ℕ} (f : FABL.BooleanFunction n)
  (d s w : ℕ) : Prop
    def FABL.DepthCircuit.HasDepthCircuit {n : ℕ}
  (f : FABL.BooleanFunction n)
  (d s w : ℕ) : Prop
    Predicate: computable by a depth-`d` circuit of size at most `s` and width at most `w`.
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.hasDepthCircuit_toBooleanFunction {n : ℕ}
  (C : FABL.DepthCircuit n) :
  FABL.DepthCircuit.HasDepthCircuit C.toBooleanFunction C.depth C.size
    C.width
    theorem FABL.DepthCircuit.hasDepthCircuit_toBooleanFunction
  {n : ℕ} (C : FABL.DepthCircuit n) :
  FABL.DepthCircuit.HasDepthCircuit
    C.toBooleanFunction C.depth C.size
    C.width
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.hasDepthCircuit_ofDNF {n : ℕ}
  (formula : FABL.DNFFormula n) :
  FABL.DepthCircuit.HasDepthCircuit formula.toBooleanFunction 2
    formula.size formula.width
    theorem FABL.DepthCircuit.hasDepthCircuit_ofDNF
  {n : ℕ} (formula : FABL.DNFFormula n) :
  FABL.DepthCircuit.HasDepthCircuit
    formula.toBooleanFunction 2
    formula.size formula.width
  • theoremdefined in FABL/Chapter04/Circuits.lean
    complete
    theorem FABL.DepthCircuit.hasDepthCircuit_ofCNF {n : ℕ}
  (formula : FABL.CNFFormula n) :
  FABL.DepthCircuit.HasDepthCircuit formula.toBooleanFunction 2
    formula.size formula.width
    theorem FABL.DepthCircuit.hasDepthCircuit_ofCNF
  {n : ℕ} (formula : FABL.CNFFormula n) :
  FABL.DepthCircuit.HasDepthCircuit
    formula.toBooleanFunction 2
    formula.size formula.width
Lemma4.5.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
Proposition 4.1.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-4-5fidelity-natural-ceiling-specialization

Lemma 4.28. Let f:\{-1,1\}^n\to\{-1,1\} be computable by a depth-d circuit of size s and width w, and let \epsilon\in(0,1]. Set \delta=\frac1{10w}\Bigl(\frac1{10\ell}\Bigr)^{d-2}, \qquad \ell=\log(2s/\epsilon). If (\boldsymbol J\mid\boldsymbol z) is a \delta-random restriction, then \Pr\bigl[\operatorname{DT}(f_{\boldsymbol J\mid\boldsymbol z})\ge\log(2/\epsilon)\bigr] \le\epsilon.

Round the logarithmic decision-tree and width thresholds up to natural numbers, with s,w>0. When \log_2(2s/\epsilon) is nonintegral, the resulting restriction rate is slightly smaller than the printed real-log rate.

Lean code for Lemma4.5.3●5 declarations
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.switchingLayerRate (w : ℕ) : ℝ
    def FABL.switchingLayerRate (w : ℕ) : ℝ
    The single-layer restriction rate used in the LMN depth reduction.
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.circuitCompressionRate (w ℓ r : ℕ) : ℝ
    def FABL.circuitCompressionRate (w ℓ r : ℕ) :
  ℝ
    Restriction rate after one width-`w` layer and `r` width-`ℓ` layers.
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.lmnLayerCutoff (s : ℕ) (ε : ℝ) : ℕ
    def FABL.lmnLayerCutoff (s : ℕ) (ε : ℝ) : ℕ
    Integer interpretation of the book's `ℓ = log₂(2s / ε)`.
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.lmnOutputCutoff (ε : ℝ) : ℕ
    def FABL.lmnOutputCutoff (ε : ℝ) : ℕ
    Integer interpretation of the book's final threshold `log₂(2 / ε)`.
  • theoremdefined in FABL/Chapter04/LMN.lean
    complete
    theorem FABL.lemma4_28 {n : ℕ} {f : FABL.BooleanFunction n} {d s w : ℕ}
  (hf : FABL.DepthCircuit.HasDepthCircuit f d s w) {ε : ℝ} (hε0 : 0 < ε)
  (hε1 : ε ≤ 1) (hs : 0 < s) (hw : 0 < w) :
  FABL.switchingFailureProbability f
      (FABL.circuitCompressionRate w (FABL.lmnLayerCutoff s ε) (d - 2))
      (FABL.lmnOutputCutoff ε) ≤
    ε
    theorem FABL.lemma4_28 {n : ℕ}
  {f : FABL.BooleanFunction n} {d s w : ℕ}
  (hf :
    FABL.DepthCircuit.HasDepthCircuit f d
      s w)
  {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1)
  (hs : 0 < s) (hw : 0 < w) :
  FABL.switchingFailureProbability f
      (FABL.circuitCompressionRate w
        (FABL.lmnLayerCutoff s ε) (d - 2))
      (FABL.lmnOutputCutoff ε) ≤
    ε
    O'Donnell, Lemma 4.28, with logarithms interpreted by the explicit natural ceilings.
Theorem4.5.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.5.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-4-5fidelity-finite-explicit-asymptotic-bridge

LMN Theorem (Linial–Mansour–Nisan). Let f:\{-1,1\}^n\to\{-1,1\} be computable by a depth-d circuit of size s>1 and let \epsilon\in(0,1/2]. Then the Fourier spectrum of f is \epsilon-concentrated up to degree O\bigl(\log(s/\epsilon)\bigr)^{d-1}\cdot\log(1/\epsilon).

Rounding the logarithmic thresholds in Lemma 4.28 gives a natural-number cutoff of the displayed asymptotic order.

Lean code for Theorem4.5.4●3 declarations
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.lmnWidthCutoff (s : ℕ) (ε : ℝ) : ℕ
    def FABL.lmnWidthCutoff (s : ℕ) (ε : ℝ) : ℕ
    Width retained after the Proposition 4.9 truncation step in the LMN proof.
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.lmnDegreeCutoff (d s : ℕ) (ε : ℝ) : ℕ
    def FABL.lmnDegreeCutoff (d s : ℕ) (ε : ℝ) : ℕ
    Exact natural degree cutoff in the finite form of the LMN theorem.
  • theoremdefined in FABL/Chapter04/LMN.lean
    complete
    theorem FABL.lmn_theorem {n : ℕ} {f : FABL.BooleanFunction n} {d s : ℕ}
  (hf : ∃ w, FABL.DepthCircuit.HasDepthCircuit f d s w) {ε : ℝ}
  (hε0 : 0 < ε) (hε1 : ε ≤ 1 / 2) (hs : 1 < s) :
  FABL.IsFourierSpectrumConcentratedUpTo f.toReal ε
    ↑(FABL.lmnDegreeCutoff d s ε)
    theorem FABL.lmn_theorem {n : ℕ}
  {f : FABL.BooleanFunction n} {d s : ℕ}
  (hf :
    ∃ w,
      FABL.DepthCircuit.HasDepthCircuit f
        d s w)
  {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1 / 2)
  (hs : 1 < s) :
  FABL.IsFourierSpectrumConcentratedUpTo
    f.toReal ε
    ↑(FABL.lmnDegreeCutoff d s ε)
    O'Donnell's LMN Theorem with its finite explicit degree cutoff.
Lemma4.5.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.
uses 0used by 0XL∃∀N
Tagssection-4-5external-resultunformalized

Remark 4.29. Håstad has slightly sharpened the degree bound in the LMN Theorem to O\bigl(\log(s/\epsilon)\bigr)^{d-2}\cdot\log s\cdot\log(1/\epsilon). This strengthening uses Håstad's sharper switching argument.

Lemma4.5.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 4
Statement dependency previews
Preview
Lemma 4.3.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-4-5supportfidelity-finite-explicit-asymptotic-bridge

Exercise 4.20. A (d,w,s')-circuit is a depth-d circuit of width at most w with at most s' nodes at layers 2 through d. By induction on d\ge2, every f:\{-1,1\}^n\to\{-1,1\} computable by a (d,w,s')-circuit satisfies \mathbf I[f]\le w\cdot O(\log s')^{d-2}. Deduce Theorem 4.30. In fact, \mathbf I[f] \le 2w\left[ 20\left(\left\lceil\log_2(s'+1)\right\rceil+2\right) \right]^{d-2}.

Lean code for Lemma4.5.6●4 declarations
  • defdefined in FABL/Chapter04/CircuitInfluence.lean
    complete
    def FABL.DepthCircuit.HasDepthWidthTailSizeCircuit {n : ℕ}
  (f : FABL.BooleanFunction n) (d w s' : ℕ) : Prop
    def FABL.DepthCircuit.HasDepthWidthTailSizeCircuit
  {n : ℕ} (f : FABL.BooleanFunction n)
  (d w s' : ℕ) : Prop
    The exact `(d,w,s')` circuit predicate from Exercise 4.20.  The final `+1` counts the
singleton output node, so the tail count covers precisely layers `2` through `d`.
  • theoremdefined in FABL/Chapter04/CircuitInfluence.lean
    complete
    theorem FABL.DepthCircuit.exercise4_20 {n : ℕ} {f : FABL.BooleanFunction n}
  {d w s' : ℕ}
  (hf : FABL.DepthCircuit.HasDepthWidthTailSizeCircuit f d w s') :
  FABL.totalInfluence f.toReal ≤
    2 * ↑w * FABL.circuitInfluenceStep s' ^ (d - 2)
    theorem FABL.DepthCircuit.exercise4_20 {n : ℕ}
  {f : FABL.BooleanFunction n}
  {d w s' : ℕ}
  (hf :
    FABL.DepthCircuit.HasDepthWidthTailSizeCircuit
      f d w s') :
  FABL.totalInfluence f.toReal ≤
    2 * ↑w *
      FABL.circuitInfluenceStep s' ^
        (d - 2)
    O'Donnell, Exercise 4.20(a), with an explicit constant.
  • defdefined in FABL/Chapter04/CircuitInfluence.lean
    complete
    def FABL.DepthCircuit.HasDepthSizeCircuit {n : ℕ}
  (f : FABL.BooleanFunction n) (d s : ℕ) : Prop
    def FABL.DepthCircuit.HasDepthSizeCircuit
  {n : ℕ} (f : FABL.BooleanFunction n)
  (d s : ℕ) : Prop
    Computability by a depth-`d`, size-at-most-`s` circuit, with no width hypothesis.
  • theoremdefined in FABL/Chapter04/CircuitInfluence.lean
    complete
    theorem FABL.DepthCircuit.exercise4_20b {n : ℕ} {f : FABL.BooleanFunction n}
  {d s : ℕ} (hf : FABL.DepthCircuit.HasDepthSizeCircuit f d s) :
  FABL.totalInfluence f.toReal ≤
    4 * ↑(FABL.DepthCircuit.initialRestrictionWidth s) *
      FABL.circuitInfluenceStep (s + 1) ^ (d - 2)
    theorem FABL.DepthCircuit.exercise4_20b {n : ℕ}
  {f : FABL.BooleanFunction n} {d s : ℕ}
  (hf :
    FABL.DepthCircuit.HasDepthSizeCircuit
      f d s) :
  FABL.totalInfluence f.toReal ≤
    4 *
        ↑(FABL.DepthCircuit.initialRestrictionWidth
            s) *
      FABL.circuitInfluenceStep (s + 1) ^
        (d - 2)
    O'Donnell, Exercise 4.20(b), with an explicit constant.
Theorem4.5.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.
uses 1used by 0✓L∃∀N
Tagssection-4-5fidelity-finite-explicit-asymptotic-bridge

Theorem 4.30. Let f:\{-1,1\}^n\to\{-1,1\} be computable by a depth-d circuit of size s. Then \mathbf I[f]\le O(\log s)^{d-1}. More explicitly, \mathbf I[f] \le 4\left[ 20\left(\left\lceil\log_2(s+2)\right\rceil+2\right) \right]^{d-1}.

Lean code for Theorem4.5.7●1 theorem
  • theoremdefined in FABL/Chapter04/CircuitInfluence.lean
    complete
    theorem FABL.DepthCircuit.theorem4_30 {n : ℕ} {f : FABL.BooleanFunction n}
  {d s : ℕ} (hf : FABL.DepthCircuit.HasDepthSizeCircuit f d s) :
  FABL.totalInfluence f.toReal ≤
    4 * FABL.circuitInfluenceStep (s + 1) ^ (d - 1)
    theorem FABL.DepthCircuit.theorem4_30 {n : ℕ}
  {f : FABL.BooleanFunction n} {d s : ℕ}
  (hf :
    FABL.DepthCircuit.HasDepthSizeCircuit
      f d s) :
  FABL.totalInfluence f.toReal ≤
    4 *
      FABL.circuitInfluenceStep (s + 1) ^
        (d - 1)
    O'Donnell, Theorem 4.30, with an explicit bound implying the stated
`O(log s)^(d-1)` estimate at every fixed depth.
Theorem4.5.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 3.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-4-5fidelity-finite-executable-asymptotic-bridge

Theorem 4.31. Let \mathcal C be the class of functions f:\{-1,1\}^n\to\{-1,1\} computable by depth-d circuits of size \operatorname{poly}(n). Then \mathcal C can be learned from random examples with error any \epsilon=1/\operatorname{poly}(n) in time n^{O(\log^d n)}. Equivalently, the complexity class \mathrm{AC}^0 is learnable in quasipolynomial time. For fixed d, the explicit LMN degree and the random-example learner of Theorem 3.29 give the displayed quasipolynomial bound.

Lean code for Theorem4.5.8●5 declarations
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.depthSizeCircuitClass (n d s : ℕ) : Set (FABL.BooleanFunction n)
    def FABL.depthSizeCircuitClass (n d s : ℕ) :
  Set (FABL.BooleanFunction n)
    Boolean functions computable by a depth-`d` circuit of size at most `s`, with no artificial
restriction on the bottom fan-in.
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.lmnCircuitLearningDegree (d size : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) : ℕ
    def FABL.lmnCircuitLearningDegree (d size : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) :
  ℕ
    Degree used by the LMN Low-Degree learner at half of the requested classification error.
  • defdefined in FABL/Chapter04/LMN.lean
    complete
    def FABL.lmnCircuitLearnerWorkCost (n d size : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) : ℕ
    def FABL.lmnCircuitLearnerWorkCost
  (n d size : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) :
  ℕ
    Exact target-independent work schedule of the LMN Low-Degree learner.
  • theoremdefined in FABL/Chapter04/LMN.lean
    complete
    theorem FABL.theorem4_31 {n : ℕ} (d size : ℕ) (hsize : 1 < size)
  (ε : ↑FABL.PositiveLearningParameter) :
  (∀ target ∈ FABL.depthSizeCircuitClass n d size,
      ((FABL.lowDegreeFourierEstimatorProgram n
              (FABL.lmnCircuitLearningDegree d size ε)
              ε).eventProbability
          target fun outcome =>
          ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
        1 / 10) ∧
    ∀ (target : FABL.BooleanFunction n),
      ∀
        outcome ∈
          (FABL.LearningProgram.runWithCost target
              (FABL.lowDegreeFourierEstimatorProgram n
                (FABL.lmnCircuitLearningDegree d size ε) ε)).support,
        outcome.2.randomExamples ≤
            FABL.lmnCircuitLearnerWorkCost n d size ε ∧
          outcome.2.queries = 0 ∧
            outcome.2.work ≤ FABL.lmnCircuitLearnerWorkCost n d size ε
    theorem FABL.theorem4_31 {n : ℕ} (d size : ℕ)
  (hsize : 1 < size)
  (ε : ↑FABL.PositiveLearningParameter) :
  (∀
      target ∈
        FABL.depthSizeCircuitClass n d
          size,
      ((FABL.lowDegreeFourierEstimatorProgram
              n
              (FABL.lmnCircuitLearningDegree
                d size ε)
              ε).eventProbability
          target fun outcome =>
          ↑↑ε <
            FABL.relativeHammingDist
              target outcome.1.evaluate) ≤
        1 / 10) ∧
    ∀ (target : FABL.BooleanFunction n),
      ∀
        outcome ∈
          (FABL.LearningProgram.runWithCost
              target
              (FABL.lowDegreeFourierEstimatorProgram
                n
                (FABL.lmnCircuitLearningDegree
                  d size ε)
                ε)).support,
        outcome.2.randomExamples ≤
            FABL.lmnCircuitLearnerWorkCost
              n d size ε ∧
          outcome.2.queries = 0 ∧
            outcome.2.work ≤
              FABL.lmnCircuitLearnerWorkCost
                n d size ε
    O'Donnell, Theorem 4.31, as an executable random-example learner with exact pathwise cost.
  • theoremdefined in FABL/Chapter04/LMN.lean
    complete
    theorem FABL.card_lmnCircuitLearningFamily_le {n : ℕ} (d size : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) :
  (FABL.lowDegreeFourierFamily n
        (FABL.lmnCircuitLearningDegree d size ε)).card ≤
    (FABL.lmnCircuitLearningDegree d size ε + 1) *
      (n + 1) ^ FABL.lmnCircuitLearningDegree d size ε
    theorem FABL.card_lmnCircuitLearningFamily_le
  {n : ℕ} (d size : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) :
  (FABL.lowDegreeFourierFamily n
        (FABL.lmnCircuitLearningDegree d
          size ε)).card ≤
    (FABL.lmnCircuitLearningDegree d size
          ε +
        1) *
      (n + 1) ^
        FABL.lmnCircuitLearningDegree d
          size ε
    The number of Fourier coefficients learned in Theorem 4.31 has the standard explicit
`(k + 1) * (n + 1)^k` bound.
Lemma4.5.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 3
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-5supportfidelity-exact-explicit-root-scale-bound

Exercise 4.12 (parity formula tightness and circuit upper bounds). (a) The parity \chi_{[n]} is computed by a DNF (or CNF) of size 2^{n-1}. (b) This size bound is tight: every term in such a DNF, and dually every clause in such a CNF, must have width exactly n. (c) There is a depth-3 circuit of size O(n^{1/2})\cdot 2^{n^{1/2}} computing \chi_{[n]}. (d) More generally, for every d\ge2 there is a depth-d circuit of size O\bigl(n^{1-1/(d-1)}\bigr)\cdot 2^{n^{1/(d-1)}} computing \chi_{[n]}. For n>0, the exact DNF and CNF size is 2^{n-1}, and every term or clause has full width. For the circuit construction, take block side \max(1,\lceil n^{1/(d-1)}\rceil). The resulting finite size bound and the identity (n^{1/(d-1)})^{d-2}=n^{1-1/(d-1)} give an explicit finite root-scale envelope corresponding to the displayed asymptotic, including the d=2 endpoint and non-perfect-power dimensions.

Lean code for Lemma4.5.9●22 declarations
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.DNFFormula.term_width_eq_dimension_of_computes_parity {n : ℕ}
  (φ : FABL.DNFFormula n)
  (hφ : φ.toBooleanFunction = FABL.parityFunction Finset.univ)
  (T : FABL.DNFTerm n) (hT : T ∈ φ.terms) : T.width = n
    theorem FABL.DNFFormula.term_width_eq_dimension_of_computes_parity
  {n : ℕ} (φ : FABL.DNFFormula n)
  (hφ :
    φ.toBooleanFunction =
      FABL.parityFunction Finset.univ)
  (T : FABL.DNFTerm n)
  (hT : T ∈ φ.terms) : T.width = n
    Exercise 4.12(b): every term in a DNF computing parity has width exactly `n`.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.DNFFormula.size_lower_bound_of_computes_parity {n : ℕ} (hn : 0 < n)
  (φ : FABL.DNFFormula n)
  (hφ : φ.toBooleanFunction = FABL.parityFunction Finset.univ) :
  2 ^ (n - 1) ≤ φ.size
    theorem FABL.DNFFormula.size_lower_bound_of_computes_parity
  {n : ℕ} (hn : 0 < n)
  (φ : FABL.DNFFormula n)
  (hφ :
    φ.toBooleanFunction =
      FABL.parityFunction Finset.univ) :
  2 ^ (n - 1) ≤ φ.size
    Every DNF computing nonconstant full parity has at least `2 ^ (n - 1)` terms.
  • defdefined in FABL/Chapter04/Parity.lean
    complete
    def FABL.parityDNF (n : ℕ) : FABL.DNFFormula n
    def FABL.parityDNF (n : ℕ) : FABL.DNFFormula n
    Exercise 4.12(a): canonical optimal DNF for full parity.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.parityDNF_toBooleanFunction (n : ℕ) :
  (FABL.parityDNF n).toBooleanFunction = FABL.parityFunction Finset.univ
    theorem FABL.parityDNF_toBooleanFunction (n : ℕ) :
  (FABL.parityDNF n).toBooleanFunction =
    FABL.parityFunction Finset.univ
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.size_parityDNF {n : ℕ} (hn : 0 < n) :
  (FABL.parityDNF n).size = 2 ^ (n - 1)
    theorem FABL.size_parityDNF {n : ℕ} (hn : 0 < n) :
  (FABL.parityDNF n).size = 2 ^ (n - 1)
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.DNFsize_parityFunction_univ {n : ℕ} (hn : 0 < n) :
  FABL.DNFsize (FABL.parityFunction Finset.univ) = 2 ^ (n - 1)
    theorem FABL.DNFsize_parityFunction_univ {n : ℕ}
  (hn : 0 < n) :
  FABL.DNFsize
      (FABL.parityFunction Finset.univ) =
    2 ^ (n - 1)
    Exercise 4.12(a)–(b): the least DNF size of nonconstant parity is `2 ^ (n - 1)`.
  • defdefined in FABL/Chapter04/Parity.lean
    complete
    def FABL.parityCNF (n : ℕ) : FABL.CNFFormula n
    def FABL.parityCNF (n : ℕ) : FABL.CNFFormula n
    Exercise 4.12(a): canonical CNF for full parity, obtained from its Boolean dual.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.size_parityCNF {n : ℕ} (hn : 0 < n) :
  (FABL.parityCNF n).size = 2 ^ (n - 1)
    theorem FABL.size_parityCNF {n : ℕ} (hn : 0 < n) :
  (FABL.parityCNF n).size = 2 ^ (n - 1)
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.parityCNF_toBooleanFunction (n : ℕ) :
  (FABL.parityCNF n).toBooleanFunction = FABL.parityFunction Finset.univ
    theorem FABL.parityCNF_toBooleanFunction (n : ℕ) :
  (FABL.parityCNF n).toBooleanFunction =
    FABL.parityFunction Finset.univ
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.CNFFormula.clause_width_eq_dimension_of_computes_parity {n : ℕ}
  (ψ : FABL.CNFFormula n)
  (hψ : ψ.toBooleanFunction = FABL.parityFunction Finset.univ)
  (C : FABL.DNFTerm n) (hC : C ∈ ψ.clauses) : C.width = n
    theorem FABL.CNFFormula.clause_width_eq_dimension_of_computes_parity
  {n : ℕ} (ψ : FABL.CNFFormula n)
  (hψ :
    ψ.toBooleanFunction =
      FABL.parityFunction Finset.univ)
  (C : FABL.DNFTerm n)
  (hC : C ∈ ψ.clauses) : C.width = n
    Exercise 4.12(b), CNF form: every clause in a CNF computing parity has width `n`.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.CNFFormula.size_lower_bound_of_computes_parity {n : ℕ} (hn : 0 < n)
  (ψ : FABL.CNFFormula n)
  (hψ : ψ.toBooleanFunction = FABL.parityFunction Finset.univ) :
  2 ^ (n - 1) ≤ ψ.size
    theorem FABL.CNFFormula.size_lower_bound_of_computes_parity
  {n : ℕ} (hn : 0 < n)
  (ψ : FABL.CNFFormula n)
  (hψ :
    ψ.toBooleanFunction =
      FABL.parityFunction Finset.univ) :
  2 ^ (n - 1) ≤ ψ.size
    Exercise 4.12(b), CNF form: every CNF for nonconstant parity has at least
`2 ^ (n - 1)` clauses.
  • defdefined in FABL/Chapter04/Parity.lean
    complete
    def FABL.parityDepthCircuitFromBlocks (n r q : ℕ) : FABL.DepthCircuit n
    def FABL.parityDepthCircuitFromBlocks
  (n r q : ℕ) : FABL.DepthCircuit n
    Exercise 4.12(c)-(d), parameterized construction. Here `q + 2 = d - 1` is the number
of non-output internal layers, so the circuit depth is `q + 3`.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.depth_parityDepthCircuitFromBlocks (n r q : ℕ) :
  (FABL.parityDepthCircuitFromBlocks n r q).depth = q + 3
    theorem FABL.depth_parityDepthCircuitFromBlocks
  (n r q : ℕ) :
  (FABL.parityDepthCircuitFromBlocks n r
        q).depth =
    q + 3
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.size_parityDepthCircuitFromBlocks (n r q : ℕ) :
  (FABL.parityDepthCircuitFromBlocks n r q).size =
    ∑ k ∈ Finset.range (q + 2), FABL.parityLayerSize r k
    theorem FABL.size_parityDepthCircuitFromBlocks
  (n r q : ℕ) :
  (FABL.parityDepthCircuitFromBlocks n r
        q).size =
    ∑ k ∈ Finset.range (q + 2),
      FABL.parityLayerSize r k
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.toBooleanFunction_parityDepthCircuitFromBlocks (n r q : ℕ)
  (hcover : n ≤ r ^ (q + 2)) :
  (FABL.parityDepthCircuitFromBlocks n r q).toBooleanFunction =
    FABL.parityFunction Finset.univ
    theorem FABL.toBooleanFunction_parityDepthCircuitFromBlocks
  (n r q : ℕ) (hcover : n ≤ r ^ (q + 2)) :
  (FABL.parityDepthCircuitFromBlocks n r
        q).toBooleanFunction =
    FABL.parityFunction Finset.univ
  • defdefined in FABL/Chapter04/Parity.lean
    complete
    def FABL.parityRealRoot (n h : ℕ) : ℝ
    def FABL.parityRealRoot (n h : ℕ) : ℝ
    Real `h`th root used by the canonical block decomposition.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.parityRealRoot_pow_pred (n h : ℕ) (hh : 0 < h) :
  FABL.parityRealRoot n h ^ (h - 1) = ↑n ^ (1 - (↑h)⁻¹)
    theorem FABL.parityRealRoot_pow_pred (n h : ℕ)
  (hh : 0 < h) :
  FABL.parityRealRoot n h ^ (h - 1) =
    ↑n ^ (1 - (↑h)⁻¹)
    The polynomial part of the block count is exactly the exponent appearing in the book.
  • defdefined in FABL/Chapter04/Parity.lean
    complete
    def FABL.parityBlockSide (n h : ℕ) : ℕ
    def FABL.parityBlockSide (n h : ℕ) : ℕ
    Ceiling of the real `h`th root, clamped to one so every block has a genuine arity.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.parityBlockSide_pow_covers (n h : ℕ) (hh : 0 < h) :
  n ≤ FABL.parityBlockSide n h ^ h
    theorem FABL.parityBlockSide_pow_covers (n h : ℕ)
  (hh : 0 < h) :
  n ≤ FABL.parityBlockSide n h ^ h
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.canonicalParityCircuit_size_real_le (n q : ℕ) :
  ↑(FABL.parityDepthCircuitFromBlocks n (FABL.parityBlockSide n (q + 2))
          q).size ≤
    (↑q + 2) * (FABL.parityRealRoot n (q + 2) + 1) ^ (q + 1) *
      2 ^ (FABL.parityRealRoot n (q + 2) + 1)
    theorem FABL.canonicalParityCircuit_size_real_le
  (n q : ℕ) :
  ↑(FABL.parityDepthCircuitFromBlocks n
          (FABL.parityBlockSide n (q + 2))
          q).size ≤
    (↑q + 2) *
        (FABL.parityRealRoot n (q + 2) +
            1) ^
          (q + 1) *
      2 ^
        (FABL.parityRealRoot n (q + 2) +
          1)
    Root-scale envelope for the canonical circuit. This is the explicit finite inequality behind
`O(n^(1-1/(d-1))) * 2^(n^(1/(d-1)))`; the two `+1`s are absorbed by constant factors.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.hasDepthCircuit_parity_depth_three (n : ℕ) :
  FABL.DepthCircuit.HasDepthCircuit (FABL.parityFunction Finset.univ) 3
    (2 * FABL.parityBlockSide n 2 * 2 ^ FABL.parityBlockSide n 2) n
    theorem FABL.hasDepthCircuit_parity_depth_three
  (n : ℕ) :
  FABL.DepthCircuit.HasDepthCircuit
    (FABL.parityFunction Finset.univ) 3
    (2 * FABL.parityBlockSide n 2 *
      2 ^ FABL.parityBlockSide n 2)
    n
    Exercise 4.12(c): the depth-three square-root block construction.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.hasDepthCircuit_parity_general (n d : ℕ) (hd : 2 ≤ d) :
  FABL.DepthCircuit.HasDepthCircuit (FABL.parityFunction Finset.univ) d
    ((d - 1) * FABL.parityBlockSide n (d - 1) ^ (d - 2) *
      2 ^ FABL.parityBlockSide n (d - 1))
    n
    theorem FABL.hasDepthCircuit_parity_general
  (n d : ℕ) (hd : 2 ≤ d) :
  FABL.DepthCircuit.HasDepthCircuit
    (FABL.parityFunction Finset.univ) d
    ((d - 1) *
        FABL.parityBlockSide n (d - 1) ^
          (d - 2) *
      2 ^ FABL.parityBlockSide n (d - 1))
    n
    Exercise 4.12(d) with the book's full range `d ≥ 2`, parity target, and layered alternating
circuit model.
Corollary4.5.10
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.
uses 1used by 0✓L∃∀N
Tagssection-4-5fidelity-finite-inverse-cutoff-asymptotic-bridge

Corollary 4.32. Fix any constant \epsilon_0>0. Suppose C is a depth-d circuit over \{-1,1\}^n with \Pr_{\boldsymbol x}[C(\boldsymbol x)=\chi_{[n]}(\boldsymbol x)]\ge\frac12+\epsilon_0. Then the size of C is at least 2^{\Omega\bigl(n^{1/(d-1)}\bigr)}. More precisely, every s>1 whose LMN cutoff is below n is strictly smaller than the circuit size. Inverting this cutoff gives the displayed 2^{\Omega(n^{1/(d-1)})} lower bound.

Lean code for Corollary4.5.10●3 theorems
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.fourierCoeff_univ_eq_two_mul_parityAgreement_sub_one {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.fourierCoeff f.toReal Finset.univ =
    (2 *
        FABL.uniformProbability fun x =>
          f x = FABL.parityFunction Finset.univ x) -
      1
    theorem FABL.fourierCoeff_univ_eq_two_mul_parityAgreement_sub_one
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.fourierCoeff f.toReal Finset.univ =
    (2 *
        FABL.uniformProbability fun x =>
          f x =
            FABL.parityFunction
              Finset.univ x) -
      1
    The top Fourier coefficient is twice the agreement advantage over one half with parity.
  • theoremdefined in FABL/Chapter04/Parity.lean
    complete
    theorem FABL.parityAgreement_forces_concentration_cutoff {n : ℕ}
  (f : FABL.BooleanFunction n) {ε₀ ε k : ℝ} (hε₀ : 0 < ε₀)
  (hε : ε < 4 * ε₀ ^ 2)
  (hagreement :
    1 / 2 + ε₀ ≤
      FABL.uniformProbability fun x =>
        f x = FABL.parityFunction Finset.univ x)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedUpTo f.toReal ε k) :
  ↑n ≤ k
    theorem FABL.parityAgreement_forces_concentration_cutoff
  {n : ℕ} (f : FABL.BooleanFunction n)
  {ε₀ ε k : ℝ} (hε₀ : 0 < ε₀)
  (hε : ε < 4 * ε₀ ^ 2)
  (hagreement :
    1 / 2 + ε₀ ≤
      FABL.uniformProbability fun x =>
        f x =
          FABL.parityFunction Finset.univ
            x)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedUpTo
      f.toReal ε k) :
  ↑n ≤ k
    If a Boolean function has constant agreement advantage `ε₀` with parity, then a Fourier
concentration error below `4 ε₀²` cannot use a cutoff below the top degree.
  • theoremdefined in FABL/Chapter04/LMN.lean
    complete
    theorem FABL.DepthCircuit.corollary4_32 {n : ℕ} (C : FABL.DepthCircuit n)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hagreement :
    1 / 2 + ε₀ ≤
      FABL.uniformProbability fun x =>
        C.toBooleanFunction x = FABL.parityFunction Finset.univ x)
  (s : ℕ) :
  1 < s → FABL.lmnDegreeCutoff C.depth s (2 * ε₀ ^ 2) < n → s < C.size
    theorem FABL.DepthCircuit.corollary4_32 {n : ℕ}
  (C : FABL.DepthCircuit n) {ε₀ : ℝ}
  (hε₀ : 0 < ε₀)
  (hagreement :
    1 / 2 + ε₀ ≤
      FABL.uniformProbability fun x =>
        C.toBooleanFunction x =
          FABL.parityFunction Finset.univ
            x)
  (s : ℕ) :
  1 < s →
    FABL.lmnDegreeCutoff C.depth s
          (2 * ε₀ ^ 2) <
        n →
      s < C.size
    O'Donnell, Corollary 4.32, in exact finite inverse-cutoff form.