Weak convergence under perturbations on varying probability spaces

Adapted from Freezing2/Probability/WeakPerturbation.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

The finite-tree laws change with the horizon. The bounded-Lipschitz estimate below therefore keeps the probability measure indexed by the horizon rather than requiring all random variables to live under one fixed measure.

theorem BGW.MetricMeasure.tendsto_probabilityMap_of_error_probability {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {E : Type u_2} [MeasurableSpace E] [PseudoMetricSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) {F G : (n : ℕ) → Ω n → E} {ν : MeasureTheory.ProbabilityMeasure E} (hF : ∀ (n : ℕ), Measurable (F n)) (hG : ∀ (n : ℕ), Measurable (G n)) (herr : ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ε < dist (F n ω) (G n ω)}) Filter.atTop (nhds 0)) (hlim : Filter.Tendsto (fun (n : ℕ) => (μ n).map (G n)) Filter.atTop (nhds ν)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map (F n)) Filter.atTop (nhds ν)

An error vanishing in probability preserves weak convergence of laws, also on varying probability spaces. The strict tail convention matches the sampled distance-matrix estimates.