Mem W01p add

theorem MemW01p.add    {Ω : Set E} {u v : E → ℝ}    (hu : MemW01p 2 u Ω) (hv : MemW01p 2 v Ω) :    MemW01p 2 (fun x => u x + v x) Ω := by  let _ := (inferInstance : NeZero d)  rcases hu with ⟨_, hwu, φu, hφu_smooth, hφu_compact, hφu_sub, hφu_fun, hφu_grad⟩  rcases hv with ⟨_, hwv, φv, hφv_smooth, hφv_compact, hφv_sub, hφv_fun, hφv_grad⟩  refine ⟨(hwu.add hwv).memW1p, hwu.add hwv, fun n x => φu n x + φv n x, ?_, ?_, ?_, ?_, ?_⟩  · intro n    exact (hφu_smooth n).add (hφv_smooth n)  · intro n    exact (hφu_compact n).add (hφv_compact n)  · intro n    exact (tsupport_add (φu n) (φv n)).trans <| union_subset (hφu_sub n) (hφv_sub n)  ·    have hupper :        ∀ n,          eLpNorm (fun x => (φu n x + φv n x) - (u x + v x)) 2 (volume.restrict Ω) ≤            eLpNorm (fun x => φu n x - u x) 2 (volume.restrict Ω) +              eLpNorm (fun x => φv n x - v x) 2 (volume.restrict Ω) := by      intro n      have hφu_mem : MemLp (φu n) 2 (volume.restrict Ω) :=        ((hφu_smooth n).continuous.memLp_of_hasCompactSupport (hφu_compact n)).restrict Ω      have hφv_mem : MemLp (φv n) 2 (volume.restrict Ω) :=        ((hφv_smooth n).continuous.memLp_of_hasCompactSupport (hφv_compact n)).restrict Ω      have hdu_mem : MemLp (fun x => φu n x - u x) 2 (volume.restrict Ω) :=        hφu_mem.sub hwu.memLp      have hdv_mem : MemLp (fun x => φv n x - v x) 2 (volume.restrict Ω) :=        hφv_mem.sub hwv.memLp      have hEq :          (fun x => (φu n x + φv n x) - (u x + v x)) =            (fun x => (φu n x - u x) + (φv n x - v x)) := by        ext x        ring      rw [hEq]      exact eLpNorm_add_le hdu_mem.aestronglyMeasurable hdv_mem.aestronglyMeasurable (by norm_num)    have hsum :        Tendsto          (fun n =>            eLpNorm (fun x => φu n x - u x) 2 (volume.restrict Ω) +              eLpNorm (fun x => φv n x - v x) 2 (volume.restrict Ω))          atTop (nhds (0 + 0)) :=      hφu_fun.add hφv_fun    refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ?_ (fun n => zero_le _) hupper    simpa using hsum  · intro i    have hupper :        ∀ n,          eLpNorm              (fun x =>                (fderiv ℝ (fun y => φu n y + φv n y) x) (EuclideanSpace.single i 1) -                  (hwu.add hwv).weakGrad x i)              2 (volume.restrict Ω) ≤            eLpNorm                (fun x => (fderiv ℝ (φu n) x) (EuclideanSpace.single i 1) - hwu.weakGrad x i)                2 (volume.restrict Ω) +              eLpNorm                (fun x => (fderiv ℝ (φv n) x) (EuclideanSpace.single i 1) - hwv.weakGrad x i)                2 (volume.restrict Ω) := by      intro n      let ei : E := EuclideanSpace.single i (1 : ℝ)      have hderiv_u_smooth : ContDiff ℝ (⊤ : ℕ∞)          (fun x => (fderiv ℝ (φu n) x) ei) :=        ((hφu_smooth n).fderiv_right (m := (⊤ : ℕ∞)) (by norm_cast)).clm_apply contDiff_const      have hderiv_v_smooth : ContDiff ℝ (⊤ : ℕ∞)          (fun x => (fderiv ℝ (φv n) x) ei) :=        ((hφv_smooth n).fderiv_right (m := (⊤ : ℕ∞)) (by norm_cast)).clm_apply contDiff_const      have hderiv_u_mem : MemLp (fun x => (fderiv ℝ (φu n) x) ei) 2 (volume.restrict Ω) :=        (hderiv_u_smooth.continuous.memLp_of_hasCompactSupport ((hφu_compact n).fderiv_apply (𝕜 := ℝ) ei)).restrict Ω      have hderiv_v_mem : MemLp (fun x => (fderiv ℝ (φv n) x) ei) 2 (volume.restrict Ω) :=        (hderiv_v_smooth.continuous.memLp_of_hasCompactSupport ((hφv_compact n).fderiv_apply (𝕜 := ℝ) ei)).restrict Ω      have hdu_mem :          MemLp (fun x => (fderiv ℝ (φu n) x) ei - hwu.weakGrad x i) 2 (volume.restrict Ω) :=        hderiv_u_mem.sub (hwu.weakGrad_component_memLp i)      have hdv_mem :          MemLp (fun x => (fderiv ℝ (φv n) x) ei - hwv.weakGrad x i) 2 (volume.restrict Ω) :=        hderiv_v_mem.sub (hwv.weakGrad_component_memLp i)      have hEq :          (fun x =>            (fderiv ℝ (fun y => φu n y + φv n y) x) ei - (hwu.add hwv).weakGrad x i) =            (fun x =>              ((fderiv ℝ (φu n) x) ei - hwu.weakGrad x i) +                ((fderiv ℝ (φv n) x) ei - hwv.weakGrad x i)) := by        ext x        have hfd :            fderiv ℝ (fun y => φu n y + φv n y) x =              fderiv ℝ (φu n) x + fderiv ℝ (φv n) x := by          have hu_diff : DifferentiableAt ℝ (φu n) x :=            ((hφu_smooth n).contDiffAt).differentiableAt (by norm_num)          have hv_diff : DifferentiableAt ℝ (φv n) x :=            ((hφv_smooth n).contDiffAt).differentiableAt (by norm_num)          exact fderiv_add hu_diff hv_diff        simp [ei, MemW1pWitness.add, hfd]        ring      rw [hEq]      exact eLpNorm_add_le hdu_mem.aestronglyMeasurable hdv_mem.aestronglyMeasurable (by norm_num)    have hsum :        Tendsto          (fun n =>            eLpNorm                (fun x => (fderiv ℝ (φu n) x) (EuclideanSpace.single i 1) - hwu.weakGrad x i)                2 (volume.restrict Ω) +              eLpNorm                (fun x => (fderiv ℝ (φv n) x) (EuclideanSpace.single i 1) - hwv.weakGrad x i)                2 (volume.restrict Ω))          atTop (nhds (0 + 0)) :=      (hφu_grad i).add (hφv_grad i)    refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ?_ (fun n => zero_le _) hupper    simpa using hsum