ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite

English

If the restricted measure μ|t is finite on t and f is integrable on t, and all restricted set integrals are nonnegative, then f ≥ 0 a.e. with respect to μ|t.

Русский

Пусть μ|t конечна на t, f интегрируема на t, и все интегралы по подмножествам s∩t неотрицательны; тогда f ≥ 0 a.e. относительно μ|t.

LaTeX

$$$0 \leq_{a.e.\,μ|t} f$$$

Lean4

theorem ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite [SigmaFinite μ] {f : α → ℝ}
    (hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) : 0 ≤ᵐ[μ] f :=
  by
  apply ae_of_forall_measure_lt_top_ae_restrict
  intro t t_meas t_lt_top
  apply ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter (hf_int_finite t t_meas t_lt_top)
  intro s s_meas _
  exact hf_zero _ (s_meas.inter t_meas) (lt_of_le_of_lt (measure_mono (Set.inter_subset_right)) t_lt_top)

Похожие утверждения