Product of bernoulli distributions on a set

This file defines the product of bernoulli distributions on a set as a measure on sets. For a set u : Set ι and p between 0 and 1, this is the measure on Set ι such that each i ∈ u belongs to the random set with probability p, and each i ∉ u doesn't belong to it.

Notation

setBer(u, p) is the product of p-Bernoulli distributions on u.

TODO

It is painful to convert from unitInterval to ENNReal. Should we introduce a coercion or explicit operation (like unitInterval.toNNReal, note the lack of dot notation!)?

noncomputable def ProbabilityTheory.setBernoulli {ι : Type u_1} (u : Set ι) (p : ↑unitInterval) : MeasureTheory.Measure (Set ι)

The product of bernoulli distributions with parameter p on the set u : Set V is the measure on Set V such that each element of u is taken with probability p, and the elements outside of u are never taken.

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

The product of bernoulli distributions with parameter p on the set u : Set V is the measure on Set V such that each element of u is taken with probability p, and the elements outside of u are never taken.

instance ProbabilityTheory.instIsProbabilityMeasureSetSetBernoulli {ι : Type u_1} {u : Set ι} {p : ↑unitInterval} : MeasureTheory.IsProbabilityMeasure (setBernoulli u p)

theorem ProbabilityTheory.setBernoulli_eq_map {ι : Type u_1} (u : Set ι) (p : ↑unitInterval) : setBernoulli u p = MeasureTheory.Measure.map (fun (p : ι → Prop) => {i : ι | p i}) (MeasureTheory.Measure.infinitePi fun (i : ι) => unitInterval.toNNReal p • MeasureTheory.Measure.dirac (i ∈ u) + unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False)

theorem ProbabilityTheory.setBernoulli_apply {ι : Type u_1} {u : Set ι} {p : ↑unitInterval} (S : Set (Set ι)) : (setBernoulli u p) S = (MeasureTheory.Measure.infinitePi fun (i : ι) => unitInterval.toNNReal p • MeasureTheory.Measure.dirac (i ∈ u) + unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False) ((fun (t : Set ι) (i : ι) => i ∈ t) '' S)

theorem ProbabilityTheory.setBernoulli_apply' {ι : Type u_1} {u : Set ι} {p : ↑unitInterval} (S : Set (Set ι)) : (setBernoulli u p) S = (MeasureTheory.Measure.infinitePi fun (i : ι) => unitInterval.toNNReal p • MeasureTheory.Measure.dirac (i ∈ u) + unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False) ((fun (p : ι → Prop) => {i : ι | p i}) ⁻¹' S)

@[simp]

theorem ProbabilityTheory.setBernoulli_zero {ι : Type u_1} (u : Set ι) : setBernoulli u 0 = MeasureTheory.Measure.dirac ∅

@[simp]

theorem ProbabilityTheory.setBernoulli_one {ι : Type u_1} (u : Set ι) : setBernoulli u 1 = MeasureTheory.Measure.dirac u

theorem ProbabilityTheory.setBernoulli_ae_subset {ι : Type u_1} {u : Set ι} {p : ↑unitInterval} [Countable ι] : ∀ᵐ (s : Set ι) ∂setBernoulli u p, s ⊆ u

@[simp]

theorem ProbabilityTheory.setBernoulli_singleton {ι : Type u_1} {s : Set ι} (u : Set ι) (p : ↑unitInterval) [Countable ι] (hsu : s ⊆ u) (hu : u.Finite) : (setBernoulli u p) {s} = ↑(unitInterval.toNNReal p) ^ s.ncard * ↑(unitInterval.toNNReal (unitInterval.symm p)) ^ (u \ s).ncard

Bernoulli random variables

@[reducible, inline]

abbrev ProbabilityTheory.IsSetBernoulli {ι : Type u_1} {Ω : Type u_2} {m : MeasurableSpace Ω} (X : Ω → Set ι) (u : Set ι) (p : ↑unitInterval) (P : MeasureTheory.Measure Ω) : Prop

A random variable X : Ω → Set ι is p-bernoulli on a set u : Set ι if its distribution is the product over u of p-bernoulli distributions.

theorem ProbabilityTheory.isSetBernoulli_congr {ι : Type u_1} {Ω : Type u_2} {m : MeasurableSpace Ω} {X Y : Ω → Set ι} {u : Set ι} {p : ↑unitInterval} {P : MeasureTheory.Measure Ω} (hXY : X =ᵐ[P] Y) : IsSetBernoulli X u p P ↔ IsSetBernoulli Y u p P

theorem ProbabilityTheory.IsSetBernoulli.ae_subset {ι : Type u_1} {Ω : Type u_2} {m : MeasurableSpace Ω} {X : Ω → Set ι} {u : Set ι} {p : ↑unitInterval} {P : MeasureTheory.Measure Ω} [Countable ι] (hX : IsSetBernoulli X u p P) : ∀ᵐ (ω : Ω) ∂P, X ω ⊆ u