Integral tendsto of Lploc tendsto

lemma integral_tendsto_of_Lploc_tendsto    {U : Set (Fin d → ℝ)}    {p : ℝ≥0∞}    {ψ : (Fin d → ℝ) → ℝ}    {f : ℕ → (Fin d → ℝ) → ℝ}    {g : (Fin d → ℝ) → ℝ}    (hp : 1 ≤ p)    (hf : ∀ i, MemLp (f i) p (μU d U))    (hg : MemLp g p (μU d U))    (hψ : ψ ∈ Cc_inftyU d U)    (hconv : Tendsto (fun i => eLpNorm (fun x => f i x - g x) p (μU d U))            atTop (𝓝 0))    : Tendsto (fun i => ∫ x, f i x * ψ x ∂μU d U) atTop (𝓝 (∫ x, g x * ψ x ∂μU d U))    := by     let q : ℝ≥0∞ := ENNReal.conjExponent p    haveI : Fact (1 ≤ p) := ⟨hp⟩    have hpq : p.HolderConjugate q := inferInstance    letI : p.HolderTriple q 1 := hpq     have hψ_Lq : MemLp ψ q (μU d U) := by      haveI : IsFiniteMeasureOnCompacts (μU d U) := by        unfold μU; infer_instance      exact (hψ.2.2.continuous).memLp_of_hasCompactSupport hψ.1     have hInt_g : Integrable (fun x => g x * ψ x) (μU d U) := by      simpa [Pi.mul_apply] using MemLp.integrable_mul hg hψ_Lq     have hfg : ∀ i, MemLp (fun x => f i x - g x) p (μU d U)      := fun i => (hf i).sub hg     have hInt_diff : ∀ i, Integrable (fun x => (f i x - g x) * ψ x) (μU d U) := by      intro i      simpa [Pi.mul_apply] using MemLp.integrable_mul (hfg i) hψ_Lq     have hstep2 : Tendsto (fun i => ∫ x, (f i x - g x) * ψ x ∂μU d U) atTop (𝓝 0) := by      set C := eLpNorm ψ q (μU d U)      have hC_fin : C ≠ ⊤ := hψ_Lq.eLpNorm_lt_top.ne       have hHolder : ∀ i, ‖∫ x, (f i x - g x) * ψ x ∂μU d U‖ ≤        (eLpNorm (fun x => f i x - g x) p (μU d U) * C).toReal := fun i => by        have h1 : ‖∫ x, (f i x - g x) * ψ x ∂μU d U‖ ≤                  ∫ x, ‖f i x - g x‖ * ‖ψ x‖ ∂μU d U :=          (norm_integral_le_integral_norm _).trans (le_of_eq (by congr 1; ext x; exact norm_mul _ _))        have h2 : ∫ x, ‖f i x - g x‖ * ‖ψ x‖ ∂μU d U ≤                (eLpNorm (fun x => f i x - g x) p (μU d U) * C).toReal := by              simp_rw [← norm_mul]              have h_int := hInt_diff i              calc ∫ x, ‖(f i x - g x) * ψ x‖ ∂μU d U                  = (eLpNorm (fun x => (f i x - g x) * ψ x) 1 (μU d U)).toReal := by                      rw [eLpNorm_one_eq_lintegral_enorm]                      exact (integral_norm_eq_lintegral_enorm h_int.aestronglyMeasurable)                _ ≤ (eLpNorm (fun x => f i x - g x) p (μU d U) * C).toReal := by                      have hR_ne_top :                          eLpNorm (fun x => f i x - g x) p (μU d U) * C ≠ ⊤ := by                        exact ENNReal.mul_ne_top (hfg i).eLpNorm_lt_top.ne hC_fin                      exact                        (ENNReal.toReal_le_toReal                          (memLp_one_iff_integrable.mpr h_int).eLpNorm_lt_top.ne                          hR_ne_top).mpr                          (by                            simpa [C, smul_eq_mul, mul_comm, mul_left_comm, mul_assoc] using                              (MeasureTheory.eLpNorm_smul_le_mul_eLpNorm                                (μ := μU d U)                                (p := p) (q := q) (r := 1)                                (f := ψ)                                hψ_Lq.aestronglyMeasurable                                (hfg i).aestronglyMeasurable))        exact h1.trans h2      exact squeeze_zero_norm hHolder (by        simp_rw [ENNReal.toReal_mul]        simpa using ((ENNReal.tendsto_toReal zero_ne_top).comp hconv).mul_const C.toReal)     have heq : ∀ i, ∫ x, f i x * ψ x ∂μU d U =        ∫ x, (f i x - g x) * ψ x ∂μU d U + ∫ x, g x * ψ x ∂μU d U := fun i => by      rw [← integral_add (hInt_diff i) hInt_g]      congr 1; ext x; ring    simp_rw [heq]    simpa using hstep2.add tendsto_const_nhds