Nonuniform circuit size for promise problems -- proof internals

theorem Complexity.mem_PromiseSIZEWithBasis_iff_internal (problem : PromiseProblem) (B : Basis) (bound : ℕ → ℕ) : problem ∈ PromiseSIZEWithBasis B bound ↔ ∃ (family : CircuitFamily B), problem.SolvedBy family.evalList ∧ family.SizeBoundedBy bound

theorem Complexity.mem_PromiseSIZE_iff_internal (problem : PromiseProblem) (bound : ℕ → ℕ) : problem ∈ PromiseSIZE bound ↔ ∃ (family : CircuitFamily Basis.andOr2), problem.SolvedBy family.evalList ∧ family.SizeBoundedBy bound

theorem Complexity.mem_PromisePPoly_iff_internal (problem : PromiseProblem) : problem ∈ PromisePPoly ↔ ∃ (family : CircuitFamily Basis.andOr2), problem.SolvedBy family.evalList ∧ family.PolynomialSize

theorem Complexity.CircuitFamily.SizeBoundedBy.eventuallySizeBoundedBy_internal {B : Basis} {family : CircuitFamily B} {bound : ℕ → ℕ} (hbound : family.SizeBoundedBy bound) : family.EventuallySizeBoundedBy bound

theorem Complexity.CircuitFamily.EventuallySizeBoundedBy.mono_internal {B : Basis} {family : CircuitFamily B} {first second : ℕ → ℕ} (hbound : family.EventuallySizeBoundedBy first) (hle : ∀ (n : ℕ), first n ≤ second n) : family.EventuallySizeBoundedBy second

theorem Complexity.CircuitFamily.EventuallySizeBoundedBy.trans_eventually_internal {B : Basis} {family : CircuitFamily B} {first second : ℕ → ℕ} (hbound : family.EventuallySizeBoundedBy first) (hle : ∀ᶠ (n : ℕ) in Filter.atTop, first n ≤ second n) : family.EventuallySizeBoundedBy second

theorem Complexity.CircuitFamily.EventuallySizeBoundedBy.polynomialSize_internal {B : Basis} {family : CircuitFamily B} {p : Polynomial ℕ} (hbound : family.EventuallySizeBoundedBy fun (n : ℕ) => Polynomial.eval n p) : family.PolynomialSize

theorem Complexity.PromiseSIZEWithBasis_subset_PromiseEventuallySIZEWithBasis_internal (B : Basis) (bound : ℕ → ℕ) : PromiseSIZEWithBasis B bound ⊆ PromiseEventuallySIZEWithBasis B bound

theorem Complexity.PromiseSIZE_subset_PromiseEventuallySIZE_internal (bound : ℕ → ℕ) : PromiseSIZE bound ⊆ PromiseEventuallySIZE bound

theorem Complexity.PromiseSIZEWithBasis_mono_internal (B : Basis) {first second : ℕ → ℕ} (hle : ∀ (n : ℕ), first n ≤ second n) : PromiseSIZEWithBasis B first ⊆ PromiseSIZEWithBasis B second

theorem Complexity.PromiseEventuallySIZEWithBasis_mono_internal (B : Basis) {first second : ℕ → ℕ} (hle : ∀ (n : ℕ), first n ≤ second n) : PromiseEventuallySIZEWithBasis B first ⊆ PromiseEventuallySIZEWithBasis B second

theorem Complexity.PromiseSIZEWithBasis_mapBasis_subset_internal {source target : Basis} (hom : source.Hom target) (bound : ℕ → ℕ) : PromiseSIZEWithBasis source bound ⊆ PromiseSIZEWithBasis target bound

theorem Complexity.PromiseEventuallySIZEWithBasis_mapBasis_subset_internal {source target : Basis} (hom : source.Hom target) (bound : ℕ → ℕ) : PromiseEventuallySIZEWithBasis source bound ⊆ PromiseEventuallySIZEWithBasis target bound

theorem Complexity.PromiseSIZEWithBasis_eq_of_homs_internal {first second : Basis} (forward : first.Hom second) (reverse : second.Hom first) (bound : ℕ → ℕ) : PromiseSIZEWithBasis first bound = PromiseSIZEWithBasis second bound

theorem Complexity.PromiseEventuallySIZEWithBasis_eq_of_homs_internal {first second : Basis} (forward : first.Hom second) (reverse : second.Hom first) (bound : ℕ → ℕ) : PromiseEventuallySIZEWithBasis first bound = PromiseEventuallySIZEWithBasis second bound

theorem Complexity.PromiseEventuallySIZE_polynomial_subset_PromisePPoly_internal (p : Polynomial ℕ) : (PromiseEventuallySIZE fun (n : ℕ) => Polynomial.eval n p) ⊆ PromisePPoly