Sobolev of mem W01p univ

theorem sobolev_of_memW01p_univ    {p : ℝ} (hp : 1 ≤ p) (hpd : p < (d : ℝ))    {u : E → ℝ}    (hu : MemW01p (ENNReal.ofReal p) u Set.univ volume) :    ∃ hw : MemW1pWitness (ENNReal.ofReal p) u Set.univ volume,      eLpNorm u (ENNReal.ofReal ((d : ℝ) * p / ((d : ℝ) - p))) volume ≤        ENNReal.ofReal (C_gns d p) *          eLpNorm (fun x => ‖hw.weakGrad x‖) (ENNReal.ofReal p) volume := by  rcases hu with ⟨_, hw, φ, hφ_smooth, hφ_cpt, _hφ_sub, hφ_fun, hφ_grad⟩  refine ⟨hw, ?_⟩  have hu_aesm : AEStronglyMeasurable u volume := by    simpa using hw.memLp.aestronglyMeasurable  have hG_comp_aesm : ∀ i : Fin d,      AEStronglyMeasurable (fun x => hw.weakGrad x i) volume := by    intro i    simpa using (hw.weakGrad_component_memLp i).aestronglyMeasurable  have hφ_fun_univ :      Tendsto (fun n => eLpNorm (fun x => φ n x - u x) (ENNReal.ofReal p) volume)        atTop (nhds 0) := by    simpa using hφ_fun  have hφ_grad_univ : ∀ i : Fin d, Tendsto      (fun n => eLpNorm        (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hw.weakGrad x i)        (ENNReal.ofReal p) volume)      atTop (nhds 0) := by    intro i    simpa using hφ_grad i  simpa [eLpNorm_norm] using    sobolev_of_approx hp hpd hu_aesm hG_comp_aesm φ      hφ_smooth hφ_cpt hφ_fun_univ hφ_grad_univ