BranchingProcess.Field

def BranchingProcess.coord {ι : Type u_1} {α : Type u_2} (i : ι) :

(ι → α) → α

The i-th coordinate of a field of labels indexed by ι.

Equations

BranchingProcess.coord i ω = ω i

Instances For

noncomputable def BranchingProcess.fieldMeasure {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] :

MeasureTheory.Measure (ι → α)

The i.i.d. field measure: the infinite product on ι → α of copies of μ, one for each index. No countability hypothesis on ι is needed.

Equations

BranchingProcess.fieldMeasure μ = MeasureTheory.Measure.infinitePi fun (x : ι) => μ

Instances For

source

instance BranchingProcess.isProbabilityMeasure_fieldMeasure {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] :

MeasureTheory.IsProbabilityMeasure (fieldMeasure μ)

source

theorem BranchingProcess.measurable_coord {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (i : ι) :

Measurable (coord i)

Every coordinate is measurable.

source

theorem BranchingProcess.coord_iIndepFun {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] :

ProbabilityTheory.iIndepFun (fun (i : ι) => coord i) (fieldMeasure μ)

Independence of the field. Under the product measure the coordinates form an independent family.

source

theorem BranchingProcess.map_coord {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (i : ι) :

MeasureTheory.Measure.map (coord i) (fieldMeasure μ) = μ

The one-coordinate law. The pushforward of the field measure under a coordinate is μ; the coordinates are identically distributed.

source

theorem BranchingProcess.coord_law {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (i : ι) {s : Set α} (hs : MeasurableSet s) :

(fieldMeasure μ) (coord i ⁻¹' s) = μ s

The set form of the one-coordinate law.

source

noncomputable def BranchingProcess.bernoulliLaw {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) :

MeasureTheory.Measure Bool

The Bernoulli law on Bool with success probability t: mass t at true and 1 - t at false.

Equations

BranchingProcess.bernoulliLaw ht ht1 = ProbabilityTheory.bernoulliMeasure true false ⟨t, ⋯⟩

Instances For

source

instance BranchingProcess.isProbabilityMeasure_bernoulliLaw {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) :

MeasureTheory.IsProbabilityMeasure (bernoulliLaw ht ht1)

source

theorem BranchingProcess.bernoulliLaw_apply_true {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) :

(bernoulliLaw ht ht1) {true } = ENNReal.ofReal t

The Bernoulli law gives mass t to {true}.

source

noncomputable def BranchingProcess.bernoulliField {ι : Type u_1} {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) :

MeasureTheory.Measure (ι → Bool)

The Bernoulli field: the i.i.d. field on ι → Bool whose coordinates are Bernoulli with success probability t.

Equations

BranchingProcess.bernoulliField ht ht1 = BranchingProcess.fieldMeasure (BranchingProcess.bernoulliLaw ht ht1)

Instances For

source

instance BranchingProcess.isProbabilityMeasure_bernoulliField {ι : Type u_1} {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) :

MeasureTheory.IsProbabilityMeasure (bernoulliField ht ht1)

source

theorem BranchingProcess.measurable_bernoulliField_coord {ι : Type u_1} (i : ι) :

Measurable (coord i)

Every coordinate of the Bernoulli field is measurable.

source

theorem BranchingProcess.bernoulliField_iIndepFun {ι : Type u_1} {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) :

ProbabilityTheory.iIndepFun (fun (i : ι) => coord i) (bernoulliField ht ht1)

The coordinates of the Bernoulli field are independent.

source

theorem BranchingProcess.bernoulliField_apply_true {ι : Type u_1} {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) (i : ι) :

(bernoulliField ht ht1) {ω : ι → Bool | ω i = true } = ENNReal.ofReal t

Each coordinate of the Bernoulli field is open with probability t.

source

theorem BranchingProcess.exists_bernoulli_field (ι : Type u) {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) :

∃ (Ω : Type u) (x : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (_ : MeasureTheory.IsProbabilityMeasure P) (X : ι → Ω → Bool), (∀ (i : ι), Measurable (X i)) ∧ ProbabilityTheory.iIndepFun X P ∧ ∀ (i : ι), P {ω : Ω | X i ω = true } = ENNReal.ofReal t

The Bernoulli field exists in the packaged shape. For 0 ≤ t ≤ 1 and an arbitrary index type ι there is a probability space carrying a measurable, independent family of Bool-valued coordinates, each open with probability t. The space is ι → Bool under bernoulliField, so it lives in the universe of ι.