def MonotoneProperty.IsMonotone {α : Type u_1} (ℱ : Finset α → Prop) : Prop

A property $\mathcal{F}$ of finite subsets is monotone (increasing) if it is closed under taking supersets: whenever $S \subseteq T$ and $\mathcal{F}(S)$ holds, so does $\mathcal{F}(T)$.

def MonotoneProperty.IsThreshold (probOfProperty : ℕ → ℝ → ℝ) (q : ℕ → ℝ) : Prop

Definition 4.3.1 (threshold function). A sequence $q(n)$ is a threshold for a monotone property with probability function $\mu_n(p)$ if $\mu_n(p_n) \to 0$ whenever $p_n / q_n \to 0$, and $\mu_n(p_n) \to 1$ whenever $p_n / q_n \to \infty$.

noncomputable def Threshold.randomSubsetProb (Ω : Type u_1) [Fintype Ω] [DecidableEq Ω] (𝓕 : Finset (Finset Ω)) (p : ℝ) : ℝ

The probability under the product Bernoulli$(p)$ distribution on $2^\Omega$ that the random subset is exactly one of the sets in $\mathcal{F}$, summing the weights $p^{|A|}(1-p)^{|\Omega| - |A|}$ over $A \in \mathcal{F}$.

def Threshold.IsSharpThreshold (μ : ℕ → ℝ → ℝ) (r : ℕ → ℝ) : Prop

A function $r(n)$ is a sharp threshold if for every $\delta > 0$, the probability $\mu_n(p_n) \to 0$ whenever eventually $p_n \le (1 - \delta) r_n$, and $\mu_n(p_n) \to 1$ whenever eventually $p_n \ge (1 + \delta) r_n$.

def Threshold.IsCoarseThreshold (μ : ℕ → ℝ → ℝ) (r : ℕ → ℝ) : Prop

A function $r(n)$ is a coarse threshold if there exist constants $0 < c < C$ and $\varepsilon > 0$ such that whenever $p_n / r_n \in [c, C]$ eventually, the property probability is eventually bounded into $[\varepsilon, 1 - \varepsilon]$.

theorem GraphMonotonicity.prodWeight_sum_eq_one (n : ℕ) (p : ℝ) : ∑ ω : Fin n → Bool, prodWeight n p ω = 1

The product Bernoulli$(p)$ weights on ${0,1}^n$ sum to $1$.

theorem GraphMonotonicity.probConst_add_compl (n : ℕ) (p : ℝ) (A : Set (Fin n → Bool)) : probConst n p A + probConst n p Aᶜ = 1

For the product Bernoulli$(p)$ measure on ${0,1}^n$, an event and its complement have measures summing to $1$.

theorem GraphMonotonicity.probConst_nonneg (n : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (A : Set (Fin n → Bool)) : 0 ≤ probConst n p A

The probability of any event under the product Bernoulli$(p)$ measure is nonnegative, provided $0 \le p \le 1$.

theorem GraphMonotonicity.probConst_compl_anti (n : ℕ) (A : Set (Fin n → Bool)) (hA : IsUpperSet A) (q p : ℝ) (hq0 : 0 ≤ q) (hqp : q ≤ p) (hp1 : p ≤ 1) : probConst n p Aᶜ ≤ probConst n q Aᶜ

For an upper (monotone increasing) set $A$, the probability of its complement under the product Bernoulli$(p)$ measure is antitone in $p$.

theorem GraphMonotonicity.union_copies_ineq (α β s : ℝ) (hα0 : 0 ≤ α) (hαβ : α ≤ β) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (m : ℕ) : 1 ≤ m → (1 - s ^ m) * α ^ m + s ^ m * β ^ m ≤ ((1 - s) * α + s * β) ^ m

An algebraic convexity-style inequality used in the union-of-copies argument: $(1 - s^m)\alpha^m + s^m \beta^m \le ((1-s)\alpha + s\beta)^m$ for $0 \le \alpha \le \beta$ and $s \in [0,1]$.

theorem GraphMonotonicity.bernoulli_complement (p : ℝ) (m : ℕ) (hm : 1 ≤ m) (hpm : p / ↑m ≤ 1) : 1 - p ≤ (1 - p / ↑m) ^ m

Bernoulli's inequality (complement form). For $m \ge 1$ and $p/m \le 1$, $1 - p \le (1 - p/m)^m$.

theorem GraphMonotonicity.probConst_compl_union_bound (n : ℕ) (A : Set (Fin n → Bool)) : IsUpperSet A → ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → ∀ (m : ℕ), 1 ≤ m → probConst n (1 - (1 - t) ^ m) Aᶜ ≤ probConst n t Aᶜ ^ m

Union of independent copies bound. For an upper set $A$ on $\{0,1\}^n$, the probability of $A^c$ under Bernoulli$(1 - (1-t)^m)$ is at most the $m$-th power of the probability of $A^c$ under Bernoulli$(t)$.

theorem GraphMonotonicity.multi_round_exposure (n : ℕ) (A : Set (Fin n → Bool)) (hA : IsUpperSet A) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (m : ℕ) (hm : 1 ≤ m) : probConst n p Aᶜ ≤ probConst n (p / ↑m) Aᶜ ^ m

Multi-round exposure inequality. For an upper set $A$, the probability that a single Bernoulli$(p)$ trial fails to land in $A$ is bounded by the $m$-th power of the failure probability for Bernoulli$(p/m)$.

theorem MonotoneProperty.one_sub_inv_pow_lt_half (m : ℕ) (hm : 1 ≤ m) : (1 - 1 / ↑m) ^ m < 1 / 2

The inequality $(1 - 1/m)^m < 1/2$ for $m \ge 1$, obtained from $(1 - 1/m)^m \le e^{-1} < 1/2$.

theorem MonotoneProperty.existence_of_threshold (μ : ℕ → ℝ → ℝ) (q : ℕ → ℝ) (h_mono : ∀ (n : ℕ) (p₁ p₂ : ℝ), 0 ≤ p₁ → p₁ ≤ p₂ → p₂ ≤ 1 → μ n p₁ ≤ μ n p₂) (h_ext_low : ∀ (n : ℕ), ∀ p ≤ 0, μ n p = 0) (h_ext_high : ∀ (n : ℕ) (p : ℝ), 1 ≤ p → μ n p = 1) (h_mre : ∀ (n : ℕ) (p : ℝ), 0 ≤ p → p ≤ 1 → ∀ (m : ℕ), 1 ≤ m → 1 - μ n p ≤ (1 - μ n (p / ↑m)) ^ m) (h_crit : ∀ (n : ℕ), μ n (q n) = 1 / 2) (hq_pos : ∀ (n : ℕ), 0 < q n) (hq_le : ∀ (n : ℕ), q n ≤ 1) (h_range : ∀ (n : ℕ) (p : ℝ), 0 ≤ μ n p ∧ μ n p ≤ 1) : IsThreshold μ q

Existence of a threshold (Theorem 4.3.5/4.3.6). Any monotone graph property $\mu_n$ satisfying the multi-round exposure inequality and reaching value $1/2$ at $q(n)$ has $q$ as a threshold function.

def MonotoneProperty.IsNontrivial (μ : ℕ → ℝ → ℝ) : Prop

A monotone property is nontrivial if $\mu_n(0) = 0$ and $\mu_n(1) = 1$ for all $n$.