Elementary theory of the Bernoulli distribution

This file computes the elementary moments and transforms of the real-valued Bernoulli 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;
• 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”.

@[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.