Finite degree-prefix observables

The path on a strict prefix depends only on the corresponding finite degree word.

@[instance_reducible]

def BGW.StableTrees.ExactPrefix.instMeasurableSpaceListNat : MeasurableSpace (List ℕ)

The discrete σ-algebra on words of natural numbers, used locally for countable sums.

Equations

• BGW.StableTrees.ExactPrefix.instMeasurableSpaceListNat = ⊤

theorem BGW.StableTrees.ExactPrefix.instMeasurableSingletonClassListNat_bGW : MeasurableSingletonClass (List ℕ)

theorem BGW.StableTrees.ExactPrefix.prefixWeightFn_nonneg (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (x : Skorokhod.D ↑a ℝ) : 0 ≤ prefixWeightFn μ B n a x

The exact-prefix weight is nonnegative, including totalized zero denominators.

theorem BGW.StableTrees.ExactPrefix.exactWalkPrefixLaw_eq_withDensity {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {n : ℕ} (hn : Admissible μ n) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ↑(exactWalkPrefixLaw μ B n hn a ⋯) = (↑(PathTail.tailWalkPrefixLaw μ B n a)).withDensity fun (x : Skorokhod.D ↑a ℝ) => ENNReal.ofReal (prefixWeightFn μ B n a x)

Prefix RN identity from the tail to the exact-size walk prefix law (K02 exactTreeLaw_prefix_eq_lintegral pushed through the prefix path).

theorem BGW.StableTrees.ExactPrefix.ae_latticeGood_tailWalkPrefixLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {n : ℕ} (hn : Admissible μ n) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ∀ᵐ (x : Skorokhod.D ↑a ℝ) ∂↑(PathTail.tailWalkPrefixLaw μ B n a), LatticeGood μ B n a x

Almost surely under the tail walk prefix law the path is lattice-good (n admissible).