Convergence of Integrals After Conditioning on a Larger Ball

This statement formalizes the conditioning step of Letwin's Lemma A.1.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $(ν_k)$ and $μ$ be probability measures on $E$, with $ν_k\to μ$ in the topology of weak convergence. Let $r<R$, assume that $μ$ gives measure zero to the complement of $\overline B(0,r)$, and let $f:E\to\mathbb R$ be continuous. Then

The conclusion concerns the conditional probability measures ProbabilityTheory.cond on the closed ball; no boundedness assumption on $f$ is stated.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS. Shown in its original module context. Proof omitted.

theorem tendsto_integral_cond_closedBall {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ν : ℕ → ProbabilityMeasure E}
    {μ : ProbabilityMeasure E} (hν : Tendsto ν atTop (𝓝 μ)) {r R : ℝ} (hrR : r < R)
    (hsupp : (μ : Measure E) (closedBall (0 : E) r)ᶜ = 0) {f : E → ℝ} (hf : Continuous f) :
    Tendsto (fun k => ∫ x, f x ∂(ProbabilityTheory.cond (ν k : Measure E) (closedBall (0 : E) R)))
      atTop (𝓝 (∫ x, f x ∂(μ : Measure E)))

Module navigation

Module: Probability/Conditioning.

Source excerpt, lines 372–377 · Frozen source 408915f.