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

Product weight for the Bernoulli product measure on $\{0,1\}^n$: assigns to a configuration $\omega : \text{Fin } n \to \text{Bool}$ the weight $\prod_i p_i^{\omega_i} (1 - p_i)^{1 - \omega_i}$.

noncomputable def Harris.P (n : ℕ) (p : Fin n → ℝ) (S : Set (Fin n → Bool)) : ℝ

Probability of an event $S \subseteq \{0,1\}^n$ under the Bernoulli product measure with parameters $p$, defined as $\sum_\omega \text{prodWeight}(\omega) \cdot \mathbf{1}_S(\omega)$.

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

The total mass of $\text{prodWeight}$ is one: $\sum_\omega \text{prodWeight}(\omega) = 1$.

theorem Harris.prodWeight_nonneg {n : ℕ} {p : Fin n → ℝ} (hp : ∀ (i : Fin n), p i ∈ Set.Icc 0 1) (ω : Fin n → Bool) : 0 ≤ prodWeight n p ω

When each $p_i \in [0,1]$ the product weight is nonnegative.

theorem Harris.prodWeight_log_modular (n : ℕ) (p : Fin n → ℝ) (a b : Fin n → Bool) : prodWeight n p a * prodWeight n p b = prodWeight n p (a ⊓ b) * prodWeight n p (a ⊔ b)

Log-modularity (FKG condition) of the Bernoulli product weight: $\mu(a)\mu(b) = \mu(a \wedge b)\mu(a \vee b)$.

theorem Harris.indicator_upperSet_mono {n : ℕ} {A : Set (Fin n → Bool)} (hA : IsUpperSet A) : Monotone (A.indicator fun (x : Fin n → Bool) => 1)

The indicator function of an upper set (increasing event) is monotone.

theorem Harris.indicator_nonneg_fun (n : ℕ) (A : Set (Fin n → Bool)) : 0 ≤ A.indicator fun (x : Fin n → Bool) => 1

The indicator function of any set is pointwise nonnegative.

theorem Harris.indicator_inter_eq_mul {n : ℕ} (A B : Set (Fin n → Bool)) : ((A ∩ B).indicator fun (x : Fin n → Bool) => 1) = fun (ω : Fin n → Bool) => A.indicator (fun (x : Fin n → Bool) => 1) ω * B.indicator (fun (x : Fin n → Bool) => 1) ω

The indicator of an intersection equals the product of indicators: $\mathbf{1}_{A \cap B}(\omega) = \mathbf{1}_A(\omega) \cdot \mathbf{1}_B(\omega)$.

theorem Harris.harris_inequality {n : ℕ} {p : Fin n → ℝ} (hp : ∀ (i : Fin n), p i ∈ Set.Icc 0 1) {A B : Set (Fin n → Bool)} (hA : IsUpperSet A) (hB : IsUpperSet B) : P n p (A ∩ B) ≥ P n p A * P n p B

Theorem 7.1.1 (Harris 1960): For independent Boolean random variables with parameters $p_i \in [0,1]$ and increasing events $A, B \subseteq \{0,1\}^n$, $\mathbb{P}(A \cap B) \geq \mathbb{P}(A)\mathbb{P}(B)$.

theorem Harris.harris_inequality_multiple_increasing {n : ℕ} {p : Fin n → ℝ} (hp : ∀ (i : Fin n), p i ∈ Set.Icc 0 1) {k : ℕ} {A : Fin k → Set (Fin n → Bool)} (hA : ∀ (i : Fin k), IsUpperSet (A i)) : P n p (⋂ (i : Fin k), A i) ≥ ∏ i : Fin k, P n p (A i)

Corollary 7.1.6 (multiple-event Harris): For finitely many increasing events $A_1, \dots, A_k$, $\mathbb{P}\!\left(\bigcap_i A_i\right) \geq \prod_i \mathbb{P}(A_i)$.

def Harris.generalProdWeight (n : ℕ) (α : Type u_1) [LinearOrder α] [Fintype α] (p : Fin n → α → ℝ) (ω : Fin n → α) : ℝ

General product weight on $\alpha^n$ for a linearly ordered finite type $\alpha$: $\mu(\omega) = \prod_i p_i(\omega_i)$.

def Harris.generalE (n : ℕ) (α : Type u_1) [LinearOrder α] [Fintype α] (p : Fin n → α → ℝ) (f : (Fin n → α) → ℝ) : ℝ

General expectation operator: $\mathbb{E}[f] = \sum_\omega \mu(\omega) f(\omega)$ under the product weight on $\alpha^n$.

theorem Harris.generalProdWeight_sum_eq_one (n : ℕ) (α : Type u_1) [LinearOrder α] [Fintype α] (p : Fin n → α → ℝ) (hp : ∀ (i : Fin n), ∑ x : α, p i x = 1) : ∑ ω : Fin n → α, generalProdWeight n α p ω = 1

If each marginal $p_i$ sums to one, then $\sum_\omega \text{generalProdWeight}(\omega) = 1$.

theorem Harris.generalProdWeight_nonneg {n : ℕ} {α : Type u_1} [LinearOrder α] [Fintype α] {p : Fin n → α → ℝ} (hp : ∀ (i : Fin n) (x : α), 0 ≤ p i x) (ω : Fin n → α) : 0 ≤ generalProdWeight n α p ω

Nonnegativity of the general product weight when each marginal is nonnegative.

theorem Harris.generalProdWeight_log_modular (n : ℕ) (α : Type u_1) [LinearOrder α] [Fintype α] (p : Fin n → α → ℝ) (a b : Fin n → α) : generalProdWeight n α p a * generalProdWeight n α p b = generalProdWeight n α p (a ⊓ b) * generalProdWeight n α p (a ⊔ b)

Log-modularity of the general product weight on the lattice $\alpha^n$.

theorem Harris.harris_inequality_general {n : ℕ} {α : Type u_1} [LinearOrder α] [Fintype α] [Nonempty α] {p : Fin n → α → ℝ} (hp_nonneg : ∀ (i : Fin n) (x : α), 0 ≤ p i x) (hp_sum : ∀ (i : Fin n), ∑ x : α, p i x = 1) {f g : (Fin n → α) → ℝ} (hf : Monotone f) (hg : Monotone g) : (generalE n α p fun (ω : Fin n → α) => f ω * g ω) ≥ generalE n α p f * generalE n α p g

Theorem 7.1.5 (Harris, general form): For monotone increasing real-valued functions $f, g$ on $\alpha^n$ under a product probability measure, $\mathbb{E}[fg] \geq \mathbb{E}[f]\mathbb{E}[g]$.