continuousOn_smul — Mathlib

English

Let g be interval integrable on [a,b] with respect to μ, and let f be continuous on [a,b]. Then the pointwise scalar multiple f(x) • g(x) is interval integrable on [a,b] (with respect to μ).

Русский

Пусть g является интервално интегрируемой по отношению к μ на отрезке [a,b], и пусть f непрерывна на [a,b]. Тогда f(x)·g(x) интегрируема по интервалу на этом же отрезке.

LaTeX

$$$IntervalIntegrable(g, μ, a, b) \land ContinuousOn(f, [a,b]) \\Rightarrow IntervalIntegrable(x \\mapsto f(x) \\cdot g(x), μ, a, b)$$$

Lean4

theorem continuousOn_smul (hg : IntervalIntegrable g μ a b) (hf : ContinuousOn f [[a, b]]) :
    IntervalIntegrable (fun x => f x • g x) μ a b :=
  by
  rw [intervalIntegrable_iff] at hg ⊢
  exact hg.continuousOn_smul_of_subset hf isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

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