English
Let f: R → E be a function valued in a normed space. The average value of f over the interval [a, b] is equal to the (vector) inverse of the interval length times the integral of f over [a, b].
Русский
Пусть f: R → E — функция в нормированном пространстве. Среднее значение f на отрезке [a, b] равно (b − a)^{-1} ∫_a^b f(x) dx.
LaTeX
$$$$\text{ave}_{[a,b]}(f) = (b-a)^{-1} \int_a^b f(x)\,dx.$$$$
Lean4
theorem interval_average_eq (f : ℝ → E) (a b : ℝ) : (⨍ x in a..b, f x) = (b - a)⁻¹ • ∫ x in a..b, f x :=
by
rcases le_or_gt a b with h | h
· rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, intervalIntegral.integral_of_le h]
·
rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, intervalIntegral.integral_of_ge h.le, smul_neg,
← neg_smul, ← inv_neg, neg_sub]
