English
Let α be a linear ordered type and x ∈ α. If g is almost everywhere μ-measurable on all intervals Ioc(x,t) with t > x, then g is almost everywhere μ-measurable on Ioi(x).
Русский
Пусть α упорядочено линейно, x∈α. Если g а.е.-измерима на всех интервалах Ioc(x,t) при t > x, то g а.е.-измерим на Ioi(x).
LaTeX
$$$\forall x\, \forall g: \alpha \to \beta,\ (\forall t>x,\ AEMeasurable\ g\ (\mu\restriction Ioc(x,t))) \Rightarrow AEMeasurable\ g\ (\mu\restriction Ioi(x))$$$
Lean4
theorem aemeasurable_Ioi_of_forall_Ioc {β} {mβ : MeasurableSpace β} [LinearOrder α]
[(atTop : Filter α).IsCountablyGenerated] {x : α} {g : α → β}
(g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))) : AEMeasurable g (μ.restrict (Ioi x)) :=
by
haveI : Nonempty α := ⟨x⟩
obtain ⟨u, hu_tendsto⟩ := exists_seq_tendsto (atTop : Filter α)
have Ioi_eq_iUnion : Ioi x = ⋃ n : ℕ, Ioc x (u n) :=
by
rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists
rw [Ioi_eq_iUnion, aemeasurable_iUnion_iff]
intro n
rcases lt_or_ge x (u n) with h | h
· exact g_meas (u n) h
· rw [Ioc_eq_empty (not_lt.mpr h), Measure.restrict_empty]
exact aemeasurable_zero_measure
