English
If each f_i is strongly measurable, then the limit under a countable generated filter of the family f is strongly measurable as a function of the base point.
Русский
Если каждая функция f_i сильно измерима, то предел по счетному фильтру от семейства f сохраняет сильную измеримость по базовой точке.
LaTeX
$$$\text{limUnder}\ l\ (f\cdot x)\ is\ strongly\ measurable\ in\ x.$$$
Lean4
theorem measurableSet_exists_tendsto (hf : ∀ i, StronglyMeasurable (f i)) :
MeasurableSet {x | ∃ c, Tendsto (f · x) l (𝓝 c)} :=
by
obtain rfl | hl := eq_or_neBot l
· simp_all
borelize E
letI := upgradeIsCompletelyMetrizable E
let s := closure (⋃ i, range (f i))
have : PolishSpace s :=
{ toSecondCountableTopology :=
@UniformSpace.secondCountable_of_separable s _ _
(IsSeparable.iUnion (fun i ↦ (hf i).isSeparable_range)).closure.separableSpace
toIsCompletelyMetrizableSpace := isClosed_closure.isCompletelyMetrizableSpace }
let g i x : s := ⟨f i x, subset_closure <| mem_iUnion.2 ⟨i, ⟨x, rfl⟩⟩⟩
have mg i : Measurable (g i) := (hf i).measurable.subtype_mk
convert MeasureTheory.measurableSet_exists_tendsto (l := l) mg with x
refine ⟨fun ⟨c, hc⟩ ↦ ⟨⟨c, ?_⟩, tendsto_subtype_rng.2 hc⟩, fun ⟨c, hc⟩ ↦ ⟨c, tendsto_subtype_rng.1 hc⟩⟩
exact mem_closure_of_tendsto hc (Eventually.of_forall fun i ↦ mem_iUnion.2 ⟨i, ⟨x, rfl⟩⟩)
