English
Existence of thickening radii with frontier measure zero for a given base μ and set s, across a family.
Русский
Существование радиусов толщины с нулевой мерой фронтира для заданного μ и множества s в семейном виде.
LaTeX
$$$\exists rs : \mathbb{N} \to \mathbb{R},\; \forall n,\; μ(\text{frontier}(\text{thickening}(rs(n), s))) = 0$$$
Lean4
/-- One implication of the portmanteau theorem:
If for all open sets G we have the liminf condition `μ(G) ≤ liminf μsₙ(G)`, then the measures
μsₙ converge weakly to the measure μ. Formulated here for countably generated filters. -/
theorem tendsto_of_forall_isOpen_le_liminf {ι : Type*} {μ : ProbabilityMeasure Ω} {μs : ι → ProbabilityMeasure Ω}
{L : Filter ι} [L.IsCountablyGenerated] (h_opens : ∀ G, IsOpen G → μ G ≤ L.liminf (fun i ↦ μs i G)) :
L.Tendsto (fun i ↦ μs i) (𝓝 μ) :=
by
apply Filter.tendsto_of_seq_tendsto (fun u hu ↦ ?_)
apply tendsto_of_forall_isOpen_le_liminf_nat (fun G hG ↦ ?_)
apply (h_opens G hG).trans
change _ ≤ atTop.liminf ((fun i ↦ μs i G) ∘ u)
rw [liminf_comp]
refine liminf_le_liminf_of_le hu (by isBoundedDefault) ?_
exact isBoundedUnder_of ⟨1, by simp⟩ |>.isCoboundedUnder_ge
