tendsto_measure_of_null_frontier_of_tendsto'

English

There exists thickening radii r with positive inner radii such that the frontier of the thickened set has measure zero.

Русский

Существует последовательность толщин радиусов r с положительным внутренним радиусом, так что frontier(толщина(r, s)) имеет нулевую меру.

LaTeX

$$$\exists r\in (a,b),\; \mu(\text{frontier}(\text{thickening}(r,s)))=0$$$

Lean4

theorem tendsto_measure_of_null_frontier_of_tendsto' {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω]
    [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : ProbabilityMeasure Ω}
    {μs : ι → ProbabilityMeasure Ω} (μs_lim : Tendsto μs L (𝓝 μ)) {E : Set Ω}
    (E_nullbdry : (μ : Measure Ω) (frontier E) = 0) :
    Tendsto (fun i ↦ (μs i : Measure Ω) E) L (𝓝 ((μ : Measure Ω) E)) :=
  haveI h_opens : ∀ G, IsOpen G → (μ : Measure Ω) G ≤ L.liminf fun i ↦ (μs i : Measure Ω) G := fun _ G_open ↦
    le_liminf_measure_open_of_tendsto μs_lim G_open
  tendsto_measure_of_null_frontier h_opens E_nullbdry

Похожие утверждения