falsePointFraction_le_one

formal source

  52  exact div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)
  53
  54/-- False-point fraction is at most 1. -/
  55theorem falsePointFraction_le_one {n : ℕ} (f : (Fin n → Bool) → Bool) :
  56    FalsePointFraction f ≤ 1 := by
  57  unfold FalsePointFraction
  58  have hcard_pos : (0 : ℝ) < (Finset.univ.card (α := Fin n → Bool) : ℝ) := by
  59    exact_mod_cast Finset.card_pos.mpr ⟨fun _ => false, Finset.mem_univ _⟩
  60  rw [div_le_one hcard_pos]
  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 →