Unrestricted depth-three lower bound: restriction correlation

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/RestrictionCorrelation.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

noncomputable def Complexity.DepthThreeLowerBound.narrowTests {V : Type uDepth1} [Fintype V] (b : ℕ) : Finset (Cube V → Bool)

The finite family of CNF tests obeying the width bound.

Equations

• Complexity.DepthThreeLowerBound.narrowTests b = {J : Complexity.DepthThreeLowerBound.Cube V → Bool | ∃ (H : Complexity.DepthThreeLowerBound.CNF V), H.WidthAtMost b ∧ H.eval = J}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_narrowTests_iff {V : Type uDepth1} [Fintype V] (b : ℕ) (J : Cube V → Bool) : J ∈ narrowTests b ↔ ∃ (H : CNF V), H.WidthAtMost b ∧ H.eval = J

theorem Complexity.DepthThreeLowerBound.eval_mem_narrowTests {V : Type uDepth1} [Fintype V] (b : ℕ) (H : CNF V) (hH : H.WidthAtMost b) : H.eval ∈ narrowTests b

theorem Complexity.DepthThreeLowerBound.narrowTests_true_mem {V : Type uDepth1} [Fintype V] (b : ℕ) : (fun (x : Cube V) => true) ∈ narrowTests b

theorem Complexity.DepthThreeLowerBound.narrowTests_false_mem {V : Type uDepth1} [Fintype V] (b : ℕ) : (fun (x : Cube V) => false) ∈ narrowTests b

theorem Complexity.DepthThreeLowerBound.narrowTests_nonempty {V : Type uDepth1} [Fintype V] (b : ℕ) : (narrowTests b).Nonempty

noncomputable def Complexity.DepthThreeLowerBound.corr {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) : ℝ

Uniform correlation with the indicator of a Boolean test.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DepthThreeLowerBound.abs_table_corr_le {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) (J : Cube V → Bool) (hJ : J ∈ narrowTests b) : |finiteAvg fun (x : Cube V) => G x * indicator (J x)| ≤ corr b G

theorem Complexity.DepthThreeLowerBound.abs_corr_le {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) (H : CNF V) (hH : H.WidthAtMost b) : |finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)| ≤ corr b G

theorem Complexity.DepthThreeLowerBound.abs_mean_le_corr {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) : |finiteAvg G| ≤ corr b G

theorem Complexity.DepthThreeLowerBound.corr_nonneg {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) : 0 ≤ corr b G

theorem Complexity.DepthThreeLowerBound.corr_le_of_forall {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) (c : ℝ) (h : ∀ (H : CNF V), H.WidthAtMost b → |finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)| ≤ c) : corr b G ≤ c

theorem Complexity.DepthThreeLowerBound.corr_attained {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) : ∃ (H : CNF V), H.WidthAtMost b ∧ corr b G = |finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)|

theorem Complexity.DepthThreeLowerBound.corr_le_abs_mean {V : Type uDepth1} [Fintype V] (b : ℕ) (G : Cube V → ℝ) : corr b G ≤ finiteAvg fun (x : Cube V) => |G x|

theorem Complexity.DepthThreeLowerBound.corr_linearCombination_identity {V : Type uDepth1} [Fintype V] {ι : Type uDepth2} (s : Finset ι) (c : ι → ℝ) (H : ι → CNF V) (G : Cube V → ℝ) : (finiteAvg fun (x : Cube V) => G x * ∑ i ∈ s, c i * indicator ((H i).eval x)) = ∑ i ∈ s, c i * finiteAvg fun (x : Cube V) => G x * indicator ((H i).eval x)

theorem Complexity.DepthThreeLowerBound.abs_corr_linearCombination_le {V : Type uDepth1} [Fintype V] {ι : Type uDepth3} (s : Finset ι) (c : ι → ℝ) (H : ι → CNF V) (b : ℕ) (G : Cube V → ℝ) (hH : ∀ i ∈ s, (H i).WidthAtMost b) : |finiteAvg fun (x : Cube V) => G x * ∑ i ∈ s, c i * indicator ((H i).eval x)| ≤ (∑ i ∈ s, |c i|) * corr b G

theorem Complexity.DepthThreeLowerBound.abs_corr_convex_mixture_le {V : Type uDepth1} [Fintype V] {ι : Type uDepth4} (s : Finset ι) (w : ι → ℝ) (H : ι → CNF V) (b : ℕ) (G : Cube V → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hsum : ∑ i ∈ s, w i = 1) (hH : ∀ i ∈ s, (H i).WidthAtMost b) : |finiteAvg fun (x : Cube V) => G x * ∑ i ∈ s, w i * indicator ((H i).eval x)| ≤ corr b G

theorem Complexity.DepthThreeLowerBound.abs_corr_uniform_mixture_le {V : Type uDepth1} [Fintype V] {ι : Type uDepth5} [Fintype ι] [Nonempty ι] (H : ι → CNF V) (b : ℕ) (G : Cube V → ℝ) (hH : ∀ (i : ι), (H i).WidthAtMost b) : |finiteAvg fun (x : Cube V) => G x * finiteAvg fun (i : ι) => indicator ((H i).eval x)| ≤ corr b G