From the imported correlation estimate to full-language threshold weight

Restrict each CNF feature along the hard input substitution and apply the correlation-to-margin inequality to the resulting features. The weights stay unchanged and the width bound is preserved by substitution.

theorem Complexity.DepthThreeLowerBound.finiteAvg_eq_expect {X : Type u_1} [Fintype X] (f : X → ℝ) : finiteAvg f = Finset.univ.expect fun (x : X) => f x

theorem Complexity.DepthThreeLowerBound.language_slice_threshold_weight_proof (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∃ (α : Fin n → Fin (dataDimension n) ⊕ Bool), ∀ (J : Type) [inst : Fintype J] (H : J → CNF (Fin (dataDimension n))) (a : J → ℝ), (∀ (j : J), (H j).WidthAtMost (degreeCutoff s (dataDimension n))) → (∀ (x : Cube (Fin (dataDimension n))), 1 ≤ sign (language (List.ofFn (GateInput.assignment α x))) * ∑ j : J, a j * indicator ((H j).eval x)) → 2 ^ (4 * (s + 1) * √↑(dataDimension n)) / 6 ≤ ∑ j : J, |a j|

theorem Complexity.DepthThreeLowerBound.language_threshold_weight_proof (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∀ (J : Type) [inst : Fintype J] (H : J → CNF (Fin n)) (a : J → ℝ), (∀ (j : J), (H j).WidthAtMost (degreeCutoff s (dataDimension n))) → (∀ (x : Fin n → Bool), 1 ≤ sign (language (List.ofFn x)) * ∑ j : J, a j * indicator ((H j).eval x)) → 2 ^ (4 * (s + 1) * √↑(dataDimension n)) / 6 ≤ ∑ j : J, |a j|

theorem Complexity.DepthThreeLowerBound.integer_threshold_margin (t : ℤ) : 1 ≤ sign (decide (0 ≤ t)) * (2 * ↑t + 1)

theorem Complexity.DepthThreeLowerBound.language_integer_threshold_weight_proof (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∀ (J : Type) [inst : Fintype J] (H : J → CNF (Fin n)) (z : J → ℤ), (∀ (j : J), (H j).WidthAtMost (degreeCutoff s (dataDimension n))) → (∀ (x : Fin n → Bool), language (List.ofFn x) = decide (0 ≤ ∑ j : J, z j * if (H j).eval x = true then 1 else 0)) → (2 ^ (4 * (s + 1) * √↑(dataDimension n)) / 6 - 1) / 2 ≤ ∑ j : J, |↑(z j)|