Refactor integrals

[urkud]

Goal

Refactor measure_theory library so that

• (almost?) all theorems about measures apply to any measure, with volume being a particular case;
• (almost?) all theorems about integrals apply to an integral of a function over a set w.r.t. a measure.

Why

With this setup we won't need to prove the same theorem several times.

How

Measure

Thanks to improved handling of coe_fn in recent community versions of Lean, we can redefine volume to be a bundled measure instead of a function. Then we can restate all theorems in measure_theory/measure_space in terms of a measure and apply them to any measure (volume or not) in a uniform way. In particular, rw will lead to a proof state with volume, not measure_space.μ. This is done in #3075.

Integrals

The text below deals with functions f : α → ennreal and lintegral. Similar changes are planned for the Bochner integral.

The design below is based on algebra.big_operators.
The main definition for integrals will be

def lintegral (μ : measure α) (s : set α) (f : α → ennreal) : ennreal := sorry

There will be no special case definitions for integrals over univ / w.r.t. volume. Instead we will use notation, see the following example.

import measure_theory.measure_space

variables {α : Type*} {β : Type*} [measurable_space α]
noncomputable theory

namespace measure_theory

variables [measure_space β] (s : set α) (t : set β)

def lintegral (μ : measure α) (s : set α) (f : α → ennreal) : ennreal := 0

notation `∫⁻` binders ` ∂ ` μ ` in ` s `, ` r:(scoped f, lintegral μ s f) := r
notation `∫⁻` binders ` in ` s ` ∂ ` μ `, ` r:(scoped f, lintegral μ s f) := r
notation `∫⁻` binders ` in ` s `, ` r:(scoped f, lintegral volume s f) := r
notation `∫⁻` binders ` ∂ ` μ `, ` r:(scoped f, lintegral μ set.univ f) := r
notation `∫⁻` binders `, ` r:(scoped f, lintegral volume set.univ f) := r

variables (μ : measure α)

#check ∫⁻ (x : β), 0
#check ∫⁻ (x : β) ∂ volume, 0
#check ∫⁻ (x : α) ∂ μ, 0
#check ∫⁻ (x : α) ∂ μ, 0
#check ∫⁻ x ∂ μ, 0
#check ∫⁻ x in t, 1
#check ∫⁻ x in s ∂ μ, 2
#check ∫⁻ x in t ∂ volume, 1
#check ∫⁻ (x : β) in set.univ ∂ volume, 1

end measure_theory