Independent Bernoulli trials, at the Finset level

Infrastructure for MiscMath.Probability.PoissonTrialsFixedMean, which is where the results are stated and where the reader should start. This file carries the model — bernWt, bernExp, tailLe — and the master pair identity every argument in the library rests on. PoissonTrialsFixedMean.Bridge identifies the model with a product of Mathlib ProbabilityTheory.bernoulliMeasures.

The model: independent Bernoulli trials, at the Finset level

The sample space is s.powerset — the possible sets of successful trials — the weight of a success set A is

bernWt s p A = (∏ i ∈ A, p i) * ∏ i ∈ s \ A, (1 - p i),

and the statistic is S = #A, so that bernExp s p g = E[g S]. Nothing is assumed about p in the definitions; the range hypotheses 0 ≤ p i ≤ 1 are carried by the theorems that need them, and where they are not needed this is said.

Everything here is stated for an arbitrary index type, an arbitrary ground set s : Finset ι and an arbitrary CommRing; the order and the range hypotheses enter only from Theorem 3 onwards. bernExp_eq_integral_pi_bernoulliMeasure, in PoissonTrialsFixedMean.Bridge, identifies this with a product of Mathlib bernoulliMeasures.

bernExp_pair_sub is the one computation of the development: every inequality in the two sections that follow is this identity with a sign supplied. It is proved by splitting the powerset on the two moved coordinates, which is Finset.sum_powerset_insert twice.

