Commit 2019-12-12 09:05 69e861e9

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