Tendsto e Lp Norm pi component

theorem tendsto_eLpNorm_pi_component    {p : ℝ≥0∞}    {G : ℕ → α → (Fin d → ℝ)} {Gext : α → (Fin d → ℝ)}    (hG_tendsto : Tendsto (fun n => eLpNorm (fun x => G n x - Gext x) p μ) atTop (nhds 0))    (i : Fin d) :    Tendsto (fun n => eLpNorm (fun x => G n x i - Gext x i) p μ) atTop (nhds 0) := by  -- Key: (fun x => G n x i - Gext x i) = (fun x => (G n x - Gext x) i)  -- This is definitionally true for Fin d → ℝ (Pi subtraction), but we make it  -- explicit to avoid expensive defeq checks inside tendsto_of_tendsto.  have hle : ∀ n, eLpNorm (fun x => G n x i - Gext x i) p μ ≤      eLpNorm (fun x => G n x - Gext x) p μ := by    intro n    -- Rewrite LHS to match eLpNorm_pi_component_le's input    show eLpNorm (fun x => (G n - Gext) x i) p μ ≤ _    exact eLpNorm_pi_component_le i  exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hG_tendsto    (fun _ => bot_le) hle