Commit 2019-12-01 17:32 177ccedb

feat(measure/bochner_integration): dominated convergence theorem (#1757)

• feat(measure/bochner_integration): dominated convergence theorem This PR
• proves the dominated convergence theorem
• and some other lemmas including integral_congr_ae, norm_integral_le_lintegral_norm.
• adds several equivalent definitions of the predicate integrable and shortens some proofs.
• fix linting error
• Add some section doc strings
• Indentation is very wrong
• Remove useless assumptions; fix doc strings
• remove private; add a doc string for Lebesgue's dominated convergence theorem
• Update basic.lean