Zero Extend mem W01p p

theorem zeroExtend_memW01p_p    {Ω : Set E} (hΩ : IsOpen Ω)    {p : ℝ} (hp : 1 < p)    {v : E → ℝ}    (hv : MemW01p (ENNReal.ofReal p) v Ω) :    MemW01p (ENNReal.ofReal p) (Ω.indicator v) Set.univ := by  classical  have hΩ_meas : MeasurableSet Ω := hΩ.measurableSet  let hw : MemW1pWitness (ENNReal.ofReal p) v Ω := Classical.choose hv.2  let hExφ := Classical.choose_spec hv.2  let φ : ℕ → E → ℝ := Classical.choose hExφ  have hφspec := Classical.choose_spec hExφ  have hφ_smooth : ∀ n, ContDiff ℝ (⊤ : ℕ∞) (φ n) := hφspec.1  have hφ_compact : ∀ n, HasCompactSupport (φ n) := hφspec.2.1  have hφ_sub : ∀ n, tsupport (φ n) ⊆ Ω := hφspec.2.2.1  have hφ_fun :      Tendsto        (fun n => eLpNorm (fun x => φ n x - v x) (ENNReal.ofReal p) (volume.restrict Ω))        atTop (nhds 0) := hφspec.2.2.2.1  have hφ_grad :      ∀ i : Fin d,        Tendsto          (fun n =>            eLpNorm              (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hw.weakGrad x i)              (ENNReal.ofReal p) (volume.restrict Ω))          atTop (nhds 0) := hφspec.2.2.2.2  let hwExt := zeroExtend_memW1pWitness_p (d := d) hΩ hp hv hw  refine ⟨hwExt.memW1p, hwExt, φ, hφ_smooth, hφ_compact, ?_, ?_, ?_⟩  · intro n    simp  · have hEq :        (fun n => eLpNorm (fun x => φ n x - Ω.indicator v x) (ENNReal.ofReal p) volume) =          fun n => eLpNorm (fun x => φ n x - v x) (ENNReal.ofReal p) (volume.restrict Ω) := by      funext n      have hFn :          (fun x => φ n x - Ω.indicator v x) =            Ω.indicator (fun x => φ n x - v x) := by        ext x        by_cases hx : x ∈ Ω        · simp [hx]        · have hφx : φ n x = 0 := zero_outside_of_tsupport_subset (Ω := Ω) (hφ_sub n) hx          simp [hx, hφx]      rw [hFn, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict        (μ := volume) (s := Ω) (p := ENNReal.ofReal p) hΩ_meas]    rw [Measure.restrict_univ, hEq]    simpa using hφ_fun  · intro i    have hEq :        (fun n =>          eLpNorm            (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hwExt.weakGrad x i)            (ENNReal.ofReal p) volume) =          fun n =>            eLpNorm              (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hw.weakGrad x i)              (ENNReal.ofReal p) (volume.restrict Ω) := by      funext n      have hFn :          (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hwExt.weakGrad x i) =            Ω.indicator              (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hw.weakGrad x i) := by        ext x        by_cases hx : x ∈ Ω        · simp [hwExt, zeroExtend_memW1pWitness_p, hx]        · have hdx :              (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) = 0 := by            exact fderiv_apply_zero_outside_of_tsupport_subset (Ω := Ω) (hf := hφ_smooth n)              (hsub := hφ_sub n) hx i          simp [hwExt, zeroExtend_memW1pWitness_p, hx, hdx]      rw [hFn, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict        (μ := volume) (s := Ω) (p := ENNReal.ofReal p) hΩ_meas]    rw [Measure.restrict_univ, hEq]    simpa using hφ_grad i