norm_integral_le_of_le_const — Mathlib

English

If |f(x)| ≤ g(x) on the domain and μ is locally finite, then ||∫ f|| ≤ ∫ g with respect to μ.

Русский

Если |f(x)| ≤ g(x) на области и μ локально сконечного типа, то ||∫ f|| ≤ ∫ g по μ.

LaTeX

$$$\forall \mu, \text{IsLocallyFiniteMeasure } \mu \Rightarrow ||\int f|| ≤ \int g$$$

Lean4

theorem norm_integral_le_of_le_const {c : ℝ} (hc : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ c) (μ : Measure ℝⁿ)
    [IsLocallyFiniteMeasure μ] : ‖(integral I l f μ.toBoxAdditive.toSMul : E)‖ ≤ μ.real I * c := by
  simpa only [integral_const] using norm_integral_le_of_norm_le hc μ (integrable_const c)

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