def GraphMonotonicity.prodWeight (n : ℕ) (p : ℝ) (ω : Fin n → Bool) : ℝ

Product Bernoulli weight of a configuration $\omega \in \{0,1\}^n$ under parameter $p$: $\prod_i p^{\omega_i} (1-p)^{1 - \omega_i}$.

noncomputable def GraphMonotonicity.probConst (n : ℕ) (p : ℝ) (A : Set (Fin n → Bool)) : ℝ

Probability of an event $A \subseteq \{0,1\}^n$ under the product Bernoulli $\mathrm{Ber}(p)^n$ measure: $\sum_{\omega \in A} \prod_i p^{\omega_i} (1-p)^{1 - \omega_i}$.

theorem GraphMonotonicity.sum_fin_succ_split (n : ℕ) (f : (Fin (n + 1) → Bool) → ℝ) : ∑ ω : Fin (n + 1) → Bool, f ω = ∑ ω : Fin n → Bool, f (Fin.cons true ω) + ∑ ω : Fin n → Bool, f (Fin.cons false ω)

Splits a sum over $\{0,1\}^{n+1}$ by conditioning on the first coordinate.

theorem GraphMonotonicity.prodWeight_cons (n : ℕ) (p : ℝ) (b : Bool) (ω : Fin n → Bool) : prodWeight (n + 1) p (Fin.cons b ω) = (bif b then p else 1 - p) * prodWeight n p ω

Factorization of the product weight after prepending a coordinate $b$.

theorem GraphMonotonicity.probConst_succ (n : ℕ) (p : ℝ) (A : Set (Fin (n + 1) → Bool)) : probConst (n + 1) p A = p * probConst n p {ω : Fin n → Bool | Fin.cons true ω ∈ A} + (1 - p) * probConst n p {ω : Fin n → Bool | Fin.cons false ω ∈ A}

Tower property of the product Bernoulli measure: conditioning on the first coordinate yields a convex combination of the conditional probabilities.

theorem GraphMonotonicity.condSet_isUpperSet (n : ℕ) (b : Bool) (A : Set (Fin (n + 1) → Bool)) (hA : IsUpperSet A) : IsUpperSet {ω : Fin n → Bool | Fin.cons b ω ∈ A}

The conditional event $\{\omega : (b, \omega) \in A\}$ inherits the upper-set (monotone) property from $A$.

theorem GraphMonotonicity.prodWeight_nonneg (n : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ω : Fin n → Bool) : 0 ≤ prodWeight n p ω

For $p \in [0, 1]$, the product weight is nonnegative.

theorem GraphMonotonicity.prodWeight_pos (n : ℕ) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (ω : Fin n → Bool) : 0 < prodWeight n p ω

For $p \in (0, 1)$, the product weight is strictly positive.

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

Monotonicity of probConst in the event: $A \subseteq B$ implies $\Pr_p[A] \le \Pr_p[B]$.

theorem GraphMonotonicity.probConst_strict_mono_set (n : ℕ) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (A B : Set (Fin n → Bool)) (hAB : A ⊆ B) (hne : ∃ ω ∈ B, ω ∉ A) : probConst n p A < probConst n p B

Strict monotonicity of probConst in the event: for $p \in (0, 1)$, if $A \subsetneq B$ then $\Pr_p[A] < \Pr_p[B]$.

theorem GraphMonotonicity.probConst_mono (n : ℕ) (A : Set (Fin n → Bool)) : IsUpperSet A → ∀ (p₁ p₂ : ℝ), 0 ≤ p₁ → p₁ ≤ p₂ → p₂ ≤ 1 → probConst n p₁ A ≤ probConst n p₂ A

Monotonicity of satisfying probability (Theorem 4.3.5): for any monotone (upper-set) event $A$ in $\{0,1\}^n$, the probability $\Pr_p[A]$ is nondecreasing in $p \in [0, 1]$.

theorem GraphMonotonicity.probConst_lower_bound {n : ℕ} {p : ℝ} (A : Set (Fin n → Bool)) (htop : (fun (x : Fin n) => true) ∈ A) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : p ^ n ≤ probConst n p A

If the all-true configuration lies in $A$, then $\Pr_p[A] \ge p^n$.

theorem GraphMonotonicity.probConst_at_zero {n : ℕ} (A : Set (Fin n → Bool)) (hbot : (fun (x : Fin n) => false) ∉ A) : probConst n 0 A = 0

At $p = 0$, $\Pr_0[A] = 0$ whenever the all-false configuration is not in $A$ (because the entire mass concentrates there).

theorem GraphMonotonicity.probConst_strictMono (n : ℕ) : 0 < n → ∀ (A : Set (Fin n → Bool)), IsUpperSet A → (fun (x : Fin n) => false) ∉ A → (fun (x : Fin n) => true) ∈ A → ∀ (p₁ p₂ : ℝ), 0 ≤ p₁ → p₁ < p₂ → p₂ ≤ 1 → probConst n p₁ A < probConst n p₂ A

Strict monotonicity of satisfying probability (Theorem 4.3.5, strict version): for any nontrivial monotone event $A$ in $\{0,1\}^n$ (containing the all-true configuration but not the all-false one), $p \mapsto \Pr_p[A]$ is strictly increasing on $[0, 1]$.