English
If an integrable function f on α is such that its integrals over every measurable set s are nonnegative, then f is nonnegative almost everywhere.
Русский
Если интегрируемая функция f такая, что интегралы по всем измеримым множествам s неотрицательны, то f неотрицательна почти повсюду.
LaTeX
$$$0 \leq f \ ae$ в смыслe интегралов по подмножествам.$$
Lean4
theorem ae_nonneg_of_forall_setIntegral_nonneg (hf : Integrable f μ)
(hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) : 0 ≤ᵐ[μ] f :=
by
simp_rw [EventuallyLE, Pi.zero_apply]
rw [ae_const_le_iff_forall_lt_measure_zero]
intro b hb_neg
let s := {x | f x ≤ b}
have hs : NullMeasurableSet s μ := nullMeasurableSet_le hf.1.aemeasurable aemeasurable_const
have mus : μ s < ∞ := Integrable.measure_le_lt_top hf hb_neg
have h_int_gt : (∫ x in s, f x ∂μ) ≤ b * μ.real s :=
by
have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ :=
by
refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_
rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]
exact Eventually.of_forall fun x hxs => hxs
rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le
contrapose! h_int_gt with H
calc
b * μ.real s < 0 := mul_neg_of_neg_of_pos hb_neg <| ENNReal.toReal_pos H mus.ne
_ ≤ ∫ x in s, f x ∂μ := by
rw [← μ.restrict_toMeasurable mus.ne]
exact hf_zero _ (measurableSet_toMeasurable ..) (by rwa [measure_toMeasurable])
