Initial source truncation and erasure #
Initial time truncation is characterized by distribution functions, without choosing a crossing time. Capping a Stieltjes function therefore erases the top mass of its pushed-forward source, including a partial boundary atom and the case where the entire source is erased.
theorem
BGW.StableTrees.map_fresh_height_translation
{μ : MeasureTheory.Measure ℝ}
{τ : ℝ → ℝ}
(hτ : Measurable τ)
{φ ψ : ℝ → NNReal}
(hφ : Measurable φ)
(hψ : Measurable ψ)
(K : NNReal)
(he : ∀ᵐ (x : ℝ) ∂μ, φ (τ x) = ψ x + K)
:
MeasureTheory.Measure.map φ (MeasureTheory.Measure.map τ μ) = MeasureTheory.Measure.map (fun (h : NNReal) => h + K) (MeasureTheory.Measure.map ψ μ)
A measurable time change and a height translation commute with the fresh pushforward.
theorem
BGW.StableTrees.map_eq_eraseMass_of_initial_cdf
{ν ν' : MeasureTheory.Measure ℝ}
[MeasureTheory.IsFiniteMeasure ν]
[MeasureTheory.IsFiniteMeasure ν']
{φ : ℝ → NNReal}
(hφ : Measurable φ)
(hmono : Monotone φ)
(m : ENNReal)
(htot : ν' Set.univ = ν Set.univ - m)
(hcdf : ∀ (a : ℝ), ν' (Set.Iic a) = min (ν (Set.Iic a)) (ν Set.univ - m))
:
A monotone height map preserves initial-segment distribution-function truncation.
theorem
BGW.StableTrees.map_stieltjes_min_eq_eraseMass
{F G : StieltjesFunction ℝ}
{T c : ℝ}
(hT : 0 ≤ T)
(hc : c ≤ ↑F T)
(he : ∀ x ∈ Set.Icc 0 T, ↑G x = min (↑F x) c)
{φ : ℝ → NNReal}
(hφ : Measurable φ)
(hmono : Monotone φ)
:
MeasureTheory.Measure.map φ (G.measure.restrict (Set.Ioc 0 T)) = eraseMass (ENNReal.ofReal (↑F T - c)) (MeasureTheory.Measure.map φ (F.measure.restrict (Set.Ioc 0 T)))
A monotone height map turns a capped Stieltjes source into top-mass erasure.
theorem
BGW.StableTrees.map_stieltjes_min_eq_eraseMass_of_ae
{F G : StieltjesFunction ℝ}
{T c : ℝ}
(hT : 0 ≤ T)
(hc : c ≤ ↑F T)
(he : ∀ x ∈ Set.Icc 0 T, ↑G x = min (↑F x) c)
{φ ψ : ℝ → NNReal}
(hψ : Measurable ψ)
(hmono : Monotone ψ)
(heq : ∀ᵐ (x : ℝ) ∂F.measure.restrict (Set.Ioc 0 T), φ x = ψ x)
:
MeasureTheory.Measure.map φ (G.measure.restrict (Set.Ioc 0 T)) = eraseMass (ENNReal.ofReal (↑F T - c)) (MeasureTheory.Measure.map φ (F.measure.restrict (Set.Ioc 0 T)))
A measurable height map agreeing with a monotone clock on the original source also erases.