English
If the interior of the integrable exponential set of X with μ is nonempty, then X is almost everywhere measurable.
Русский
Если interior интегрируемого экспонентного множества X по μ непуст, то X измеримо почти всюду.
LaTeX
$$$\text{If } \operatorname{int}(\text{integrableExpSet}(X,\mu)) \neq \emptyset, \text{ then } X \text{ is AEMeasurable w.r.t. } \mu.$$$
Lean4
/-- If the interior of the interval `integrableExpSet X μ` is nonempty,
then `X` is a.e. measurable. -/
theorem aemeasurable_of_mem_interior_integrableExpSet (hv : v ∈ interior (integrableExpSet X μ)) : AEMeasurable X μ :=
by
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv
obtain ⟨l, u, hvlu, h_subset⟩ := hv
let t := ((v - l) ⊓ (u - v)) / 2
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
have ht : 0 < t := half_pos h_pos
by_cases hvt : v + t = 0
· have hvt' : v - t ≠ 0 := by
rw [sub_ne_zero]
refine fun h_eq ↦ ht.ne' ?_
simpa [h_eq] using hvt
exact aemeasurable_of_aemeasurable_exp_mul hvt' (h_subset (sub_half_inf_sub_mem_Ioo hvlu)).aemeasurable
· exact aemeasurable_of_aemeasurable_exp_mul hvt (h_subset (add_half_inf_sub_mem_Ioo hvlu)).aemeasurable
