Exponential tilting preserves size-conditioned Bienaymé laws

If two offspring probability measures satisfy ν {k} = a * b ^ k * μ {k}, their tree laws restricted to size n differ by the constant a ^ n * b ^ (n - 1). For finite nonzero a and b, this factor cancels on conditioning. The equality holds at every size: at a null size event, including size zero, both conditioned measures are zero. No hypothesis on the offspring mean or on a lattice span is used.

This proves Proposition prop:tilting (Kennedy) of papers/arXiv-2503.07530v2 (1)/subcritical_cauchy_final_arxiv.tex, with the two offspring laws interchanged in the displayed tilting relation. It does not construct a tilt with a prescribed mean or assert that such a tilt exists.

theorem BGW.LocallyFinite.bienaymeLaw_restrict_sizeEvent_tilt (μ ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (a b : ENNReal) (htilt : ∀ (k : ℕ), ν {k} = a * b ^ k * μ {k}) (n : ℕ) : (bienaymeLaw ν).restrict (sizeEvent n) = (a ^ n * b ^ (n - 1)) • (bienaymeLaw μ).restrict (sizeEvent n)

On a fixed size class, exponential tilting scales the entire restricted tree law.

theorem BGW.LocallyFinite.bienaymeLaw_sizeEvent_tilt (μ ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (a b : ENNReal) (htilt : ∀ (k : ℕ), ν {k} = a * b ^ k * μ {k}) (n : ℕ) : (bienaymeLaw ν) (sizeEvent n) = a ^ n * b ^ (n - 1) * (bienaymeLaw μ) (sizeEvent n)

The mass of a fixed size class changes by its common tree-weight factor.

theorem BGW.LocallyFinite.bienaymeLaw_sizeEvent_ne_zero_iff_tilt (μ ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (a b : ENNReal) (htilt : ∀ (k : ℕ), ν {k} = a * b ^ k * μ {k}) (ha : a ≠ 0) (hb : b ≠ 0) (n : ℕ) : (bienaymeLaw ν) (sizeEvent n) ≠ 0 ↔ (bienaymeLaw μ) (sizeEvent n) ≠ 0

Nonzero tilt parameters preserve the set of admissible sizes.

theorem BGW.LocallyFinite.cond_sizeEvent_eq_of_tilt (μ ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (a b : ENNReal) (htilt : ∀ (k : ℕ), ν {k} = a * b ^ k * μ {k}) (ha : a ≠ 0) (ha_top : a ≠ ⊤) (hb : b ≠ 0) (hb_top : b ≠ ⊤) (n : ℕ) : (bienaymeLaw ν)[|sizeEvent n] = (bienaymeLaw μ)[|sizeEvent n]

Finite positive exponential tilting preserves size-conditioned tree measures. At inadmissible sizes, including zero, both sides are the zero measure.