Continuous linear maps composed with integration

The goal of this file is to prove that integration commutes with continuous linear maps. This holds for simple functions. The general result follows from the continuity of all involved operations on the space L¹. Note that composition by a continuous linear map on L¹ is not just the composition, as we are dealing with classes of functions, but it has already been defined as ContinuousLinearMap.compLp. We take advantage of this construction here.

theorem ContinuousLinearMap.integral_compLp {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [NormedSpace ℝ F] (L : E →L[𝕜] F) (φ : ↥(MeasureTheory.Lp E p μ)) : ∫ (x : X), ↑↑(L.compLp φ) x ∂μ = ∫ (x : X), L (↑↑φ x) ∂μ

theorem ContinuousLinearMap.setIntegral_compLp {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [NormedSpace ℝ F] (L : E →L[𝕜] F) (φ : ↥(MeasureTheory.Lp E p μ)) {s : Set X} (hs : MeasurableSet s) : ∫ (x : X) in s, ↑↑(L.compLp φ) x ∂μ = ∫ (x : X) in s, L (↑↑φ x) ∂μ

theorem ContinuousLinearMap.continuous_integral_comp_L1 {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] (L : E →L[𝕜] F) : Continuous fun (φ : ↥(MeasureTheory.Lp E 1 μ)) => ∫ (x : X), L (↑↑φ x) ∂μ

theorem ContinuousLinearMap.integral_comp_comm {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ E] [CompleteSpace E] (L : E →L[𝕜] F) {φ : X → E} (φ_int : MeasureTheory.Integrable φ μ) : ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

theorem ContinuousLinearMap.integral_apply {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : X → H →L[𝕜] E} (φ_int : MeasureTheory.Integrable φ μ) (v : H) : (∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ

theorem ContinuousMultilinearMap.integral_apply {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] {ι : Type u_6} [Fintype ι] {M : ι → Type u_7} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {φ : X → ContinuousMultilinearMap 𝕜 M E} (φ_int : MeasureTheory.Integrable φ μ) (m : (i : ι) → M i) : (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

theorem ContinuousLinearMap.integral_comp_comm' {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ E] [CompleteSpace E] (L : E →L[𝕜] F) {K : NNReal} (hL : AntilipschitzWith K ⇑L) (φ : X → E) : ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

theorem ContinuousLinearMap.integral_comp_L1_comm {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ E] [CompleteSpace E] (L : E →L[𝕜] F) (φ : ↥(MeasureTheory.Lp E 1 μ)) : ∫ (x : X), L (↑↑φ x) ∂μ = L (∫ (x : X), ↑↑φ x ∂μ)

theorem LinearIsometry.integral_comp_comm {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [NormedSpace ℝ F] [CompleteSpace E] [NormedSpace ℝ E] (L : E →ₗᵢ[𝕜] F) (φ : X → E) : ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

theorem ContinuousLinearEquiv.integral_comp_comm {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [NormedSpace ℝ E] (L : E ≃L[𝕜] F) (φ : X → E) : ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

theorem ContinuousMap.integral_apply {X : Type u_1} {Y : Type u_2} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [TopologicalSpace Y] [CompactSpace Y] [NormedSpace ℝ E] [CompleteSpace E] {f : X → C(Y, E)} (hf : MeasureTheory.Integrable f μ) (y : Y) : (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

theorem ContinuousMapZero.integral_apply {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] [CompactSpace Y] {R : Type u_6} [NormedCommRing R] [Zero Y] [NormedAlgebra ℝ R] [CompleteSpace R] {f : X → ContinuousMapZero Y R} (hf : MeasureTheory.Integrable f μ) (y : Y) : (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

theorem integral_ofReal {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {f : X → ℝ} : ∫ (x : X), ↑(f x) ∂μ = ↑(∫ (x : X), f x ∂μ)

theorem integral_complex_ofReal {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {f : X → ℝ} : ∫ (x : X), ↑(f x) ∂μ = ↑(∫ (x : X), f x ∂μ)

theorem integral_re {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {f : X → 𝕜} (hf : MeasureTheory.Integrable f μ) : ∫ (x : X), RCLike.re (f x) ∂μ = RCLike.re (∫ (x : X), f x ∂μ)

theorem integral_im {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {f : X → 𝕜} (hf : MeasureTheory.Integrable f μ) : ∫ (x : X), RCLike.im (f x) ∂μ = RCLike.im (∫ (x : X), f x ∂μ)

theorem integral_conj {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {f : X → 𝕜} : ∫ (x : X), (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : X), f x ∂μ)

theorem integral_coe_re_add_coe_im {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {f : X → 𝕜} (hf : MeasureTheory.Integrable f μ) : ∫ (x : X), ↑(RCLike.re (f x)) ∂μ + (∫ (x : X), ↑(RCLike.im (f x)) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ

theorem integral_re_add_im {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {f : X → 𝕜} (hf : MeasureTheory.Integrable f μ) : ↑(∫ (x : X), RCLike.re (f x) ∂μ) + ↑(∫ (x : X), RCLike.im (f x) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ

theorem setIntegral_re_add_im {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {f : X → 𝕜} {i : Set X} (hf : MeasureTheory.IntegrableOn f i μ) : ↑(∫ (x : X) in i, RCLike.re (f x) ∂μ) + ↑(∫ (x : X) in i, RCLike.im (f x) ∂μ) * RCLike.I = ∫ (x : X) in i, f x ∂μ

theorem swap_integral {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (f : X → E × F) : (∫ (x : X), f x ∂μ).swap = ∫ (x : X), (f x).swap ∂μ

theorem fst_integral {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace F] {f : X → E × F} (hf : MeasureTheory.Integrable f μ) : (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

theorem snd_integral {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace E] {f : X → E × F} (hf : MeasureTheory.Integrable f μ) : (∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ

theorem integral_pair {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] {f : X → E} {g : X → F} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : ∫ (x : X), (f x, g x) ∂μ = (∫ (x : X), f x ∂μ, ∫ (x : X), g x ∂μ)

theorem integral_smul_const {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_6} [RCLike 𝕜] [NormedSpace 𝕜 E] [CompleteSpace E] (f : X → 𝕜) (c : E) : ∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c

theorem integral_withDensity_eq_integral_smul {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → NNReal} (f_meas : Measurable f) (g : X → E) : (∫ (x : X), g x ∂μ.withDensity fun (x : X) => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

theorem integral_withDensity_eq_integral_smul₀ {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → NNReal} (hf : AEMeasurable f μ) (g : X → E) : (∫ (x : X), g x ∂μ.withDensity fun (x : X) => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

theorem integral_withDensity_eq_integral_toReal_smul₀ {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → ENNReal} (f_meas : AEMeasurable f μ) (hf_lt_top : ∀ᵐ (x : X) ∂μ, f x < ⊤) (g : X → E) : ∫ (x : X), g x ∂μ.withDensity f = ∫ (x : X), (f x).toReal • g x ∂μ

theorem integral_withDensity_eq_integral_toReal_smul {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → ENNReal} (f_meas : Measurable f) (hf_lt_top : ∀ᵐ (x : X) ∂μ, f x < ⊤) (g : X → E) : ∫ (x : X), g x ∂μ.withDensity f = ∫ (x : X), (f x).toReal • g x ∂μ

theorem setIntegral_withDensity_eq_setIntegral_smul₀ {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → NNReal} {s : Set X} (hf : AEMeasurable f (μ.restrict s)) (g : X → E) (hs : MeasurableSet s) : (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

theorem setIntegral_withDensity_eq_setIntegral_toReal_smul₀ {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → ENNReal} {s : Set X} (hf : AEMeasurable f (μ.restrict s)) (hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) (g : X → E) (hs : MeasurableSet s) : (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) => f x) = ∫ (x : X) in s, (f x).toReal • g x ∂μ

theorem setIntegral_withDensity_eq_setIntegral_smul {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → NNReal} (f_meas : Measurable f) (g : X → E) {s : Set X} (hs : MeasurableSet s) : (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

theorem setIntegral_withDensity_eq_setIntegral_toReal_smul {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → ENNReal} {s : Set X} (hf : Measurable f) (hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) (g : X → E) (hs : MeasurableSet s) : (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) => f x) = ∫ (x : X) in s, (f x).toReal • g x ∂μ

theorem setIntegral_withDensity_eq_setIntegral_smul₀' {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : X → NNReal} (s : Set X) (hf : AEMeasurable f (μ.restrict s)) (g : X → E) : (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

theorem setIntegral_withDensity_eq_setIntegral_toReal_smul₀' {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : X → ENNReal} (s : Set X) (hf : AEMeasurable f (μ.restrict s)) (hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) (g : X → E) : ∫ (x : X) in s, g x ∂μ.withDensity f = ∫ (x : X) in s, (f x).toReal • g x ∂μ

theorem setIntegral_withDensity_eq_setIntegral_toReal_smul' {X : Type u_1} {E : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : X → ENNReal} (s : Set X) (hf : Measurable f) (hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) (g : X → E) : ∫ (x : X) in s, g x ∂μ.withDensity f = ∫ (x : X) in s, (f x).toReal • g x ∂μ