Moser power Cutoff mem W01p energy of subsolution

theorem moser_powerCutoff_memW01p_energy_of_subsolution    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {u η : E → ℝ} {p s Cη : ℝ}    (hp : 1 < p)    (hs : 0 < s) (hs1 : s ≤ 1)    (hsub : IsSubsolution A.1 u)    (hpInt :      IntegrableOn (fun x => |max (u x) 0| ^ p)        (Metric.ball (0 : E) s) volume)    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (hη_nonneg : ∀ x, 0 ≤ η x)    (hη_bound : ∀ x, |η x| ≤ 1)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ Cη)    (hη_sub_ball : tsupport η ⊆ Metric.ball (0 : E) s) :    ∃ hwv : MemW1pWitness 2 (moserPowerCutoff (d := d) η u p) (Metric.ball (0 : E) s),      MemW01p 2 (moserPowerCutoff (d := d) η u p) (Metric.ball (0 : E) s) ∧      ∫ x in Metric.ball (0 : E) s, ‖hwv.weakGrad x‖ ^ 2 ∂volume ≤        2 * Cη ^ 2 * (A.1.Λ * (p / (p - 1)) ^ 2 + 1) *          ∫ x in Metric.ball (0 : E) s, |max (u x) 0| ^ p ∂volume := by  let Ω : Set E := Metric.ball (0 : E) s  let v : E → ℝ := moserPowerCutoff (d := d) η u p  have hv_support : tsupport v ⊆ Ω :=    moserPowerCutoff_tsupport_subset (d := d) (u := u) (η := η) (p := p) hη_sub_ball  obtain ⟨hwv, henergy⟩ :=    moser_powerCutoff_memW1p_energy_of_subsolution_core      (d := d) hd A (u := u) (η := η) (p := p) (s := s) (Cη := Cη)      hp hs hs1 hsub hpInt hη hη_nonneg hη_bound hη_grad_bound hη_sub_ball  have hv_compact : HasCompactSupport v :=    hasCompactSupport_of_tsupport_subset_ball hv_support  have hv_memW1p_real : MemW1p (ENNReal.ofReal (2 : ℝ)) v Ω := by    simpa [Ω] using hwv.memW1p  have hvW01_real : MemW01p (ENNReal.ofReal (2 : ℝ)) v Ω := by    exact memW01p_of_memW1p_of_tsupport_subset      (d := d) Metric.isOpen_ball (p := (2 : ℝ)) (by norm_num) hv_memW1p_real hv_compact hv_support  have hvW01 : MemW01p 2 v Ω := by    simpa [Ω] using hvW01_real  exact ⟨hwv, hvW01, henergy⟩