norm_integral_min_max — Mathlib

English

Let f: R → E be a function into a normed additive group E, and μ be a measure on R. Then the norm of the integral of f over the closed interval with endpoints a and b equals the norm of the integral over the closed interval with endpoints min(a,b) and max(a,b): ∥∫_{min(a,b)}^{max(a,b)} f(x) dμ∥ = ∥∫_{a}^{b} f(x) dμ∥.

Русский

Пусть f: ℝ → E, E — нормированная абелева группа, μ — мера на ℝ. Тогда норма интеграла функции f по замкнутому интервалу между a и b равна норме интеграла по замкнутому интервалу между min(a,b) и max(a,b): ∥∫_{min(a,b)}^{max(a,b)} f(x) dμ∥ = ∥∫_{a}^{b} f(x) dμ∥.

LaTeX

$$$\|\int_{\min(a,b)}^{\max(a,b)} f(x) \, d\mu\| = \|\int_{a}^{b} f(x) \, d\mu\|$$$

Lean4

theorem norm_integral_min_max (f : ℝ → E) : ‖∫ x in min a b..max a b, f x ∂μ‖ = ‖∫ x in a..b, f x ∂μ‖ := by
  cases le_total a b <;> simp [*, integral_symm a b]

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