The model and the comparator, in Mathlib's vocabulary

Part of MiscMath.Probability.PoissonTrialsFixedMean, whose module docstring states the results and where the reader should start. This file ties the four definitions local to this library — bernWt, bernExp, tailLe, binTail — back to Mathlib's ProbabilityTheory.binomial and ProbabilityTheory.bernoulliMeasure, so that the results are not comparisons of one bespoke object against another.

Relation to Mathlib's vocabulary

Four definitions are local to this library — bernWt, bernExp and tailLe from PoissonTrialsFixedMean.Model, binTail from PoissonTrialsFixedMean.BinomialTail — and the theorems are inequalities between them. This module ties all four back to Mathlib, so that the results are not comparisons of one bespoke object against another.

• bernExp_const_eq_integral_binomial and binTail_eq_binomial_real_Iic identify the comparator — the right-hand side of Theorem 3 and one side of Theorem 4 — with Mathlib's ProbabilityTheory.binomial, as an integral and as a measure of Set.Iic k respectively.
• bernExp_eq_integral_pi_bernoulliMeasure identifies the model with the integral of g ∘ (number of successes) against MeasureTheory.Measure.pi of Mathlib's ProbabilityTheory.bernoulliMeasure — an honest product of independent, individually parameterised Bernoulli measures on Bool. This is the statement that says bernWt means what its docstring says it means.

theorem MiscMath.Probability.bernExp_const_eq_integral_binomial {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (P : ↑unitInterval) (g : ℕ → ℝ) : bernExp s (fun (x : ι) => ↑P) g = ∫ (x : ℕ), g x ∂ProbabilityTheory.binomial s.card P

The comparator is Mathlib's binomial distribution. At a constant success probability P the model is the integral against Bin(#s, P).

theorem MiscMath.Probability.binTail_eq_binomial_real_Iic (n k : ℕ) (P : ↑unitInterval) : binTail n (↑P) k = (ProbabilityTheory.binomial n P).real (Set.Iic k)

The binomial tail is the measure of Set.Iic k under Mathlib's binomial distribution.

theorem MiscMath.Probability.bernExp_eq_integral_pi_bernoulliMeasure {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {p : ι → ℝ} (h0 : ∀ i ∈ s, 0 ≤ p i) (h1 : ∀ i ∈ s, p i ≤ 1) (g : ℕ → ℝ) : bernExp s p g = ∫ (ω : ↥s → Bool), g {z : ↥s | ω z = true}.card ∂MeasureTheory.Measure.pi fun (z : ↥s) => ProbabilityTheory.bernoulliMeasure true false ⟨p ↑z, ⋯⟩

The model is a product of Mathlib Bernoulli measures. With one Bool-valued trial per element of s, the i-th succeeding with probability p i, bernExp s p g is the expectation of g applied to the number of successes.

The trials are indexed by {x // x ∈ s} and the product is MeasureTheory.Measure.pi, so independence is Mathlib's, not a convention of this file; each factor is ProbabilityTheory.bernoulliMeasure true false ⟨p i, _⟩, Mathlib's Bernoulli measure with its own parameter.