Geometric distributions over ℕ

Define the geometric measure over the natural numbers

Main definitions

• geometricPMFReal: the function p n ↦ (1-p) ^ n * p for n ∈ ℕ, which is the probability density function of a geometric distribution with success probability p ∈ (0,1].
• geometricPMF: ℝ≥0∞-valued pmf, geometricPMF p = ENNReal.ofReal (geometricPMFReal p).
• geometricMeasure: a geometric measure on ℕ, parametrized by its success probability p.

noncomputable def ProbabilityTheory.geometricPMFReal (p : ℝ) (n : ℕ) : ℝ

The pmf of the geometric distribution depending on its success probability.

Equations

• ProbabilityTheory.geometricPMFReal p n = (1 - p) ^ n * p

theorem ProbabilityTheory.geometricPMFRealSum {p : ℝ} (hp_pos : 0 < p) (hp_le_one : p ≤ 1) : HasSum (fun (n : ℕ) => geometricPMFReal p n) 1

theorem ProbabilityTheory.geometricPMFReal_pos {p : ℝ} {n : ℕ} (hp_pos : 0 < p) (hp_lt_one : p < 1) : 0 < geometricPMFReal p n

The geometric pmf is positive for all natural numbers

theorem ProbabilityTheory.geometricPMFReal_nonneg {p : ℝ} {n : ℕ} (hp_pos : 0 < p) (hp_le_one : p ≤ 1) : 0 ≤ geometricPMFReal p n

noncomputable def ProbabilityTheory.geometricPMF {p : ℝ} (hp_pos : 0 < p) (hp_le_one : p ≤ 1) : PMF ℕ

Geometric distribution with success probability p.

Equations

• ProbabilityTheory.geometricPMF hp_pos hp_le_one = ⟨fun (n : ℕ) => ENNReal.ofReal (ProbabilityTheory.geometricPMFReal p n), ⋯⟩

theorem ProbabilityTheory.measurable_geometricPMFReal {p : ℝ} : Measurable (geometricPMFReal p)

The geometric pmf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_geometricPMFReal {p : ℝ} : MeasureTheory.StronglyMeasurable (geometricPMFReal p)

noncomputable def ProbabilityTheory.geometricMeasure {p : ℝ} (hp_pos : 0 < p) (hp_le_one : p ≤ 1) : MeasureTheory.Measure ℕ

Measure defined by the geometric distribution

Equations

• ProbabilityTheory.geometricMeasure hp_pos hp_le_one = (ProbabilityTheory.geometricPMF hp_pos hp_le_one).toMeasure

theorem ProbabilityTheory.isProbabilityMeasureGeometric {p : ℝ} (hp_pos : 0 < p) (hp_le_one : p ≤ 1) : MeasureTheory.IsProbabilityMeasure (geometricMeasure hp_pos hp_le_one)