Unrestricted depth-three lower bound: correlation transfer

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

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

theorem Complexity.DepthThreeLowerBound.restrictionAvg_mask_le {V : Type uDepth1} [Fintype V] {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (W : Restriction V → ℝ) (hW : ∀ (σ : Restriction V), 0 ≤ W σ) (good : Restriction V → Prop) : (restrictionAvg p fun (σ : Restriction V) => if good σ then W σ else 0) ≤ restrictionAvg p W

theorem Complexity.DepthThreeLowerBound.restrictionAvg_abs_le_split {V : Type uDepth1} [Fintype V] {p ε δ C : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (hε : 0 ≤ ε) (q W : Restriction V → ℝ) (good : Restriction V → Prop) (hW : ∀ (σ : Restriction V), 0 ≤ W σ) (hmean : restrictionAvg p W ≤ C) (hgood : ∀ (σ : Restriction V), good σ → |q σ| ≤ ε * W σ) (hunit : ∀ (σ : Restriction V), |q σ| ≤ 1) (hbad : (restrictionAvg p fun (σ : Restriction V) => if ¬good σ then 1 else 0) ≤ δ) : |restrictionAvg p q| ≤ ε * C + δ

theorem Complexity.DepthThreeLowerBound.abs_finiteAvg_sign_indicator_le_one {Z : Type uDepth2} [Fintype Z] (f J : Cube Z → Bool) : |finiteAvg fun (x : Cube Z) => sign (f x) * indicator (J x)| ≤ 1

theorem Complexity.DepthThreeLowerBound.restriction_correlation_transfer {V : Type uDepth1} [Fintype V] [instDecidableEqV : DecidableEq V] {p ε δ C : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (hε : 0 ≤ ε) (f : Cube V → Bool) (H : CNF V) (b : ℕ) (good : Restriction V → Prop) (W : Restriction V → ℝ) (hW : ∀ (σ : Restriction V), 0 ≤ W σ) (hmean : restrictionAvg p W ≤ C) (hdom : ∀ (σ : Restriction V), |finiteAvg fun (z : Cube (Live σ)) => sign (f (fill σ z)) * indicator (H.eval (fill σ z))| ≤ W σ * corr b fun (z : Cube (Live σ)) => sign (f (fill σ z))) (hgood : ∀ (σ : Restriction V), good σ → (corr b fun (z : Cube (Live σ)) => sign (f (fill σ z))) ≤ ε) (hbad : (restrictionAvg p fun (σ : Restriction V) => if ¬good σ then 1 else 0) ≤ δ) : |finiteAvg fun (x : Cube V) => sign (f x) * indicator (H.eval x)| ≤ ε * C + δ

theorem Complexity.DepthThreeLowerBound.restriction_correlation_transfer_six {V : Type uDepth1} [Fintype V] [instDecidableEqV : DecidableEq V] {p ε : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (hε : 0 ≤ ε) (f : Cube V → Bool) (H : CNF V) (b : ℕ) (good : Restriction V → Prop) (W : Restriction V → ℝ) (hW : ∀ (σ : Restriction V), 0 ≤ W σ) (hmean : restrictionAvg p W ≤ 2) (hdom : ∀ (σ : Restriction V), |finiteAvg fun (z : Cube (Live σ)) => sign (f (fill σ z)) * indicator (H.eval (fill σ z))| ≤ W σ * corr b fun (z : Cube (Live σ)) => sign (f (fill σ z))) (hgood : ∀ (σ : Restriction V), good σ → (corr b fun (z : Cube (Live σ)) => sign (f (fill σ z))) ≤ ε) (hbad : (restrictionAvg p fun (σ : Restriction V) => if ¬good σ then 1 else 0) ≤ 4 * ε) : |finiteAvg fun (x : Cube V) => sign (f x) * indicator (H.eval x)| ≤ 6 * ε