mathlib3 documentation

measure_theory.integral.interval_average

Integral average over an interval #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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.

theorem interval_average_symm {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (a b : ) :
(x : ) in a..b, f x = (x : ) in b..a, f x
theorem interval_average_eq {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (f : E) (a b : ) :
(x : ) in a..b, f x = (b - a)⁻¹ (x : ) in a..b, f x
theorem interval_average_eq_div (f : ) (a b : ) :
(x : ) in a..b, f x = ( (x : ) in a..b, f x) / (b - a)