De Giorgi cutoff Sobolev on concentric Balls of ball Pos Part

theorem deGiorgi_cutoffSobolev_on_concentricBalls_of_ballPosPart    {u η : E → ℝ} {x₀ : E} {r s θ lam : ℝ}    (hd : 2 < (d : ℝ))    (hr : 0 < r) (hrs : r < s)    (hu : MemW1pWitness 2 u (Metric.ball x₀ s))    (hwθ : MemW1pWitness 2 (positivePartSub u θ) (Metric.ball x₀ s))    (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  have hs : 0 < s := lt_trans hr hrs  let v : E → ℝ := deGiorgiCutoffTestGeneral η u θ  haveI : IsFiniteMeasure (volume.restrict (Metric.ball x₀ s)) := by    rw [isFiniteMeasure_restrict]    exact measure_ball_lt_top.ne  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_of_truncWitness      isOpen_ball hwθ hη (by norm_num) hCη hη_bound hη_grad_bound hη_comp hη_sub_ball  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 }  refine ⟨hwηθ, ?_⟩  simpa [v, hwηθ] using    deGiorgi_cutoffSobolev_superlevelStep (d := d) hd hr hrs hu hwθ hθl hη_eq_one      hwηθ_real hSob''