Integral average over an interval #
In this file we introduce notation ⨍ x in a..b, f x
for the average ⨍ x in Ι a b, f x
of f
over the interval Ι a b = Set.Ioc (min a b) (max a b)
w.r.t. the Lebesgue measure, then prove
formulas for this average:
interval_average_eq
:⨍ x in a..b, f x = (b - a)⁻¹ • ∫ x in a..b, f x
;interval_average_eq_div
:⨍ x in a..b, f x = (∫ x in a..b, f x) / (b - a)
;exists_eq_interval_average
:∃ c, f c = ⨍ (x : ℝ) in a..b, f x
.
We also prove that ⨍ x in a..b, f x = ⨍ x in b..a, f x
, see interval_average_symm
.
Notation #
⨍ x in a..b, f x
: average of f
over the interval Ι a b
w.r.t. the Lebesgue measure.
⨍ x in a..b, f x
is the average of f
over the interval `Ι a w.r.t. the Lebesgue measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
exists_eq_interval_average
{f : ℝ → ℝ}
{a b : ℝ}
(hab : a ≠ b)
(hf : ContinuousOn f (Set.uIcc a b))
:
The mean value theorem for integrals: There exists a point in an interval such that the mean of a continuous function over the interval equals the value of the function at the point.