English
The linear (Monoid) homomorphism structure is compatible with AEEqFun construction, aligning sums and scalar multiplications.
Русский
Структура линейного гомоморфизма согласуется с построением AEEqFun: суммы и скаляры сохраняются.
LaTeX
$$$L(x+y) = Lx + Ly$ and $L(cx) = cLx$ for the appropriate linear structure.$$
Lean4
theorem ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real {f : α → ℝ}
(hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
(hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) {t : Set α} (ht : MeasurableSet t)
(hμt : μ t ≠ ∞) : f =ᵐ[μ.restrict t] 0 :=
by
suffices h_and : f ≤ᵐ[μ.restrict t] 0 ∧ 0 ≤ᵐ[μ.restrict t] f from
h_and.1.mp (h_and.2.mono fun x hx1 hx2 => le_antisymm hx2 hx1)
refine
⟨?_,
ae_nonneg_restrict_of_forall_setIntegral_nonneg hf_int_finite (fun s hs hμs => (hf_zero s hs hμs).symm.le) ht hμt⟩
suffices h_neg : 0 ≤ᵐ[μ.restrict t] -f by
refine h_neg.mono fun x hx => ?_
rw [Pi.neg_apply] at hx
simpa using hx
refine
ae_nonneg_restrict_of_forall_setIntegral_nonneg (fun s hs hμs => (hf_int_finite s hs hμs).neg) (fun s hs hμs => ?_)
ht hμt
simp_rw [Pi.neg_apply]
rw [integral_neg, neg_nonneg]
exact (hf_zero s hs hμs).le
