English
Let m be a sub-sigma-algebra of m0. If f is m0-measurable and g is m-measurable, and their (signed) integrals agree on every m-measurable set of finite measure, then for every m-measurable set s with μ(s) finite, the L1-norm of g on s is at most the L1-norm of f on s; that is, ∫_s |g| ≤ ∫_s |f|.
Русский
Пусть m ≤ m0. Пусть f есть m0-правда измеримая функция, a g — m-измеримая. Пусть их интегралы по любому m-измеримому множеству конечного меры совпадают. Тогда для всякого множества s, измеримого по m, с μ(s) < ∞, выполняется ∫_s |g| ≤ ∫_s |f|.
LaTeX
$$$\\forall m \\le m_0\\;\\forall f,g:\\alpha \\to \\mathbb{R}\\;\\Big( \\text{StronglyMeasurable } f \\land \\text{IntegrableOn } f\\, s\\, \\mu \\land \\text{StronglyMeasurable}[m]\, g \\land \\text{IntegrableOn } g\, s\, \\mu \\land \\forall t,\\ MeasurableSet[m]\\ t \\rightarrow \\mu t < \\infty \\rightarrow \\int_{t} g \\, d\\mu = \\int_{t} f \\, d\\mu\\Big) \\rightarrow \\forall s,\\ MeasurableSet[m] s \\rightarrow \\mu s \\neq \\infty \\rightarrow \\int_{s} |g| \\, d\\mu \\le \\int_{s} |f| \\, d\\mu$$
Lean4
/-- Let `m` be a sub-σ-algebra of `m0`, `f` an `m0`-measurable function and `g` an `m`-measurable
function, such that their integrals coincide on `m`-measurable sets with finite measure.
Then `∫ x in s, ‖g x‖ ∂μ ≤ ∫ x in s, ‖f x‖ ∂μ` on all `m`-measurable sets with finite measure. -/
theorem integral_norm_le_of_forall_fin_meas_integral_eq (hm : m ≤ m0) {f g : α → ℝ} (hf : StronglyMeasurable f)
(hfi : IntegrableOn f s μ) (hg : StronglyMeasurable[m] g) (hgi : IntegrableOn g s μ)
(hgf : ∀ t, MeasurableSet[m] t → μ t < ∞ → ∫ x in t, g x ∂μ = ∫ x in t, f x ∂μ) (hs : MeasurableSet[m] s)
(hμs : μ s ≠ ∞) : (∫ x in s, ‖g x‖ ∂μ) ≤ ∫ x in s, ‖f x‖ ∂μ :=
by
rw [integral_norm_eq_pos_sub_neg hgi, integral_norm_eq_pos_sub_neg hfi]
have h_meas_nonneg_g : MeasurableSet[m] {x | 0 ≤ g x} := (@stronglyMeasurable_const _ _ m _ _).measurableSet_le hg
have h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x} := stronglyMeasurable_const.measurableSet_le hf
have h_meas_nonpos_g : MeasurableSet[m] {x | g x ≤ 0} := hg.measurableSet_le (@stronglyMeasurable_const _ _ m _ _)
have h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0} := hf.measurableSet_le stronglyMeasurable_const
refine sub_le_sub ?_ ?_
· rw [Measure.restrict_restrict (hm _ h_meas_nonneg_g), Measure.restrict_restrict h_meas_nonneg_f,
hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonneg_g hs)
((measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμs)),
← Measure.restrict_restrict (hm _ h_meas_nonneg_g), ← Measure.restrict_restrict h_meas_nonneg_f]
exact setIntegral_le_nonneg (hm _ h_meas_nonneg_g) hf hfi
· rw [Measure.restrict_restrict (hm _ h_meas_nonpos_g), Measure.restrict_restrict h_meas_nonpos_f,
hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonpos_g hs)
((measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμs)),
← Measure.restrict_restrict (hm _ h_meas_nonpos_g), ← Measure.restrict_restrict h_meas_nonpos_f]
exact setIntegral_nonpos_le (hm _ h_meas_nonpos_g) hf hfi
