The prefix Radon–Nikodym identity and its mass

On the countable space of degree words the atom identities determine the entire prefix measure. Invalid prefixes have zero exact mass. Zero remaining-tail mass also forces zero remaining exact mass, respecting totalized division.

@[instance_reducible]

def BGW.StableTrees.DiscreteForest.prefixDensityWordMeasurable : MeasurableSpace (List ℕ)

A local discrete measurable structure for prefix-law comparison.

Equations

• BGW.StableTrees.DiscreteForest.prefixDensityWordMeasurable = ⊤

theorem BGW.StableTrees.DiscreteForest.prefixDensityWordSingleton : MeasurableSingletonClass (List ℕ)

Single words are measurable in the local prefix-law structure.

theorem BGW.StableTrees.DiscreteForest.exactTreeLaw_prefix_eq_lintegral (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} (hn : Admissible μ n) (hmn : m < n) (S : Set (List ℕ)) : ↑(exactTreeLaw μ n) (treePrefix m ⁻¹' S) = ∫⁻ (τ : LocallyFinite.Tree) in treePrefix m ⁻¹' S, prefixDensity μ n m (treePrefix m τ) ∂↑(tailTreeLaw μ n)

Radon-Nikodym identity from the tail to the exact law on the first-m-degrees sigma-field: for every set S of degree words, P_exact(prefix ∈ S) = ∫_{prefix ∈ S} prefixDensity d P_tail.

theorem BGW.StableTrees.DiscreteForest.lintegral_prefixDensity_tail (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} (hn : Admissible μ n) (hmn : m < n) : ∫⁻ (τ : LocallyFinite.Tree), prefixDensity μ n m (treePrefix m τ) ∂↑(tailTreeLaw μ n) = 1

The tail expectation of the RN density is one.