English
If m ≤ m0, s is m-measurable, and f is AEStronglyMeasurable on μ with f vanishing off s, under suitable compatibility with another σ-algebra m', then f is AEStronglyMeasurable with respect to m'.
Русский
Если m ≤ m0, множество s мeа-измеримо, а f является AEStronglyMeasurable по μ и нуль вне s, при условии совместимости σ-алгебр m' на ограничении, тогда f является AEStronglyMeasurable по m'.
LaTeX
$$$m \\le m_0 \\rightarrow MeasurableSet[m]\, s \\rightarrow (\\forall t, MeasurableSet[m](s \\cap t) \\rightarrow MeasurableSet[m'](s \\cap t)) \\rightarrow AEStronglyMeasurable[m] f μ \\rightarrow (f =^{\\mu}_{\\text{restrict } s^c} 0) \\Rightarrow AEStronglyMeasurable[m'] f μ$$$
Lean4
/-- If the restriction to a set `s` of a σ-algebra `m` is included in the restriction to `s` of
another σ-algebra `m₂` (hypothesis `hs`), the set `s` is `m` measurable and a function `f` almost
everywhere supported on `s` is `m`-ae-strongly-measurable, then `f` is also
`m₂`-ae-strongly-measurable. -/
theorem of_measurableSpace_le_on {m' m₀ : MeasurableSpace α} {μ : Measure[m₀] α} [Zero β] (hm : m ≤ m₀) {s : Set α}
(hs_m : MeasurableSet[m] s) (hs : ∀ t, MeasurableSet[m] (s ∩ t) → MeasurableSet[m'] (s ∩ t))
(hf : AEStronglyMeasurable[m] f μ) (hf_zero : f =ᵐ[μ.restrict sᶜ] 0) : AEStronglyMeasurable[m'] f μ :=
by
have h_ind_eq : s.indicator (hf.mk f) =ᵐ[μ] f :=
by
refine Filter.EventuallyEq.trans ?_ <| indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs_m) hf_zero
filter_upwards [hf.ae_eq_mk] with x hx
by_cases hxs : x ∈ s
· simp [hxs, hx]
· simp [hxs]
suffices StronglyMeasurable[m'] (s.indicator (hf.mk f)) from this.aestronglyMeasurable.congr h_ind_eq
exact
(hf.stronglyMeasurable_mk.indicator hs_m).stronglyMeasurable_of_measurableSpace_le_on hs_m hs fun x hxs =>
Set.indicator_of_notMem hxs _
