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).

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.

def «term⨍_In_.._,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term⨍_In_.._,_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem interval_average_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ 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} [NormedAddCommGroup E] [NormedSpace ℝ 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)