English
In the Lp setting, if all set integrals vanish under suitable conditions for f, then f equals zero a.e.
Русский
В пространстве Lp, если эндеглазные интегралы по всем множествам равны нулю, то f = 0 a.e.
LaTeX
$$$$ f =_{a.e.} 0 $$$$
Lean4
/-- **Uniqueness of the conditional expectation** -/
theorem ae_eq_of_forall_setIntegral_eq' (hm : m ≤ m0) (f g : Lp E' p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
(hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn f s μ)
(hg_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn g s μ)
(hfg : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ)
(hf_meas : AEStronglyMeasurable[m] f μ) (hg_meas : AEStronglyMeasurable[m] g μ) : f =ᵐ[μ] g :=
by
suffices h_sub : ⇑(f - g) =ᵐ[μ] 0 by rw [← sub_ae_eq_zero]; exact (Lp.coeFn_sub f g).symm.trans h_sub
have hfg' : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 :=
by
intro s hs hμs
rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
exact sub_eq_zero.mpr (hfg s hs hμs)
have hfg_int : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (⇑(f - g)) s μ :=
by
intro s hs hμs
rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]
exact (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
exact
Lp.ae_eq_zero_of_forall_setIntegral_eq_zero' 𝕜 hm (f - g) hp_ne_zero hp_ne_top hfg_int hfg' <|
(hf_meas.sub hg_meas).congr (Lp.coeFn_sub f g).symm
