FalsePointFraction

formal source

  41    This is the direct analog of landscape depth without going through CNF.
  42    For any CNF-encodable function, this equals the landscape depth of the
  43    canonical full-width encoding (one blocking clause per false-point). -/
  44def FalsePointFraction {n : ℕ} (f : (Fin n → Bool) → Bool) : ℝ :=
  45  (Finset.univ.filter (fun a : Fin n → Bool => !f a)).card /
  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