De Giorgi Cutoff Test mem W01p of pos Part Approx

theorem deGiorgiCutoffTest_memW01p_of_posPartApprox    {Ω : Set E} [IsFiniteMeasure (volume.restrict Ω)]    (hΩ : IsOpen Ω)    {u η : E → ℝ}    (hw : MemW1pWitness 2 u Ω)    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    {C₀ C₁ : ℝ}    (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁)    (hη_bound : ∀ x, |η x| ≤ C₀)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ C₁)    (hη_comp : HasCompactSupport η)    (hη_sub : tsupport η ⊆ Ω)    (k : ℝ)    (happroxShift :      ∃ ψ : ℕ → E → ℝ,        (∀ n, ContDiff ℝ 1 (ψ n)) ∧        (∀ n, HasCompactSupport (ψ n)) ∧        Tendsto (fun n => eLpNorm (fun x => ψ n x - (u x - k)) 2 (volume.restrict Ω))          atTop (nhds 0) ∧        (∀ i : Fin d,          Tendsto (fun n => eLpNorm (fun x =>            (fderiv ℝ (ψ n) x) (EuclideanSpace.single i 1) - hw.weakGrad x i)            2 (volume.restrict Ω))          atTop (nhds 0))) :    MemW01p 2 (deGiorgiCutoffTestGeneral η u k) Ω := by  let hw_trunc : MemW1pWitness 2 (positivePartSub u k) Ω :=    positivePartSub_memW1pWitness hΩ hw k happroxShift  exact    deGiorgiCutoffTest_memW01p_of_truncWitness      hΩ hw_trunc hη hC₀ hC₁ hη_bound hη_grad_bound hη_comp hη_sub