Commit 2020-09-18 21:57 0269a76e

feat(integration): integral commutes with continuous linear maps (#4167) from the sphere eversion project. Main result:

continuous_linear_map.integral_apply_comm {α : Type*} [measurable_space α] {μ : measure α} 
  {E : Type*} [normed_group E]  [second_countable_topology E] [normed_space ℝ E] [complete_space E]
  [measurable_space E] [borel_space E] {F : Type*} [normed_group F]
  [second_countable_topology F] [normed_space ℝ F] [complete_space F]
  [measurable_space F] [borel_space F] 
  {φ : α → E} (L : E →L[ℝ] F) (φ_meas : measurable φ) (φ_int : integrable φ μ) :
  ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ)