feat(measure_theory/bochner_integration): connecting the Bochner integral with the integral on ennreal-valued functions (#1790)

* shorter proof

* feat(measure_theory/bochner_integration): connecting the Bochner integral with the integral on `ennreal`

This PR proves that `∫ f = ∫ f⁺ - ∫ f⁻`, with the first integral sign being the Bochner integral of a real-valued function `f : α → ℝ`, and second and third integral sign being the integral on `ennreal`-valued functions. See `integral_eq_lintegral_max_sub_lintegral_min`.

I feel that most of the basic properties of the Bochner integral are proved. Please let me know if you think something else is needed.

* various things :

* add guides for typeclass inference;
* add `norm_cast` tags;
* prove some corollaries;
* add doc strings;
* other fixes

* Update bochner_integration.lean

* add some doc strings

* Fix doc strings

* Update bochner_integration.lean

* Update bochner_integration.lean

* fix doc strings

* Update bochner_integration.lean

* Use dot notation

* use dot notation

* Update Meas.lean

Author: Zhouhang Zhou

src/algebra/order_functions.lean

@@ -251,6 +251,29 @@ calc
 lemma max_le_add_of_nonneg {a b : α} (ha : a ≥ 0) (hb : b ≥ 0) : max a b ≤ a + b :=
 max_le_iff.2 (by split; simpa)
 
+lemma max_zero_sub_eq_self (a : α) : max a 0 - max (-a) 0 = a :=
+begin
+  rcases le_total a 0,
+  { rw [max_eq_right h, max_eq_left, zero_sub, neg_neg], { rwa [le_neg, neg_zero] } },
+  { rw [max_eq_left, max_eq_right, sub_zero], { rwa [neg_le, neg_zero] }, exact h }
+end
+
+lemma abs_max_sub_max_le_abs (a b c : α) : abs (max a c - max b c) ≤ abs (a - b) :=
+begin
+  simp only [max],
+  split_ifs,
+  { rw [sub_self, abs_zero], exact abs_nonneg _ },
+  { calc abs (c - b) = - (c - b) : abs_of_neg (sub_neg_of_lt (lt_of_not_ge h_1))
+      ... = b - c : neg_sub _ _
+      ... ≤ b - a : by { rw sub_le_sub_iff_left, exact h }
+      ... = - (a - b) : by rw neg_sub
+      ... ≤ abs (a - b) : neg_le_abs_self _ },
+  { calc abs (a - c) = a - c : abs_of_pos (sub_pos_of_lt (lt_of_not_ge h))
+      ... ≤ a - b : by { rw sub_le_sub_iff_left, exact h_1 }
+      ... ≤ abs (a - b) : le_abs_self _ },
+  { refl }
+end
+
 end decidable_linear_ordered_comm_group
 
 section decidable_linear_ordered_semiring

src/measure_theory/ae_eq_fun.lean

@@ -8,42 +8,42 @@ import measure_theory.integration
 
 /-!
 
-# ALmost everywhere equal functions
+# Almost everywhere equal functions
 
 Two measurable functions are treated as identical if they are almost everywhere equal. We form the
 set of equivalence classes under the relation of being almost everywhere equal, which is sometimes
-known as the L0 space.
+known as the `L⁰` space.
 
-See `l1_space.lean` for L1 space.
+See `l1_space.lean` for `L¹` space.
 
 
 ## Notation
 
-* `α →ₘ β` is the type of L0 space, where `α` is a measure space and `β` is a measurable space.
-  `f : α →ₘ β` is a "function" in L0. In comments, `[f]` is also used to denote an L0 function.
+* `α →ₘ β` is the type of `L⁰` space, where `α` is a measure space and `β` is a measurable space.
+  `f : α →ₘ β` is a "function" in `L⁰`. In comments, `[f]` is also used to denote an `L⁰` function.
 
   `ₘ` can be typed as `\_m`. Sometimes it is shown as a box if font is missing.
 
 
 ## Main statements
 
-* The linear structure of L0 :
-    Addition and scalar multiplication are defined on L0 in the natural way, i.e.,
+* The linear structure of `L⁰` :
+    Addition and scalar multiplication are defined on `L⁰` in the natural way, i.e.,
     `[f] + [g] := [f + g]`, `c • [f] := [c • f]`. So defined, `α →ₘ β` inherits the linear structure
     of `β`. For example, if `β` is a module, then `α →ₘ β` is a module over the same ring.
 
     See `mk_add_mk`,  `neg_mk`,     `mk_sub_mk`,  `smul_mk`,
         `add_to_fun`, `neg_to_fun`, `sub_to_fun`, `smul_to_fun`
 
-* The order structure of L0 :
+* The order structure of `L⁰` :
     `≤` can be defined in a similar way: `[f] ≤ [g]` if `f a ≤ g a` for almost all `a` in domain.
     And `α →ₘ β` inherits the preorder and partial order of `β`.
 
-    TODO: Define `sup` and `inf` on L0 so that it forms a lattice. It seems that `β` must be a
+    TODO: Define `sup` and `inf` on `L⁰` so that it forms a lattice. It seems that `β` must be a
     linear order, since otherwise `f ⊔ g` may not be a measurable function.
 
-* Emetric on L0 :
-    If `β` is an `emetric_space`, then L0 can be made into an `emetric_space`, where
+* Emetric on `L⁰` :
+    If `β` is an `emetric_space`, then `L⁰` can be made into an `emetric_space`, where
     `edist [f] [g]` is defined to be `∫⁻ a, edist (f a) (g a)`.
 
     The integral used here is `lintegral : (α → ennreal) → ennreal`, which is defined in the file
@@ -54,24 +54,22 @@ See `l1_space.lean` for L1 space.
 
 ## Implementation notes
 
-`f.to_fun`     : To find a representative of `f : α →ₘ β`, use `f.to_fun`.
-                 For each operation `op` in L0, there is a lemma called `op_to_fun`, characterizing,
+* `f.to_fun`     : To find a representative of `f : α →ₘ β`, use `f.to_fun`.
+                 For each operation `op` in `L⁰`, there is a lemma called `op_to_fun`, characterizing,
                  say, `(f op g).to_fun`.
-
-`ae_eq_fun.mk` : To constructs an L0 function `α →ₘ β` from a measurable function `f : α → β`,
+* `ae_eq_fun.mk` : To constructs an `L⁰` function `α →ₘ β` from a measurable function `f : α → β`,
                  use `ae_eq_fun.mk`
-
-`comp`         : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ`
-
-`comp₂`        : Use `comp₂ g f₁ f₂ to get `[λa, g (f₁ a) (f₂ a)]`.
+* `comp`         : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ`
+* `comp₂`        : Use `comp₂ g f₁ f₂ to get `[λa, g (f₁ a) (f₂ a)]`.
                  For example, `[f + g]` is `comp₂ (+)`
 
 
 ## Tags
 
-function space, almost everywhere equal, L0, ae_eq_fun
+function space, almost everywhere equal, `L⁰`, ae_eq_fun
 
 -/
+
 noncomputable theory
 open_locale classical
 
@@ -162,7 +160,7 @@ def comp₂ {γ δ : Type*} [measurable_space γ] [measurable_space δ]
   (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) : α →ₘ δ :=
 begin
   refine quotient.lift_on₂ f₁ f₂ (λf₁ f₂, mk (λa, g (f₁.1 a) (f₂.1 a)) $ _) _,
-  { exact measurable.comp hg (measurable_prod_mk f₁.2 f₂.2) },
+  { exact measurable.comp hg (measurable.prod_mk f₁.2 f₂.2) },
   { rintros ⟨f₁, hf₁⟩ ⟨f₂, hf₂⟩ ⟨g₁, hg₁⟩ ⟨g₂, hg₂⟩ h₁ h₂,
     refine quotient.sound _,
     filter_upwards [h₁, h₂],
@@ -172,13 +170,13 @@ end
 @[simp] lemma comp₂_mk_mk {γ δ : Type*} [measurable_space γ] [measurable_space δ]
   (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α → β) (f₂ : α → γ) (hf₁ hf₂) :
   comp₂ g hg (mk f₁ hf₁) (mk f₂ hf₂) =
-    mk (λa, g (f₁ a) (f₂ a)) (measurable.comp hg (measurable_prod_mk hf₁ hf₂)) :=
+    mk (λa, g (f₁ a) (f₂ a)) (measurable.comp hg (measurable.prod_mk hf₁ hf₂)) :=
 rfl
 
 lemma comp₂_eq_mk_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ]
   (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) :
   comp₂ g hg f₁ f₂ = mk (λa, g (f₁.to_fun a) (f₂.to_fun a))
-    (hg.comp (measurable_prod_mk f₁.measurable f₂.measurable)) :=
+    (hg.comp (measurable.prod_mk f₁.measurable f₂.measurable)) :=
 by conv_lhs { rw [self_eq_mk f₁, self_eq_mk f₂, comp₂_mk_mk] }
 
 lemma comp₂_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ]
