E Lp Norm pi le sum component

theorem eLpNorm_pi_le_sum_component    {p : ℝ≥0∞} (hp1 : 1 ≤ p)    {F : α → (Fin d → ℝ)}    (hF_comp_aesm : ∀ i : Fin d, AEStronglyMeasurable (fun x => F x i) μ) :    eLpNorm F p μ ≤ ∑ i : Fin d, eLpNorm (fun x => F x i) p μ := by  calc eLpNorm F p μ      ≤ eLpNorm (fun x => ∑ i : Fin d, ‖F x i‖) p μ :=        eLpNorm_mono_real fun x => pi_norm_le_sum_norms (F x)    _ ≤ ∑ i : Fin d, eLpNorm (fun x => ‖F x i‖) p μ := by        let g : Fin d → α → ℝ := fun i x => ‖F x i‖        have hg_aesm : ∀ i : Fin d, AEStronglyMeasurable (g i) μ :=          fun i => (hF_comp_aesm i).norm        suffices h : ∀ (s : Finset (Fin d)),            eLpNorm (∑ i ∈ s, g i) p μ ≤ ∑ i ∈ s, eLpNorm (g i) p μ by          have hg_eq : (fun x => ∑ i : Fin d, ‖F x i‖) = ∑ i : Fin d, g i := by            ext x; simp [g, Finset.sum_apply]          rw [hg_eq]; simp only [g]; exact h Finset.univ        intro s        induction s using Finset.cons_induction with        | empty => simp [eLpNorm_zero]        | cons a s has ih =>          rw [Finset.sum_cons, Finset.sum_cons]          calc eLpNorm (g a + ∑ i ∈ s, g i) p μ              ≤ eLpNorm (g a) p μ + eLpNorm (∑ i ∈ s, g i) p μ :=                eLpNorm_add_le (hg_aesm a)                  (Finset.aestronglyMeasurable_sum s fun i _ => hg_aesm i) hp1            _ ≤ eLpNorm (g a) p μ + ∑ i ∈ s, eLpNorm (g i) p μ := by gcongr    _ = ∑ i : Fin d, eLpNorm (fun x => F x i) p μ := by        congr 1; ext i; exact eLpNorm_norm _