def MiscMath.Probability.bernWt {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (p : ι → 𝕜) (A : Finset ι) : 𝕜

The Bernoulli product weight of the success set A among the trials s: (∏ i ∈ A, p i) * ∏ i ∈ s \ A, (1 - p i). No hypothesis on p.

Equations

• MiscMath.Probability.bernWt s p A = (∏ i ∈ A, p i) * ∏ i ∈ s \ A, (1 - p i)

def MiscMath.Probability.bernExp {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (p : ι → 𝕜) (g : ℕ → 𝕜) : 𝕜

E[g S], where S = #A is the number of successes.

Equations

• MiscMath.Probability.bernExp s p g = ∑ A ∈ s.powerset, MiscMath.Probability.bernWt s p A * g A.card

def MiscMath.Probability.secondDiff {𝕜 : Type u_2} [CommRing 𝕜] (g : ℕ → 𝕜) (k : ℕ) : 𝕜

The second difference of g on the integer grid: g (k+2) - 2 g (k+1) + g k. Grid convexity is 0 ≤ secondDiff g k, strict grid convexity 0 < secondDiff g k.

Equations

• MiscMath.Probability.secondDiff g k = g (k + 2) - 2 * g (k + 1) + g k

@[simp]

theorem MiscMath.Probability.bernWt_empty {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (p : ι → 𝕜) (A : Finset ι) : bernWt ∅ p A = ∏ i ∈ A, p i

theorem MiscMath.Probability.sum_bernWt {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (p : ι → 𝕜) : ∑ A ∈ s.powerset, bernWt s p A = 1

The weights sum to 1. This is Finset.prod_add and nothing else — in particular it needs no hypothesis on p at all, which is what makes the necessity witnesses for Theorem 3 possible: outside [0,1] the weights are still a (signed) unit mass.

theorem MiscMath.Probability.bernWt_congr {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s A : Finset ι} {p q : ι → 𝕜} (hA : A ⊆ s) (h : ∀ i ∈ s, p i = q i) : bernWt s p A = bernWt s q A

bernWt s p A only reads p on s.

theorem MiscMath.Probability.bernExp_congr {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s : Finset ι} {p q : ι → 𝕜} (h : ∀ i ∈ s, p i = q i) (g : ℕ → 𝕜) : bernExp s p g = bernExp s q g

bernExp s p g only reads p on s.

theorem MiscMath.Probability.bernExp_neg {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (p : ι → 𝕜) (g : ℕ → 𝕜) : (bernExp s p fun (k : ℕ) => -g k) = -bernExp s p g

theorem MiscMath.Probability.bernExp_zero_fun {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (p : ι → 𝕜) : (bernExp s p fun (x : ℕ) => 0) = 0

theorem MiscMath.Probability.bernWt_insert_notMem {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s A : Finset ι} {i : ι} (hi : i ∉ s) (hA : A ⊆ s) (p : ι → 𝕜) : bernWt (insert i s) p A = (1 - p i) * bernWt s p A

theorem MiscMath.Probability.bernWt_insert_mem {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s A : Finset ι} {i : ι} (hi : i ∉ s) (hA : A ⊆ s) (p : ι → 𝕜) : bernWt (insert i s) p (insert i A) = p i * bernWt s p A

theorem MiscMath.Probability.sum_powerset_split_two {ι : Type u_1} [DecidableEq ι] {M : Type u_2} [AddCommMonoid M] {R : Finset ι} {i j : ι} (hj : j ∉ R) (hi : i ∉ insert j R) (F : Finset ι → M) : ∑ A ∈ (insert i (insert j R)).powerset, F A = ∑ B ∈ R.powerset, (F B + F (insert j B) + F (insert i B) + F (insert i (insert j B)))

Splitting a powerset sum on two distinct elements. Bookkeeping only: four applications of Finset.sum_powerset_insert.

theorem MiscMath.Probability.bernExp_pair_expand {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {R : Finset ι} {i j : ι} (hj : j ∉ R) (hi : i ∉ insert j R) (p : ι → 𝕜) (g : ℕ → 𝕜) : bernExp (insert i (insert j R)) p g = ∑ B ∈ R.powerset, bernWt R p B * ((1 - p i) * (1 - p j) * g B.card + ((1 - p i) * p j + p i * (1 - p j)) * g (B.card + 1) + p i * p j * g (B.card + 2))

The powerset sum split on the pair {i, j}: the inner bracket is the three-point expectation of g given the successes outside the pair.

theorem MiscMath.Probability.bernExp_pair_sub {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {R : Finset ι} {i j : ι} (hj : j ∉ R) (hi : i ∉ insert j R) (p q : ι → 𝕜) (g : ℕ → 𝕜) (hout : ∀ k ∈ R, q k = p k) (hsum : q i + q j = p i + p j) : bernExp (insert i (insert j R)) q g - bernExp (insert i (insert j R)) p g = (q i * q j - p i * p j) * ∑ B ∈ R.powerset, bernWt R p B * secondDiff g B.card

The master identity. Along any move of the pair (p i, p j) that preserves the sum, the expectation changes by the change in the product times a factor that never reads p i or p j. No sign hypothesis, no convexity, and no range hypothesis.

theorem MiscMath.Probability.exists_pair_decomp {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : ∃ (R : Finset ι), j ∉ R ∧ i ∉ insert j R ∧ insert i (insert j R) = s ∧ R.card + 2 = s.card

Peel two distinct elements off a ground set.

theorem MiscMath.Probability.pair_decomp {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : j ∉ s \ {i, j} ∧ i ∉ insert j (s \ {i, j}) ∧ insert i (insert j (s \ {i, j})) = s

s peeled at a distinct pair, with the explicit remainder s \ {i,j} — the form the pair-move argument for Corollary 2.1 needs.

The closed form at a constant vector: the model is the binomial

theorem MiscMath.Probability.bernWt_const {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s A : Finset ι} (hA : A ⊆ s) (P : 𝕜) : bernWt s (fun (x : ι) => P) A = P ^ A.card * (1 - P) ^ (s.card - A.card)

theorem MiscMath.Probability.bernExp_const {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (P : 𝕜) (g : ℕ → 𝕜) : bernExp s (fun (x : ι) => P) g = ∑ k ∈ Finset.range (s.card + 1), ↑(s.card.choose k) * P ^ k * (1 - P) ^ (s.card - k) * g k

At a constant vector the model is the binomial: the powerset sum collapses to ∑_{k ≤ #s} C(#s,k) P^k (1-P)^{#s-k} g k.

theorem MiscMath.Probability.bernExp_pair {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {a b : ι} (hab : a ≠ b) (p : ι → 𝕜) (g : ℕ → 𝕜) : bernExp {a, b} p g = (1 - p a) * (1 - p b) * g 0 + ((1 - p a) * p b + p a * (1 - p b)) * g 1 + p a * p b * g 2

Explicit expansion on a two-element ground set, for the numerical witnesses.

theorem MiscMath.Probability.bernExp_triple {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {a b c : ι} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (p : ι → 𝕜) (g : ℕ → 𝕜) : bernExp {a, b, c} p g = (1 - p c) * ((1 - p a) * (1 - p b) * g 0 + ((1 - p a) * p b + p a * (1 - p b)) * g 1 + p a * p b * g 2) + p c * ((1 - p a) * (1 - p b) * g 1 + ((1 - p a) * p b + p a * (1 - p b)) * g 2 + p a * p b * g 3)

Explicit expansion on a three-element ground set, for the numerical witnesses.

Conditioning on one trial, and the three-valued points

theorem MiscMath.Probability.bernExp_insert {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {t : Finset ι} {i : ι} (hi : i ∉ t) (q : ι → 𝕜) (g : ℕ → 𝕜) : bernExp (insert i t) q g = (1 - q i) * bernExp t q g + q i * bernExp t q fun (r : ℕ) => g (r + 1)

Conditioning on one trial: E[g S] = (1 - p i) E[g S'] + p i E[g (S'+1)], with S' the number of successes among the remaining trials.

theorem MiscMath.Probability.bernExp_drop_one {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s : Finset ι} {q : ι → 𝕜} {i : ι} (hi : i ∈ s) (hq : q i = 1) (g : ℕ → 𝕜) : bernExp s q g = bernExp (s.erase i) q fun (r : ℕ) => g (r + 1)

Peeling a coordinate pinned at 1: it always succeeds, so the count shifts.

theorem MiscMath.Probability.bernExp_drop_zero {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s : Finset ι} {q : ι → 𝕜} {i : ι} (hi : i ∈ s) (hq : q i = 0) (g : ℕ → 𝕜) : bernExp s q g = bernExp (s.erase i) q g

Peeling a coordinate pinned at 0: it never succeeds, so nothing changes.

theorem MiscMath.Probability.bernExp_drop_ones {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {q : ι → 𝕜} (O s : Finset ι) : O ⊆ s → (∀ i ∈ O, q i = 1) → ∀ (g : ℕ → 𝕜), bernExp s q g = bernExp (s \ O) q fun (r : ℕ) => g (r + O.card)

All the 1-coordinates peel off at once, shifting g by their number.

theorem MiscMath.Probability.bernExp_drop_zeros {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {q : ι → 𝕜} (Z s : Finset ι) : Z ⊆ s → (∀ i ∈ Z, q i = 0) → ∀ (g : ℕ → 𝕜), bernExp s q g = bernExp (s \ Z) q g

All the 0-coordinates peel off at once, changing nothing.

theorem MiscMath.Probability.bernExp_shape_eval {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s : Finset ι} {q : ι → 𝕜} {x : 𝕜} {O Z : Finset ι} (hOs : O ⊆ s) (hZs : Z ⊆ s \ O) (hO : ∀ i ∈ O, q i = 1) (hZ : ∀ i ∈ Z, q i = 0) (hI : ∀ i ∈ (s \ O) \ Z, q i = x) (g : ℕ → 𝕜) : bernExp s q g = ∑ j ∈ Finset.range (((s \ O) \ Z).card + 1), ↑(((s \ O) \ Z).card.choose j) * x ^ j * (1 - x) ^ (((s \ O) \ Z).card - j) * g (O.card + j)

The three-valued evaluation. At a point taking only the values 1 (on O), 0 (on Z) and one repeated x (elsewhere),

E[g S] = ∑_{j ≤ r} C(r,j) x^j (1-x)^{r-j} g (a + j), a = #O, r = #(s \ O \ Z).

This is S = a + Bin(r, x), and it is what makes the extremal shapes of Corollary 2.1 computable.

The lower tail

def MiscMath.Probability.tailLe {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (p : ι → 𝕜) (k : ℕ) : 𝕜

P[S ≤ k], the lower tail of the number of successes, as the expectation of an indicator.

Equations

• MiscMath.Probability.tailLe s p k = MiscMath.Probability.bernExp s p fun (r : ℕ) => if r ≤ k then 1 else 0

theorem MiscMath.Probability.tailLe_const {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (k : ℕ) (P : 𝕜) : tailLe s (fun (x : ι) => P) k = binTail s.card P k

The comparator is the model at the constant vector: P[S ≤ k] for #s identical trials at success probability P is binTail #s P k. Stated for an arbitrary ground set.

theorem MiscMath.Probability.tailLe_eq_one {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s : Finset ι} (p : ι → 𝕜) {k : ℕ} (hk : s.card ≤ k) : tailLe s p k = 1

In the degenerate range #s ≤ k the tail is 1: every success set is small enough. This is sum_bernWt, so it holds for every p whatsoever.

theorem MiscMath.Probability.tailLe_eq_zero_of_lt {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {s : Finset ι} {q : ι → 𝕜} {O : Finset ι} {k : ℕ} (hOs : O ⊆ s) (hO : ∀ i ∈ O, q i = 1) (hk : k < O.card) : tailLe s q k = 0

Below the ones the tail vanishes. If fewer than #O successes are allowed and O is pinned at 1, the event {S ≤ k} is impossible.

theorem MiscMath.Probability.tailLe_shape_eval {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {q : ι → ℝ} {x : ℝ} {O Z : Finset ι} {k : ℕ} (hOs : O ⊆ s) (hZs : Z ⊆ s \ O) (hO : ∀ i ∈ O, q i = 1) (hZ : ∀ i ∈ Z, q i = 0) (hI : ∀ i ∈ (s \ O) \ Z, q i = x) (hk : O.card ≤ k) : tailLe s q k = binTail ((s \ O) \ Z).card x (k - O.card)

The lower tail at a three-valued point is a shifted binomial tail.