lemma
proved
linearFamily_length_bound
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.SAT.SmallBias on GitHub at line 67.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
64 omega
65
66/-- Linear family length bound O((n+1)²). -/
67lemma linearFamily_length_bound (n : Nat) :
68 (linearFamily n).length ≤ 2 * (n.succ ^ 2) := by
69 rw [linearFamily_length_eq]
70
71/-- Polynomial bound witness for the linear family. -/
72lemma linearFamily_poly_bound :
73 ∃ c k : Nat, ∀ n, (linearFamily n).length ≤ c * n.succ ^ k := by
74 refine ⟨2, 2, ?_⟩
75 intro n
76 exact linearFamily_length_bound n
77
78instance linearSmallBias_poly : HasPolySize linearSmallBias :=
79 ⟨linearFamily_poly_bound⟩
80
81end SAT
82end Complexity
83end IndisputableMonolith