norm_integral_le_of_norm_le_const_ae

English

If ‖f t‖ ≤ C a.e. on Ι a b, then ∥∫_{a}^{b} f t ∂μ∥ ≤ C · |b - a|.

Русский

Если ‖f(t)‖ ≤ C почти всюду на Ι a b, то ∥∫_{a}^{b} f(t) dt∥ ≤ C · |b - a|.

LaTeX

$$$\|\int_{a}^{b} f(t) \, dμ\| \leq C \cdot |b - a|$$

Lean4

theorem norm_integral_le_of_norm_le_const_ae {a b C : ℝ} {f : ℝ → E} (h : ∀ᵐ x, x ∈ Ι a b → ‖f x‖ ≤ C) :
    ‖∫ x in a..b, f x‖ ≤ C * |b - a| :=
  by
  rw [norm_integral_eq_norm_integral_uIoc]
  convert norm_setIntegral_le_of_norm_le_const_ae' _ h using 1
  · rw [uIoc, Real.volume_real_Ioc_of_le inf_le_sup, max_sub_min_eq_abs]
  · simp [uIoc, Real.volume_Ioc]

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