Elementary theory of the Bernoulli distribution

This file computes the elementary moments and transforms of the real-valued Bernoulli law Ber((1 : ℝ), 0, p), together with the probability-generating function of the native ℕ-valued law Ber((1 : ℕ), 0, p). It uses Mathlib's convention that the value 1 has mass p and the value 0 has mass 1 - p.

Main results

• integral_id_bernoulliMeasure and variance_id_bernoulliMeasure give the mean and variance;
• integral_of_hasLaw_bernoulliMeasure and variance_of_hasLaw_bernoulliMeasure give the corresponding random-variable statements;
• hasLaw_natCast_bernoulliMeasure and hasLaw_cast_eval_bernoulliMeasure relate native Bernoulli variables to their real casts;
• pgf_bernoulliMeasure computes the probability-generating function on the native carrier;
• mgf_id_bernoulliMeasure and cgf_id_bernoulliMeasure compute the moment- and cumulant-generating functions;
• charFun_bernoulliMeasure computes the characteristic function.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 1, “Bernoulli and binomial”.

theorem TauCeti.Probability.bernoulliMeasure_singleton_zero_lt_one {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Zero α] {a : α} {p : ↑unitInterval} (ha : a ≠ 0) (hp : 0 < ↑p) : (ProbabilityTheory.bernoulliMeasure a 0 p) {0} < 1

A Bernoulli law with a nonzero success value and positive success probability has mass strictly less than one at zero.

@[simp]

theorem TauCeti.Probability.pgf_bernoulliMeasure (p : ↑unitInterval) (t : ℝ) : pgf id (ProbabilityTheory.bernoulliMeasure 1 0 p) t = 1 - ↑p + ↑p * t

The probability-generating function of a Bernoulli distribution.

theorem TauCeti.Probability.hasLaw_natCast_bernoulliMeasure (p : ↑unitInterval) : ProbabilityTheory.HasLaw Nat.cast (ProbabilityTheory.bernoulliMeasure 1 0 p) (ProbabilityTheory.bernoulliMeasure 1 0 p)

The real cast of a native Bernoulli variable has the corresponding real Bernoulli law.

theorem TauCeti.Probability.hasLaw_cast_eval_bernoulliMeasure {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (i : ι) : ProbabilityTheory.HasLaw (fun (x : ι → ℕ) => ↑(x i)) (ProbabilityTheory.bernoulliMeasure 1 0 (p i)) (MeasureTheory.Measure.pi fun (i : ι) => ProbabilityTheory.bernoulliMeasure 1 0 (p i))

A real-cast coordinate under a product of native Bernoulli laws has the corresponding real Bernoulli law.

@[simp]

theorem TauCeti.Probability.integral_id_bernoulliMeasure (p : ↑unitInterval) : ∫ (x : ℝ), x ∂ProbabilityTheory.bernoulliMeasure 1 0 p = ↑p

The mean of the real-valued Bernoulli law with success probability p is p.

@[simp]

theorem TauCeti.Probability.variance_id_bernoulliMeasure (p : ↑unitInterval) : ProbabilityTheory.variance id (ProbabilityTheory.bernoulliMeasure 1 0 p) = ↑p * (1 - ↑p)

The variance of the real-valued Bernoulli law with success probability p is p(1-p).

theorem TauCeti.Probability.integral_of_hasLaw_bernoulliMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {p : ↑unitInterval} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.bernoulliMeasure 1 0 p) P) : ∫ (x : Ω), X x ∂P = ↑p

A real-valued Bernoulli random variable with success probability p has mean p.

theorem TauCeti.Probability.variance_of_hasLaw_bernoulliMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {p : ↑unitInterval} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.bernoulliMeasure 1 0 p) P) : ProbabilityTheory.variance X P = ↑p * (1 - ↑p)

A real-valued Bernoulli random variable with success probability p has variance p(1-p).

@[simp]

theorem TauCeti.Probability.mgf_id_bernoulliMeasure (p : ↑unitInterval) (t : ℝ) : ProbabilityTheory.mgf id (ProbabilityTheory.bernoulliMeasure 1 0 p) t = 1 - ↑p + ↑p * Real.exp t

The moment-generating function of the real-valued Bernoulli law.

theorem TauCeti.Probability.mgf_id_bernoulliMeasure_pos (p : ↑unitInterval) (t : ℝ) : 0 < ProbabilityTheory.mgf id (ProbabilityTheory.bernoulliMeasure 1 0 p) t

The moment-generating function of a real-valued Bernoulli law is strictly positive.

@[simp]

theorem TauCeti.Probability.cgf_id_bernoulliMeasure (p : ↑unitInterval) (t : ℝ) : ProbabilityTheory.cgf id (ProbabilityTheory.bernoulliMeasure 1 0 p) t = Real.log (1 - ↑p + ↑p * Real.exp t)

The cumulant-generating function of the real-valued Bernoulli law.

@[simp]

theorem TauCeti.Probability.charFun_bernoulliMeasure (p : ↑unitInterval) (t : ℝ) : MeasureTheory.charFun (ProbabilityTheory.bernoulliMeasure 1 0 p) t = 1 - ↑↑p + ↑↑p * Complex.exp (Complex.I * ↑t)

The characteristic function of the real-valued Bernoulli law.