De Giorgi cutoff Sobolev on concentric Balls of pos Part Approx

theorem deGiorgi_cutoffSobolev_on_concentricBalls_of_posPartApprox    {u η : E → ℝ} {x₀ : E} {r s θ lam : ℝ}    (hd : 2 < (d : ℝ))    (hs : 0 < s) (hr : 0 < r) (hrs : r < s)    (hu : MemW1pWitness 2 u (Metric.ball x₀ s))    (happroxBallTheta :      ∃ ψ : ℕ → E → ℝ,        (∀ n, ContDiff ℝ 1 (ψ n)) ∧        (∀ n, HasCompactSupport (ψ n)) ∧        Tendsto          (fun n =>            eLpNorm (fun x => ψ n x - (u x - θ)) 2              (volume.restrict (Metric.ball x₀ s)))          atTop (nhds 0) ∧        (∀ i : Fin d,          Tendsto            (fun n =>              eLpNorm                (fun x =>                  (fderiv ℝ (ψ n) x) (EuclideanSpace.single i 1) - hu.weakGrad x i)                2 (volume.restrict (Metric.ball x₀ s)))            atTop (nhds 0)))    (hθl : θ < lam)    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (_hη_nonneg : ∀ x, 0 ≤ η x)    (hη_eq_one : ∀ x ∈ Metric.ball x₀ r, η x = 1)    (hη_bound : ∀ x, |η x| ≤ 1)    (hη_sub_ball : tsupport η ⊆ Metric.ball x₀ s) :    ∃ hwηθ : MemW1pWitness 2 (deGiorgiCutoffTestGeneral η u θ) (Metric.ball x₀ s),      ∫ x in Metric.ball x₀ r, |positivePartSub u lam x| ^ 2 ∂volume ≤        (C_gns d 2) ^ 2 *          (∫ x in Metric.ball x₀ s, ‖hwηθ.weakGrad x‖ ^ 2 ∂volume) *          ((volume.restrict (Metric.ball x₀ s)).real {x | lam < u x}) ^ (2 / (d : ℝ)) := by  let v : E → ℝ := deGiorgiCutoffTestGeneral η u θ  have hη_comp : HasCompactSupport η :=    hasCompactSupport_of_tsupport_subset_ball hη_sub_ball  obtain ⟨Cη, hCη, hη_grad_bound⟩ :=    exists_fderiv_bound_of_contDiff_hasCompactSupport hη hη_comp  have hvW01 :      MemW01p 2 (deGiorgiCutoffTestGeneral η u θ) (Metric.ball x₀ s) :=    deGiorgiCutoffTest_memW01p_on_ball_of_ballPosPartApprox      hs hu hη hη_bound hCη hη_grad_bound hη_sub_ball θ happroxBallTheta  obtain ⟨hwηθ_real, hSob''⟩ :=    deGiorgi_cutoffSobolev_prepare (d := d) hd hs hu hη hη_bound hη_sub_ball hvW01  let hwηθ : MemW1pWitness 2 v (Metric.ball x₀ s) :=    { memLp := by        simpa [v] using hwηθ_real.memLp      weakGrad := hwηθ_real.weakGrad      weakGrad_component_memLp := by        simpa using hwηθ_real.weakGrad_component_memLp      isWeakGrad := by        simpa [v] using hwηθ_real.isWeakGrad }  let hwθ : MemW1pWitness 2 (positivePartSub u θ) (Metric.ball x₀ s) :=    positivePartSub_memW1pWitness_on_ball hs hu θ happroxBallTheta  refine ⟨hwηθ, ?_⟩  simpa [v, hwηθ, hwθ] using    deGiorgi_cutoffSobolev_superlevelStep (d := d) hd hr hrs hu hwθ hθl hη_eq_one      hwηθ_real hSob''