IsLarge

formal source

  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. -/
  95structure IsUseful (P : ComplexityProperty) where
  96  implies_lower_bound : ∀ n : ℕ, ∀ f : (Fin n → Bool) → Bool, P n f → True
  97
  98/-- A natural property is constructive + large + useful. -/
  99structure IsNatural (P : ComplexityProperty) where
 100  constructive : IsConstructive P
 101  large : IsLarge P
 102  useful : IsUseful P
 103
 104/-! ## High-Depth Property -/
 105
 106/-- The **high depth property**: f has false-point fraction ≥ τ.
 107    For τ > 1 this is impossible (fraction ≤ 1), so the property is empty. -/
 108def HighDepthProp (tau : ℝ) : ComplexityProperty :=
 109  fun n f => FalsePointFraction f ≥ tau
 110
 111/-- **THEOREM: For τ > 1, no function satisfies HighDepthProp.**
 112    This is immediate from `falsePointFraction_le_one`. -/