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 measure Ber(x, y, p) which gives mass p to {x} and 1 - p to {y}.

Notation

• Ber(x, y, p): notation for bernoulliMeasure x y p.

Tags

Bernoulli distribution

noncomputable def ProbabilityTheory.bernoulliMeasure {X : Type u_1} [MeasurableSpace X] (x y : X) (p : ↑unitInterval) : MeasureTheory.Measure X

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

• ProbabilityTheory.bernoulliMeasure x y p = unitInterval.toNNReal p • MeasureTheory.Measure.dirac x + unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac y

def ProbabilityTheory.«termBer(_,_,_)» : Lean.ParserDescr

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.

theorem ProbabilityTheory.bernoulliMeasure_def {X : Type u_1} [MeasurableSpace X] (x y : X) (p : ↑unitInterval) : bernoulliMeasure x y p = unitInterval.toNNReal p • MeasureTheory.Measure.dirac x + unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac y

@[simp]

theorem ProbabilityTheory.bernoulliMeasure_zero {X : Type u_1} [MeasurableSpace X] (x y : X) : bernoulliMeasure x y 0 = MeasureTheory.Measure.dirac y

@[simp]

theorem ProbabilityTheory.bernoulliMeasure_one {X : Type u_1} [MeasurableSpace X] (x y : X) : bernoulliMeasure x y 1 = MeasureTheory.Measure.dirac x

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) : (bernoulliMeasure x y p) s = 1

@[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) : (bernoulliMeasure x y p).real s = 1

@[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) : (bernoulliMeasure x y p) s = ↑(unitInterval.toNNReal p)

@[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) : (bernoulliMeasure x y p).real s = ↑p

@[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) : (bernoulliMeasure x y p) s = ↑(unitInterval.toNNReal (unitInterval.symm p))

@[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) : (bernoulliMeasure x y p).real s = 1 - ↑p

@[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) : (bernoulliMeasure x y p) s = 0

@[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) : (bernoulliMeasure x y p).real s = 0

instance ProbabilityTheory.instIsProbabilityMeasureBernoulliMeasure {X : Type u_1} [MeasurableSpace X] {x y : X} {p : ↑unitInterval} : MeasureTheory.IsProbabilityMeasure (bernoulliMeasure x y p)

@[simp]

theorem ProbabilityTheory.bernoulliMeasure_self_eq_dirac {X : Type u_1} [MeasurableSpace X] (x : X) (p : ↑unitInterval) : bernoulliMeasure x x p = MeasureTheory.Measure.dirac x

@[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) : MeasureTheory.Measure.map f (bernoulliMeasure x y p) = bernoulliMeasure (f x) (f y) p

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) : MeasureTheory.Measure.map f (bernoulliMeasure x y p) = bernoulliMeasure (f x) (f y) p

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) : ∫ (z : X), f z ∂bernoulliMeasure x y p = ↑p • f x + (1 - ↑p) • f y