Caccioppoli weighted on ball of ball Pos Part

theorem caccioppoli_weighted_on_ball_of_ballPosPart    {u η : E → ℝ} {x₀ : E} {s Cη k : ℝ}    (A : EllipticCoeff d (Metric.ball x₀ s))    (_hs : 0 < s)    (hsub : IsSubsolution A u)    (hu : MemW1pWitness 2 u (Metric.ball x₀ s))    (hw_trunc : MemW1pWitness 2 (positivePartSub u k) (Metric.ball x₀ s))    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (hη_nonneg : ∀ x, 0 ≤ η x)    (hη_bound : ∀ x, |η x| ≤ 1)    (hCη : 0 ≤ Cη)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ Cη)    (hη_sub_ball : tsupport η ⊆ Metric.ball x₀ s) :    ∫ x in Metric.ball x₀ s, η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume ≤      4 * ellipticityRatio A *        ∫ x in Metric.ball x₀ s, ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u k x| ^ 2 ∂volume := by  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  have hη_admissible :      MemW01p 2 (deGiorgiCutoffTestGeneral η u k) (Metric.ball x₀ s) :=    deGiorgiCutoffTest_memW01p_of_truncWitness      isOpen_ball hw_trunc hη (by norm_num) hCη hη_bound hη_grad_bound hη_comp hη_sub_ball  exact caccioppoli_weighted_of_subsolution isOpen_ball A hsub hu hw_trunc hη hη_nonneg    (by norm_num) hCη hη_bound hη_grad_bound hη_admissible