Has Weak Partial Deriv of e Lp Norm Approx p

theorem HasWeakPartialDeriv.of_eLpNormApprox_p    {Ω : Set E} (hΩ : IsOpen Ω)    {p : ℝ} (hp : 1 < p)    {i : Fin d} {f g : E → ℝ} {ψ : ℕ → E → ℝ} {gψ : ℕ → E → ℝ}    (hf_memLp : MemLp f (ENNReal.ofReal p) (volume.restrict Ω))    (hg_memLp : MemLp g (ENNReal.ofReal p) (volume.restrict Ω))    (hψ_wd : ∀ n, HasWeakPartialDeriv i (gψ n) (ψ n) Ω)    (hψ_fun_memLp : ∀ n, MemLp (fun x => ψ n x - f x) (ENNReal.ofReal p) (volume.restrict Ω))    (hψ_fun :      Tendsto (fun n => eLpNorm (fun x => ψ n x - f x) (ENNReal.ofReal p) (volume.restrict Ω))        atTop (nhds 0))    (hψ_grad_memLp : ∀ n, MemLp (fun x => gψ n x - g x) (ENNReal.ofReal p) (volume.restrict Ω))    (hψ_grad :      Tendsto (fun n => eLpNorm (fun x => gψ n x - g x) (ENNReal.ofReal p) (volume.restrict Ω))        atTop (nhds 0)) :    HasWeakPartialDeriv i g f Ω := by  let _ := hΩ  intro φ hφ hφ_supp hφ_sub  let μ : Measure E := volume.restrict Ω  let dφ : E → ℝ := fun x => (fderiv ℝ φ x) (EuclideanSpace.single i 1)  let q : ℝ := Real.conjExponent p  have hpqR : p.HolderConjugate q := Real.HolderConjugate.conjExponent hp  have hpq : p⁻¹ + q⁻¹ = 1 := (Real.holderConjugate_iff.mp hpqR).2  have hq : 1 < q := (Real.holderConjugate_iff.mp hpqR.symm).1  letI : (ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) 1 :=    ENNReal.HolderConjugate.of_toReal <| by      simpa [ENNReal.toReal_ofReal (by linarith : 0 ≤ p),        ENNReal.toReal_ofReal (by linarith : 0 ≤ q)] using hpqR  have hdφ_memLp : MemLp dφ (ENNReal.ofReal q) μ := by    have hcont : Continuous dφ := by      simpa [dφ] using        ((hφ.continuous_fderiv (by simp : ((⊤ : ℕ∞) : WithTop ℕ∞) ≠ 0)).clm_apply          continuous_const)    have hcpt : HasCompactSupport dφ := by      simpa [dφ] using hφ_supp.fderiv_apply (𝕜 := ℝ) (EuclideanSpace.single i 1)    exact (hcont.memLp_of_hasCompactSupport hcpt).restrict _  have hφ_memLp : MemLp φ (ENNReal.ofReal q) μ :=    (hφ.continuous.memLp_of_hasCompactSupport hφ_supp).restrict _  have h_fun_int :      Tendsto (fun n => ∫ x, dφ x * (ψ n x - f x) ∂μ) atTop (nhds 0) :=    tendsto_integral_mul_of_eLpNorm_tendsto_zero_p hpq hp hq hdφ_memLp hψ_fun_memLp hψ_fun  have h_grad_int :      Tendsto (fun n => ∫ x, φ x * (gψ n x - g x) ∂μ) atTop (nhds 0) :=    tendsto_integral_mul_of_eLpNorm_tendsto_zero_p hpq hp hq hφ_memLp hψ_grad_memLp hψ_grad  have h_lhs_tendsto :      Tendsto (fun n => ∫ x in Ω, ψ n x * dφ x)        atTop (nhds (∫ x in Ω, f x * dφ x)) := by    have h_eq :        (fun n => ∫ x in Ω, ψ n x * dφ x) =          fun n => (∫ x in Ω, f x * dφ x) + ∫ x, dφ x * (ψ n x - f x) ∂μ := by      funext n      have hfi : Integrable (fun x => f x * dφ x) μ := by        simpa [mul_comm] using hdφ_memLp.integrable_mul hf_memLp      have hdi : Integrable (fun x => dφ x * (ψ n x - f x)) μ :=        hdφ_memLp.integrable_mul (hψ_fun_memLp n)      calc        ∫ x in Ω, ψ n x * dφ x            = ∫ x, (f x * dφ x) + dφ x * (ψ n x - f x) ∂μ := by                congr with x                ring        _ = (∫ x, f x * dφ x ∂μ) + ∫ x, dφ x * (ψ n x - f x) ∂μ :=              integral_add hfi hdi    rw [h_eq]    simpa [μ] using Tendsto.const_add _ h_fun_int  have h_rhs_tendsto :      Tendsto (fun n => -∫ x in Ω, gψ n x * φ x)        atTop (nhds (-∫ x in Ω, g x * φ x)) := by    have h_eq :        (fun n => -∫ x in Ω, gψ n x * φ x) =          fun n => -(∫ x in Ω, g x * φ x) - ∫ x, φ x * (gψ n x - g x) ∂μ := by      funext n      have hgi : Integrable (fun x => g x * φ x) μ := by        simpa [mul_comm] using hφ_memLp.integrable_mul hg_memLp      have hdi : Integrable (fun x => φ x * (gψ n x - g x)) μ :=        hφ_memLp.integrable_mul (hψ_grad_memLp n)      have : ∫ x, gψ n x * φ x ∂μ =          (∫ x, g x * φ x ∂μ) + ∫ x, φ x * (gψ n x - g x) ∂μ := by        calc          ∫ x, gψ n x * φ x ∂μ              = ∫ x, (g x * φ x) + φ x * (gψ n x - g x) ∂μ := by                  congr with x                  ring          _ = (∫ x, g x * φ x ∂μ) + ∫ x, φ x * (gψ n x - g x) ∂μ :=                integral_add hgi hdi      linarith    have h_aux :        Tendsto          (fun n => -(∫ x, g x * φ x ∂μ) - ∫ x, φ x * (gψ n x - g x) ∂μ)          atTop (nhds (-(∫ x, g x * φ x ∂μ) - 0)) :=      Tendsto.const_sub _ h_grad_int    simpa [μ, h_eq] using h_aux  have h_eq_n :      ∀ n,        ∫ x in Ω, ψ n x * dφ x = -∫ x in Ω, gψ n x * φ x := by    intro n    exact hψ_wd n φ hφ hφ_supp hφ_sub  have h_eq_tendsto :      Tendsto (fun n => ∫ x in Ω, ψ n x * dφ x)        atTop (nhds (-∫ x in Ω, g x * φ x)) := by    simpa [h_eq_n] using h_rhs_tendsto  exact tendsto_nhds_unique h_lhs_tendsto h_eq_tendsto