norm_integral_le_of_norm_le_const

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

URI: https://scilib.ai/kg/mathlib#intervalIntegral.norm_integral_le_of_norm_le_const

← MathLib Explorer

English

If a.e. ‖f t‖ ≤ C on Ι a b, then ∥∫ f∥ ≤ |b-a| · C.

Русский

Если почти везде ‖f t‖ ≤ C на Ι a b, то ∥∫ f∥ ≤ |b-a| · C.

LaTeX

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

Lean4

theorem norm_integral_le_of_norm_le_const {a b C : ℝ} {f : ℝ → E} (h : ∀ x ∈ Ι a b, ‖f x‖ ≤ C) :
    ‖∫ x in a..b, f x‖ ≤ C * |b - a| :=
  norm_integral_le_of_norm_le_const_ae <| Eventually.of_forall h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru