First-success masses for product sequences

The event of r failures followed by a success in a prescribed set is a finite box. Summing its masses gives the normalized restriction to the success set.

def BGW.StableTrees.DiscreteForest.firstSuccess {Ω : Type u_1} (Q A : Set Ω) (r : ℕ) : Set (ℕ → Ω)

The first visit to Q is at r, and the visited point also belongs to A.

Equations

• BGW.StableTrees.DiscreteForest.firstSuccess Q A r = {ω : ℕ → Ω | ω r ∈ Q ∩ A ∧ ∀ i < r, ω i ∉ Q}

theorem BGW.StableTrees.DiscreteForest.measurableSet_firstSuccess {Ω : Type u_1} [MeasurableSpace Ω] {Q A : Set Ω} (hQ : MeasurableSet Q) (hA : MeasurableSet A) (r : ℕ) : MeasurableSet (firstSuccess Q A r)

First-success events are measurable.

theorem BGW.StableTrees.DiscreteForest.infinitePi_firstSuccess_atom {Ω : Type u_1} [MeasurableSpace Ω] (ρ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure ρ] {Q A : Set Ω} (hQ : MeasurableSet Q) (hA : MeasurableSet A) (r : ℕ) : (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ρ) (firstSuccess Q A r) = ρ Qᶜ ^ r * ρ (Q ∩ A)

A first-success event has the expected finite product mass.

theorem BGW.StableTrees.DiscreteForest.infinitePi_firstSuccess_mass {Ω : Type u_1} [MeasurableSpace Ω] (ρ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure ρ] {Q A : Set Ω} (hQ : MeasurableSet Q) (hA : MeasurableSet A) : (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ρ) (⋃ (r : ℕ), firstSuccess Q A r) = (ρ Q)⁻¹ * ρ (Q ∩ A)

Summing first-success masses gives the conditional mass in the success set.

theorem BGW.StableTrees.DiscreteForest.infinitePi_ae_exists_success {Ω : Type u_1} [MeasurableSpace Ω] (ρ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure ρ] {Q : Set Ω} (hQ : MeasurableSet Q) (hq : ρ Q ≠ 0) : ∀ᵐ (ω : ℕ → Ω) ∂MeasureTheory.Measure.infinitePi fun (x : ℕ) => ρ, ∃ (r : ℕ), ω r ∈ Q

A positive-mass success set is visited almost surely by an iid sequence.