mathlib3

0269a76e - feat(integration): integral commutes with continuous linear maps (#4167)

feat(integration): integral commutes with continuous linear maps (#4167) from the sphere eversion project. Main result: ```lean 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 ∂μ) ```