@@ -199,8 +197,8 @@ end
     `(f a, g a)` for almost all `a` -/
 def lift_rel {γ : Type*} [measurable_space γ] (r : β → γ → Prop) (f : α →ₘ β) (g : α →ₘ γ) : Prop :=
 lift_pred (λp:β×γ, r p.1 p.2)
-  (comp₂ prod.mk (measurable_prod_mk
-    (measurable_fst measurable_id) (measurable_snd measurable_id)) f g)
+  (comp₂ prod.mk (measurable.prod_mk
+    (measurable.fst measurable_id) (measurable.snd measurable_id)) f g)
 
 lemma lift_rel_mk_mk {γ : Type*} [measurable_space γ] (r : β → γ → Prop)
   (f : α → β) (g : α → γ) (hf hg) : lift_rel r (mk f hf) (mk g hg) ↔ ∀ₘ a, r (f a) (g a) :=
@@ -236,7 +234,7 @@ instance [partial_order β] : partial_order (α →ₘ β) :=
   end,
   .. ae_eq_fun.preorder }
 
-/- TODO: Prove L0 space is a lattice if β is linear order.
+/- TODO: Prove `L⁰` space is a lattice if β is linear order.
          What if β is only a lattice? -/
 
 -- instance [linear_order β] : semilattice_sup (α →ₘ β) :=
