mathlib

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

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