Weighted weak convergence on separable metric spaces #
Dudley representation transfers the weights to a common probability space. The mass-one Scheffé theorem then gives convergence of bounded continuous weighted expectations.
theorem
BGW.StableTrees.ExactPrefix.tendsto_integral_mul_weight
{E : Type u_1}
[MetricSpace E]
[MeasurableSpace E]
[BorelSpace E]
[TopologicalSpace.SeparableSpace E]
{P : ℕ → MeasureTheory.ProbabilityMeasure E}
{P₀ : MeasureTheory.ProbabilityMeasure E}
(hP : Filter.Tendsto P Filter.atTop (nhds P₀))
{w : ℕ → E → ℝ}
{w₀ : E → ℝ}
(hw : ∀ (k : ℕ), Measurable (w k))
(hw₀ : Measurable w₀)
(hnn : ∀ (k : ℕ) (x : E), 0 ≤ w k x)
(hnn₀ : ∀ (x : E), 0 ≤ w₀ x)
(h1 : ∀ (k : ℕ), ∫ (x : E), w k x ∂↑(P k) = 1)
(h10 : ∫ (x : E), w₀ x ∂↑P₀ = 1)
(S : ℕ → Set E)
(hS : ∀ (k : ℕ), ↑(P k) (S k)ᶜ = 0)
(G : Set E)
(hG : ↑P₀ Gᶜ = 0)
(hconv :
∀ x ∈ G,
∀ (y : ℕ → E),
(∀ (k : ℕ), y k ∈ S k) →
Filter.Tendsto y Filter.atTop (nhds x) → Filter.Tendsto (fun (k : ℕ) => w k (y k)) Filter.atTop (nhds (w₀ x)))
(F : BoundedContinuousFunction E ℝ)
:
Generic weighted-convergence helper (also for K15). If P_k ⇒ P₀ on a separable metric
space, w_k, w₀ ≥ 0 have mean one under P_k, P₀, and w_k (y_k) → w₀ (x) whenever
y_k → x with x ∈ G (P₀ G = 1) and y_k ∈ S_k (P_k S_k = 1), then the weighted measures
converge weakly: ∫ F w_k dP_k → ∫ F w₀ dP₀ for every bounded continuous F. (Skorokhod
coupling, a.s. convergence of weights, Scheffé.)