English
There exists a natural homeomorphism between X and the image range of diracProba, making diracProbaEquiv a homeomorphism onto its image.
Русский
Существует естественный гомеоморфизм между X и образом диапазона diracProba, делающий diracProbaEquiv гомеоморфизмом на его образ.
LaTeX
$$$\\text{diracProbaHomeomorph}: X \\to range(\\mathrm{diracProba}) \\quad\\text{is a homeomorphism}$$$
Lean4
theorem not_tendsto_diracProba_of_not_tendsto [CompletelyRegularSpace X] {x : X} (L : Filter X)
(h : ¬Tendsto id L (𝓝 x)) : ¬Tendsto diracProba L (𝓝 (diracProba x)) :=
by
obtain ⟨U, U_nhds, hU⟩ : ∃ U, U ∈ 𝓝 x ∧ ∃ᶠ x in L, x ∉ U :=
by
by_contra! con
apply h
intro U U_nhds
simpa only [not_frequently, not_not] using con U U_nhds
have Uint_nhds : interior U ∈ 𝓝 x := by simpa only [interior_mem_nhds] using U_nhds
obtain ⟨f, fx_eq_one, f_vanishes_outside⟩ :=
CompletelyRegularSpace.exists_BCNN isOpen_interior.isClosed_compl
(by simpa only [mem_compl_iff, not_not] using mem_of_mem_nhds Uint_nhds)
rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto, not_forall]
use f
simp only [diracProba, ProbabilityMeasure.coe_mk, fx_eq_one,
lintegral_dirac' _ (measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable)]
apply not_tendsto_iff_exists_frequently_notMem.mpr
refine ⟨Ioi 0, Ioi_mem_nhds (by simp only [ENNReal.coe_one, zero_lt_one]), hU.mp (Eventually.of_forall ?_)⟩
intro x x_notin_U
rw [f_vanishes_outside x (compl_subset_compl.mpr (show interior U ⊆ U from interior_subset) x_notin_U)]
simp only [ENNReal.coe_zero, mem_Ioi, lt_self_iff_false, not_false_eq_true]
