Bernoulli distribution #
We define the Bernoulli distribution over an arbitrary measurable space X. Given x y : X
and p : I (I is the unitInterval),
Ber(x, y, p) := toNNReal p • dirac x + toNNReal (σ p) • dirac y.
It is the measure which gives mass p to {x} and 1 - p to {y}.
Main definition #
bernoulliMeasure x y p: The measureBer(x, y, p)which gives masspto{x}and1 - pto{y}.
Notation #
Ber(x, y, p): notation forbernoulliMeasure x y p.
Tags #
Bernoulli distribution
noncomputable def
ProbabilityTheory.bernoulliMeasure
{X : Type u_1}
[MeasurableSpace X]
(x y : X)
(p : ↑unitInterval)
:
The Bernoulli distribution over an arbitrary measurable space X.
Given x y : X and p : I (I is the unitInterval),
it is the measure which gives mass p to {x} and 1 - p to {y}.
Equations
Instances For
The Bernoulli distribution over an arbitrary measurable space X.
Given x y : X and p : I (I is the unitInterval),
it is the measure which gives mass p to {x} and 1 - p to {y}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.bernoulliMeasure_def
{X : Type u_1}
[MeasurableSpace X]
(x y : X)
(p : ↑unitInterval)
:
@[simp]
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_apply
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
[DecidablePred fun (x : X) => x ∈ s]
:
(bernoulliMeasure x y p) s = if x ∈ s then if y ∈ s then 1 else ↑(unitInterval.toNNReal p)
else if y ∈ s then ↑(unitInterval.toNNReal (unitInterval.symm p)) else 0
theorem
ProbabilityTheory.bernoulliMeasure_real_apply
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
[DecidablePred fun (x : X) => x ∈ s]
:
(bernoulliMeasure x y p).real s = if x ∈ s then if y ∈ s then 1 else ↑(unitInterval.toNNReal p)
else if y ∈ s then ↑(unitInterval.toNNReal (unitInterval.symm p)) else 0
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_apply_of_mem_of_mem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∈ s)
(hy : y ∈ s)
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_real_apply_of_mem_of_mem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∈ s)
(hy : y ∈ s)
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_apply_of_mem_of_notMem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∈ s)
(hy : y ∉ s)
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_real_apply_of_mem_of_notMem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∈ s)
(hy : y ∉ s)
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_apply_of_notMem_of_mem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∉ s)
(hy : y ∈ s)
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_real_apply_of_notMem_of_mem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∉ s)
(hy : y ∈ s)
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_apply_of_notMem_of_notMem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∉ s)
(hy : y ∉ s)
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_real_apply_of_notMem_of_notMem
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
(p : ↑unitInterval)
{s : Set X}
(hs : MeasurableSet s)
(hx : x ∉ s)
(hy : y ∉ s)
:
instance
ProbabilityTheory.instIsProbabilityMeasureBernoulliMeasure
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
{p : ↑unitInterval}
:
@[simp]
theorem
ProbabilityTheory.bernoulliMeasure_self_eq_dirac
{X : Type u_1}
[MeasurableSpace X]
(x : X)
(p : ↑unitInterval)
:
@[simp]
theorem
ProbabilityTheory.map_bernoulliMeasure
{X : Type u_1}
{Y : Type u_2}
[MeasurableSpace X]
[MeasurableSpace Y]
[MeasurableSingletonClass X]
[MeasurableSingletonClass Y]
(x y : X)
(f : X → Y)
(p : ↑unitInterval)
:
theorem
ProbabilityTheory.map_bernoulliMeasure'
{X : Type u_1}
{Y : Type u_2}
[MeasurableSpace X]
[MeasurableSpace Y]
(x y : X)
{f : X → Y}
(hf : Measurable f)
(p : ↑unitInterval)
:
theorem
ProbabilityTheory.eq_bernoulliMeasure
{X : Type u_1}
[MeasurableSpace X]
{x y : X}
{p : ↑unitInterval}
{μ : MeasureTheory.Measure X}
(h1 : ∀ (s : Set X), MeasurableSet s → x ∈ s → y ∈ s → μ s = 1)
(h2 : ∀ (s : Set X), MeasurableSet s → x ∈ s → y ∉ s → μ s = ↑(unitInterval.toNNReal p))
(h3 : ∀ (s : Set X), MeasurableSet s → x ∉ s → y ∈ s → μ s = ↑(unitInterval.toNNReal (unitInterval.symm p)))
(h4 : ∀ (s : Set X), MeasurableSet s → x ∉ s → y ∉ s → μ s = 0)
:
theorem
ProbabilityTheory.integrable_bernoulliMeasure
{X : Type u_1}
[MeasurableSpace X]
{E : Type u_3}
[NormedAddCommGroup E]
[MeasurableSingletonClass X]
(x y : X)
(p : ↑unitInterval)
(f : X → E)
:
MeasureTheory.Integrable f (bernoulliMeasure x y p)
theorem
ProbabilityTheory.integral_bernoulliMeasure
{X : Type u_1}
[MeasurableSpace X]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
(x y : X)
(p : ↑unitInterval)
(f : X → E)
:
Bernoulli random variables #
theorem
ProbabilityTheory.hasLaw_indicator_bernoulliMeasure
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{M : Type u_4}
[Zero M]
[MeasurableSpace M]
(c : M)
{s : Set Ω}
(hs : MeasureTheory.NullMeasurableSet s P)
:
The constant indicator of a set follows a Bernoulli distribution.
theorem
ProbabilityTheory.hasLaw_indicator_one_bernoulliMeasure
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{M : Type u_4}
[Zero M]
[One M]
[MeasurableSpace M]
{s : Set Ω}
(hs : MeasureTheory.NullMeasurableSet s P)
:
The constant indicator of a set follows a Bernoulli distribution.