Documentation

BGW.StableTrees.DiscreteBridgeRN

Path prefix Radon–Nikodym identities for the discrete bridge #

The conditional prefix-word masses are transported through the prefix path map. Nonzero norming recovers the integer walk endpoint by rounding.

source
@[instance_reducible]
def BGW.StableTrees.DiscreteBridge.rnWordMeasurable :
MeasurableSpace (List ℕ)

Discrete measurable structure for the prefix-word carrier in this module.

Equations
Instances For
    source
    theorem BGW.StableTrees.DiscreteBridge.rnWordSingleton :
    MeasurableSingletonClass (List ℕ)

    Every prefix-word singleton is measurable in the local structure.

    source
    theorem BGW.StableTrees.DiscreteBridge.measurable_bridgePathDensity (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) :
    Measurable (bridgePathDensity μ B n a)

    The path prefix density is measurable through its terminal coordinate.

    source
    theorem BGW.StableTrees.DiscreteBridge.endValue_forestWalkPath (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (ω : ℕ → ℕ) :
    endValue a (DiscreteForest.forestWalkPath B n a ω) = ↑(DiscreteForest.walk ω ⌊↑a * ↑n⌋₊) / B n

    The terminal value of a forest walk prefix is its integer partial sum divided by the norming.

    source
    theorem BGW.StableTrees.DiscreteBridge.map_forestWalkPath (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) :
    MeasureTheory.Measure.map (DiscreteForest.forestWalkPath B n a) ↑(DiscreteForest.offspringSeqLaw μ) = ↑(stepPathLaw (realOffspringStepLaw μ) (↑a) B n)

    The iid offspring sequence pushed through its prefix path has the canonical step-path law.

    source
    theorem BGW.StableTrees.DiscreteBridge.restrictLaw_walkBridgeLaw_eq_withDensity {μ : PMF ℕ} {B : ℕ → ℝ} {n : ℕ} (hn : Admissible μ n) (hB : B n ≠ 0) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) :
    ↑(restrictLaw a ⋯ (walkBridgeLaw μ B n hn)) = (↑(stepPathLaw (realOffspringStepLaw μ) (↑a) B n)).withDensity fun (x : Skorokhod.D ↑a ℝ) => ENNReal.ofReal (bridgePathDensity μ B n a x)

    Prefix Radon-Nikodym identity: for a < 1, admissible n and nonzero norming B n (without it the rounded endpoint loses the walk value: audit finding 1), the bridge path on [0,a] has density bridgePathDensity with respect to the unconditioned step-path law.