interval_average_eq_div — Mathlib

English

For a real-valued function f, the interval average equals the integral over the interval divided by its length.

Русский

Для функции f: R → R среднее по интервалу равняется интегралу по интервалу, делённому на его длину.

LaTeX

$$$$\text{avg}_{[a,b]}(f) = \frac{\int_a^b f(x)\,dx}{b-a}.$$$$

Lean4

theorem interval_average_eq_div (f : ℝ → ℝ) (a b : ℝ) : (⨍ x in a..b, f x) = (∫ x in a..b, f x) / (b - a) := by
  rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]

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