English
Let s be a set and b a nonzero constant in β, with MeasurableSingletonClass β. Then AEMeasurable (indicator s (fun _ ↦ b)) μ iff NullMeasurableSet s μ.
Русский
Для набора s и постоянной величины b ≠ 0 в β (β имеет класс измеримых одноэлементов) верно: AЕ-мeасируемость индикатора, равного b на s, относительно μ эквивалентна нулевой измеримости множества s относительно μ.
LaTeX
$$$\mathrm{AEMeasurable}(\mathrm{indicator}\ s\ (\lambda\_.\ b),\ μ) \iff \mathrm{NullMeasurableSet}(s, μ)$$$
Lean4
/-- A characterization of the a.e.-measurability of the indicator function which takes a constant
value `b` on a set `A` and `0` elsewhere. -/
theorem aemeasurable_indicator_const_iff {s} [MeasurableSingletonClass β] (b : β) [NeZero b] :
AEMeasurable (s.indicator (fun _ ↦ b)) μ ↔ NullMeasurableSet s μ := by
classical
constructor <;> intro h
· convert h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl
rw [indicator_const_preimage_eq_union s {0}ᶜ b]
simp [NeZero.ne b]
· exact (aemeasurable_indicator_iff₀ h).mpr aemeasurable_const
