Circuit depth classes -- proof internals

theorem Complexity.polylogDepth_zero_internal (c n : ℕ) : polylogDepth 0 c n = c

theorem Complexity.polylogDepth_one_internal (c n : ℕ) : polylogDepth 1 c n = c * Nat.log 2 n + c

theorem Complexity.polylogDepth_mono_constant_internal {c c' : ℕ} (hcc' : c ≤ c') (i n : ℕ) : polylogDepth i c n ≤ polylogDepth i c' n

theorem Complexity.polylogDepth_mono_exponent_internal {i j : ℕ} (hij : i ≤ j) (c n : ℕ) : polylogDepth i c n ≤ polylogDepth j c n

theorem Complexity.DEPTHWithBasis_mono_internal (B : Basis) {d e : ℕ → ℕ} (hde : ∀ (n : ℕ), d n ≤ e n) : DEPTHWithBasis B d ⊆ DEPTHWithBasis B e

theorem Complexity.NC_mono_internal {i j : ℕ} (hij : i ≤ j) : NC i ⊆ NC j

theorem Complexity.AC_mono_internal {i j : ℕ} (hij : i ≤ j) : AC i ⊆ AC j

theorem Complexity.TC_mono_internal {i j : ℕ} (hij : i ≤ j) : TC i ⊆ TC j

theorem Complexity.AC_subset_TC_internal (i : ℕ) : AC i ⊆ TC i

theorem Complexity.mem_NC1_iff_internal {f : BoolFunFamily} : f ∈ NC1 ↔ ∃ (F : CircuitFamily Basis.andOr2) (c : ℕ), F.Computes f ∧ F.PolynomialSize ∧ F.DepthBoundedBy fun (n : ℕ) => c * Nat.log 2 n + c

theorem Complexity.mem_AC0_iff_internal {f : BoolFunFamily} : f ∈ AC0 ↔ ∃ (F : CircuitFamily Basis.unboundedAndOr) (c : ℕ), F.Computes f ∧ F.PolynomialSize ∧ F.DepthBoundedBy fun (x : ℕ) => c

theorem Complexity.mem_TC0_iff_internal {f : BoolFunFamily} : f ∈ TC0 ↔ ∃ (F : CircuitFamily Basis.threshold) (c : ℕ), F.Computes f ∧ F.PolynomialSize ∧ F.DepthBoundedBy fun (x : ℕ) => c