Documentation

BGW.StableTrees.DiscreteHeightApproxRenewalRestart

Restart with the height of a weak ascending epoch #

The complete restarted sequence is independent of every pre-stopped event. Applying this to an epoch's attained walk value permits occupation at that random gap level.

source
noncomputable def BGW.StableTrees.DiscreteHeightApprox.epochRestart (i : ℕ) (ω : ℕ → ℕ) :
ℕ → ℕ

The sequence restarted at the ith totalized natural weak epoch.

Equations
Instances For
    source
    theorem BGW.StableTrees.DiscreteHeightApprox.measurable_epochRestart (i : ℕ) :
    Measurable (epochRestart i)

    Restart at a natural weak epoch is measurable on all sequences.

    source
    noncomputable def BGW.StableTrees.DiscreteHeightApprox.weakEpochHeight (ω : ℕ → ℕ) (i : ℕ) :
    ℕ

    The nonnegative attained height of a weak ascending epoch.

    Equations
    Instances For
      source
      theorem BGW.StableTrees.DiscreteHeightApprox.walk_weakEpoch_nonneg {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i : ℕ) :
      0 ≤ DiscreteForest.walk ω (weakEpoch ω i)

      The walk value at a weak epoch is nonnegative on finite paths.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.weakEpochHeight_cast {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i : ℕ) :
      ↑(weakEpochHeight ω i) = DiscreteForest.walk ω (weakEpoch ω i)

      Natural epoch heights agree with the attained integer walk values on finite paths.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.measurable_walk_epoch (i : ℕ) :
      Measurable fun (ω : ℕ → ℕ) => DiscreteForest.walk ω (weakEpoch ω i)

      Walk evaluation at a totalized natural weak epoch is measurable.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.measurable_weakEpochHeight (i : ℕ) :
      Measurable fun (ω : ℕ → ℕ) => weakEpochHeight ω i

      Every attained natural epoch height is measurable.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.map_epochRestart_restrict (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (i : ℕ) {E : Set (ℕ → ℕ)} (hE : DiscreteForest.PreStopped (fun (ω : ℕ → ℕ) => weakEpochStop ω i) E) :
      MeasureTheory.Measure.map (epochRestart i) ((↑(DiscreteForest.offspringSeqLaw μ)).restrict E) = ↑(DiscreteForest.offspringSeqLaw μ) E • ↑(DiscreteForest.offspringSeqLaw μ)

      Restricted restart law for any pre-stopped event at a genuine weak epoch.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_epochRestart_restrict (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (i : ℕ) {E : Set (ℕ → ℕ)} (hE : DiscreteForest.PreStopped (fun (ω : ℕ → ℕ) => weakEpochStop ω i) E) {F : (ℕ → ℕ) → ENNReal} (hF : Measurable F) :
      ∫⁻ (ω : ℕ → ℕ) in E, F (epochRestart i ω) ∂↑(DiscreteForest.offspringSeqLaw μ) = ↑(DiscreteForest.offspringSeqLaw μ) E * ∫⁻ (ω : ℕ → ℕ), F ω ∂↑(DiscreteForest.offspringSeqLaw μ)

      Nonnegative integrals factor at a weak epoch over any pre-stopped event.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_epochRestart_level (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (i h : ℕ) :
      ∫⁻ (ω : ℕ → ℕ) in {ω : ℕ → ℕ | DiscreteForest.walk ω (weakEpoch ω i) = ↑h}, levelOccupation h (epochRestart i ω) ∂↑(DiscreteForest.offspringSeqLaw μ) = ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | DiscreteForest.walk ω (weakEpoch ω i) = ↑h}

      The occupation of the epoch's attained integer gap has conditional mean one.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_epochRestart_height (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (i h : ℕ) {F : (ℕ → ℕ) → ENNReal} (hF : Measurable F) :
      ∫⁻ (ω : ℕ → ℕ) in {ω : ℕ → ℕ | weakEpochHeight ω i = h}, F (epochRestart i ω) ∂↑(DiscreteForest.offspringSeqLaw μ) = ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | weakEpochHeight ω i = h} * ∫⁻ (ω : ℕ → ℕ), F ω ∂↑(DiscreteForest.offspringSeqLaw μ)

      Restarted nonnegative observables factor over each attained natural epoch height.