const_true_zero_fraction

formal source

  61  exact_mod_cast Finset.card_filter_le _ _
  62
  63/-- The constant-true function has zero false-point fraction. -/
  64theorem const_true_zero_fraction (n : ℕ) :
  65    FalsePointFraction (fun _ : Fin n → Bool => true) = 0 := by
  66  unfold FalsePointFraction
  67  simp
  68
  69/-- The constant-false function has false-point fraction 1. -/
  70theorem const_false_full_fraction (n : ℕ) :
  71    FalsePointFraction (fun _ : Fin n → Bool => false) = 1 := by
  72  unfold FalsePointFraction
  73  simp
  74
  75/-! ## Razborov-Rudich Framework -/
  76
  77/-- A complexity property maps each arity n and truth table to a proposition. -/
  78def ComplexityProperty := ∀ n : ℕ, ((Fin n → Bool) → Bool) → Prop
  79
  80/-- A property is **large** if the fraction of n-ary truth tables satisfying it
  81    is at least 1/n^k for some fixed k. -/
  82structure IsLarge (P : ComplexityProperty) where
  83  k : ℕ
  84  dec : ∀ n : ℕ, ∀ f : (Fin n → Bool) → Bool, Decidable (P n f)
  85  count_bound : ∀ n : ℕ, 0 < n →
  86    (Finset.univ.filter (fun f : (Fin n → Bool) → Bool =>
  87      @decide (P n f) (dec n f))).card * n ^ k ≥
  88    Finset.univ.card (α := (Fin n → Bool) → Bool)
  89
  90/-- A property is constructive if decidable. -/
  91structure IsConstructive (P : ComplexityProperty) where
  92  dec : ∀ n : ℕ, ∀ f : (Fin n → Bool) → Bool, Decidable (P n f)
  93
  94/-- A property is useful if it implies hardness. -/