feat(measure_theory/integral): add formulas for average over an inter…

…val (#14132)

src/measure_theory/integral/interval_average.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import analysis.convex.integral
+import measure_theory.integral.interval_integral
+
+/-!
+# 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.
+
+-/
+
+open measure_theory set topological_space
+open_locale interval
+
+variables {E : Type*} [normed_group E] [normed_space ℝ E] [complete_space E]
+
+notation `⨍` binders ` in ` a `..` b `, `
+  r:(scoped:60 f, average (measure.restrict volume (Ι a b)) f) := r
+
+lemma interval_average_symm (f : ℝ → E) (a b : ℝ) : ⨍ x in a..b, f x = ⨍ x in b..a, f x :=
+by rw [set_average_eq, set_average_eq, interval_oc_swap]
+
+lemma interval_average_eq (f : ℝ → E) (a b : ℝ) : ⨍ x in a..b, f x = (b - a)⁻¹ • ∫ x in a..b, f x :=
+begin
+  cases le_or_lt a b with h h,
+  { rw [set_average_eq, interval_oc_of_le h, real.volume_Ioc, interval_integral.integral_of_le h,
+      ennreal.to_real_of_real (sub_nonneg.2 h)] },
+  { rw [set_average_eq, interval_oc_of_lt h, real.volume_Ioc, interval_integral.integral_of_ge h.le,
+     ennreal.to_real_of_real (sub_nonneg.2 h.le), smul_neg, ← neg_smul, ← inv_neg, neg_sub] }
+end
+
+lemma 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]