@@ -266,12 +264,12 @@ variables {γ : Type*}
   [topological_space γ] [second_countable_topology γ] [add_monoid γ] [topological_add_monoid γ]
 
 protected def add : (α →ₘ γ) → (α →ₘ γ) → (α →ₘ γ) :=
-comp₂ (+) (measurable_add (measurable_fst measurable_id) (measurable_snd  measurable_id))
+comp₂ (+) (measurable.add (measurable.fst measurable_id) (measurable.snd  measurable_id))
 
 instance : has_add (α →ₘ γ) := ⟨ae_eq_fun.add⟩
 
 @[simp] lemma mk_add_mk (f g : α → γ) (hf hg) :
-   (mk f hf) + (mk g hg) = mk (f + g) (measurable_add hf hg) := rfl
+   (mk f hf) + (mk g hg) = mk (f + g) (measurable.add hf hg) := rfl
 
 lemma add_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f + g).to_fun a = f.to_fun a + g.to_fun a :=
 comp₂_to_fun _ _ _ _
@@ -300,11 +298,11 @@ section add_group
 
 variables {γ : Type*} [topological_space γ] [add_group γ] [topological_add_group γ]
 
-protected def neg : (α →ₘ γ) → (α →ₘ γ) := comp has_neg.neg (measurable_neg measurable_id)
+protected def neg : (α →ₘ γ) → (α →ₘ γ) := comp has_neg.neg (measurable.neg measurable_id)
 
 instance : has_neg (α →ₘ γ) := ⟨ae_eq_fun.neg⟩
 
-@[simp] lemma neg_mk (f : α → γ) (hf) : -(mk f hf) = mk (-f) (measurable_neg hf) := rfl
+@[simp] lemma neg_mk (f : α → γ) (hf) : -(mk f hf) = mk (-f) (measurable.neg hf) := rfl
 
 lemma neg_to_fun (f : α →ₘ γ) : ∀ₘ a, (-f).to_fun a = - f.to_fun a := comp_to_fun _ _ _
 
@@ -316,7 +314,7 @@ instance : add_group (α →ₘ γ) :=
  }
 
 @[simp] lemma mk_sub_mk (f g : α → γ) (hf hg) :
-   (mk f hf) - (mk g hg) = mk (λa, (f a) - (g a)) (measurable_sub hf hg) := rfl
+   (mk f hf) - (mk g hg) = mk (λa, (f a) - (g a)) (measurable.sub hf hg) := rfl
 
 lemma sub_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f - g).to_fun a = f.to_fun a - g.to_fun a :=
 begin
@@ -403,8 +401,8 @@ instance : vector_space 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule }
 
 end vector_space
 
-/- TODO : Prove that L0 is a complete space if the codomain is complete. -/
-/- TODO : Multiplicative structure of L0 if useful -/
+/- TODO : Prove that `L⁰` is a complete space if the codomain is complete. -/
+/- TODO : Multiplicative structure of `L⁰` if useful -/
 
 open ennreal
 
@@ -541,6 +539,26 @@ end
 
 end normed_space
 
+section pos_part
+
+variables {γ : Type*} [topological_space γ] [decidable_linear_order γ] [ordered_topology γ]
+  [second_countable_topology γ] [has_zero γ]
+
+/-- Positive part of an `ae_eq_fun`. -/
+def pos_part (f : α →ₘ γ) : α →ₘ γ :=
+comp₂ max (measurable.max (measurable.fst measurable_id) (measurable.snd measurable_id)) f 0
+
+lemma pos_part_to_fun (f : α →ₘ γ) : ∀ₘ a, (pos_part f).to_fun a = max (f.to_fun a) (0:γ) :=
+begin
+  filter_upwards [comp₂_to_fun max (measurable.max (measurable.fst measurable_id)
+    (measurable.snd measurable_id)) f 0, @ae_eq_fun.zero_to_fun α γ],
+  simp only [mem_set_of_eq],
+  assume a h₁ h₂,
+  rw [pos_part, h₁, h₂]
+end
+
+end pos_part
+
 end ae_eq_fun
 
 end measure_theory