Geometric distributions

We define the geometric distributions over natural numbers. For 0 < p ≤ 1, geometricMeasure p is the measure which to {n} associates (1 - p) ^ n * n.

As the parameter p needs to lie between 0 and 1, we define geometricMeasure p with p : unitInterval.

Imagine a certain experience which has success probability p. If you repeat this experience infintely many times and independently, the number of failures before the first success follows a geometric distribution with parameter p.

Main definition

• geometricMeasure p: a geometric measure on a semiring R, parametrized by its success probability p.

Implementation note

To avoid having to carry around a hypothesis p ≠ 0, we define geometricMeasure 0 := Measure.dirac 0. That way IsProbabilityMeasure (geometricMeasure p) can be automatically inferred.

Tags

geometric distribution

noncomputable def ProbabilityTheory.geometricMeasure (p : ↑unitInterval) : MeasureTheory.Measure ℕ

The geometric measure with success probability p as a measure over ℕ.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.geometricMeasure_eq {p : ↑unitInterval} (hp : p ≠ 0) : geometricMeasure p = MeasureTheory.Measure.sum fun (n : ℕ) => ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • MeasureTheory.Measure.dirac n

theorem ProbabilityTheory.geometricMeasure_nonneg (p : ↑unitInterval) (n : ℕ) : 0 ≤ (1 - ↑p) ^ n * ↑p

The positivty tactic does not work for this goal. Use this lemma to rewrite (ENNReal.ofReal ((1 - p) ^ n * p)).toReal = (1 - p) ^ n * p.

theorem ProbabilityTheory.geometricMeasure_pos {p : ↑unitInterval} (h1 : p ≠ 0) (h2 : p ≠ 1) (n : ℕ) : 0 < (1 - ↑p) ^ n * ↑p

theorem ProbabilityTheory.geometricMeasure_singleton {p : ↑unitInterval} (hp : p ≠ 0) (n : ℕ) : (geometricMeasure p) {n} = ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)

theorem ProbabilityTheory.geometricMeasure_real_singleton {p : ↑unitInterval} (hp : p ≠ 0) (n : ℕ) : (geometricMeasure p).real {n} = (1 - ↑p) ^ n * ↑p

theorem ProbabilityTheory.geometricMeasure_real_singleton_pos {p : ↑unitInterval} (h1 : p ≠ 0) (h2 : p ≠ 1) (n : ℕ) : 0 < (geometricMeasure p).real {n}

theorem ProbabilityTheory.hasSum_one_geometricMeasure {p : ↑unitInterval} (hp : p ≠ 0) : HasSum (fun (n : ℕ) => (1 - ↑p) ^ n * ↑p) 1

instance ProbabilityTheory.isProbabilityMeasure_geometricMeasure {p : ↑unitInterval} : MeasureTheory.IsProbabilityMeasure (geometricMeasure p)

theorem ProbabilityTheory.integrable_geometricMeasure_iff {p : ↑unitInterval} {E : Type u_1} [NormedAddCommGroup E] {f : ℕ → E} (hp : p ≠ 0) : MeasureTheory.Integrable f (geometricMeasure p) ↔ Summable fun (n : ℕ) => (1 - ↑p) ^ n * ↑p * ‖f n‖

theorem ProbabilityTheory.hasSum_integral_geometricMeasure {p : ↑unitInterval} {E : Type u_1} [NormedAddCommGroup E] {f : ℕ → E} [NormedSpace ℝ E] [CompleteSpace E] (hp : p ≠ 0) (hf : MeasureTheory.Integrable f (geometricMeasure p)) : HasSum (fun (n : ℕ) => ((1 - ↑p) ^ n * ↑p) • f n) (∫ (n : ℕ), f n ∂geometricMeasure p)

theorem ProbabilityTheory.integral_geometricMeasure' {p : ↑unitInterval} {E : Type u_1} [NormedAddCommGroup E] {f : ℕ → E} [NormedSpace ℝ E] [CompleteSpace E] (hp : p ≠ 0) (hf : MeasureTheory.Integrable f (geometricMeasure p)) : ∫ (n : ℕ), f n ∂geometricMeasure p = ∑' (n : ℕ), ((1 - ↑p) ^ n * ↑p) • f n

If a function is integrable with respect to geometricMeasure p, then its integral against this measure is given by its sum weighted by (1 - p) ^ n * p.

See integral_geometricMeasure for a version where the codomain is finite-dimensional and does not require the integrability hypothesis.

theorem ProbabilityTheory.integral_geometricMeasure {p : ↑unitInterval} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (hp : p ≠ 0) (f : ℕ → E) : ∫ (n : ℕ), f n ∂geometricMeasure p = ∑' (n : ℕ), ((1 - ↑p) ^ n * ↑p) • f n

The integral of a function taking values in a finite-dimensional space against geometricMeasure p is given by its sum weighted by (1 - p) ^ n * p. This version does not require integrability, as the integral exists if and only if the sum exists, and otherwise they are both defined to be zero.

See integral_geometricMeasure' with a general codomain which assumes integrability.

@[deprecated ProbabilityTheory.geometricMeasure (since := "2026-03-08")]

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

@[deprecated ProbabilityTheory.hasSum_one_geometricMeasure (since := "2026-03-08")]

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

@[deprecated ProbabilityTheory.geometricMeasure_real_singleton_pos (since := "2026-03-08")]

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

@[deprecated MeasureTheory.measureReal_nonneg (since := "2026-03-08")]

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

@[deprecated ProbabilityTheory.geometricMeasure (since := "2026-03-08")]

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), ⋯⟩

@[deprecated Measurable.of_discrete (since := "2026-03-08")]

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

@[deprecated MeasureTheory.StronglyMeasurable.of_discrete (since := "2026-03-08")]

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