English
If |f(x)| ≤ g(x) and g is integrable, then ||∫ f|| ≤ ∫ g.
Русский
Если модуль функции f не превышает g и g интегрируема, то модуль интеграла f не превосходит интеграла g.
LaTeX
$$$\forall x, \ |f(x)| \le g(x) \Rightarrow \|\int f\| ≤ \int g$ (при интегрируемости g)$$
Lean4
/-- If `‖f x‖ ≤ g x` on `[l, u]` and `g` is integrable, then the norm of the integral of `f` is less
than or equal to the integral of `g`. -/
theorem norm_integral_le_of_norm_le {g : ℝⁿ → ℝ} (hle : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ g x) (μ : Measure ℝⁿ)
[IsLocallyFiniteMeasure μ] (hg : Integrable I l g μ.toBoxAdditive.toSMul) :
‖(integral I l f μ.toBoxAdditive.toSMul : E)‖ ≤ integral I l g μ.toBoxAdditive.toSMul :=
by
by_cases hfi : Integrable.{u, v, v} I l f μ.toBoxAdditive.toSMul
· refine le_of_tendsto_of_tendsto' hfi.hasIntegral.norm hg.hasIntegral fun π => ?_
refine norm_sum_le_of_le _ fun J _ => ?_
simp only [BoxAdditiveMap.toSMul_apply, norm_smul, smul_eq_mul, Real.norm_eq_abs, μ.toBoxAdditive_apply,
abs_of_nonneg measureReal_nonneg]
gcongr
exact hle _ <| π.tag_mem_Icc _
· rw [integral, dif_neg hfi, norm_zero]
exact integral_nonneg (fun x hx => (norm_nonneg _).trans (hle x hx)) μ
