pith. machine review for the scientific record. sign in
lemma

linearFamily_poly_bound

proved
show as:
view math explainer →
module
IndisputableMonolith.Complexity.SAT.SmallBias
domain
Complexity
line
72 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.SmallBias on GitHub at line 72.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.