falsePointFraction_nonneg

formal source

  46  (Finset.univ.card (α := Fin n → Bool) : ℝ)
  47
  48/-- False-point fraction is non-negative. -/
  49theorem falsePointFraction_nonneg {n : ℕ} (f : (Fin n → Bool) → Bool) :
  50    0 ≤ FalsePointFraction f := by
  51  unfold FalsePointFraction
  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