English
Suppose m ≤ m0, f,g: α→ℝ with integrability properties and the same finite-measure integrals on m-sets; then on any m-measurable s with μ(s) finite, the Lintegral of the norm of g is at most that of f: ∫⁻_s ‖g‖ ≤ ∫⁻_s ‖f‖.
Русский
Пусть m ≤ m0, f,g: α→ℝ с соответствующими интегрируемыми свойствами и равенствами интегралов на множество с конечной мерой; тогда для любого m-измеримого s с μ(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⁻ x \\in s, ‖g x‖ \\partial μ ≤ \\int⁻ x \\in s, ‖f x‖ \\partial μ$$
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 lintegral_enorm_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 [← ofReal_integral_norm_eq_lintegral_enorm hfi, ← ofReal_integral_norm_eq_lintegral_enorm hgi,
ENNReal.ofReal_le_ofReal_iff]
· exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs
· positivity
