Moser Reg Test Cutoff mem H01

theorem moserRegTestCutoff_memH01    {u η : E → ℝ} {s ε N p Cη : ℝ}    (hs : 0 < s) (hs1 : s ≤ 1) (hε : 0 < ε) (hN : 0 ≤ N) (_hp : 1 < p)    (hu1 : MemW1pWitness 2 u (Metric.ball (0 : E) 1))    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (hη_bound : ∀ x, |η x| ≤ 1)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ Cη)    (hη_sub_ball : tsupport η ⊆ Metric.ball (0 : E) s) :    MemH01 (moserRegTestCutoff η u ε N p) (Metric.ball (0 : E) s) := by  let hwTest := moserRegTestCutoffWitness (d := d) (p := p) hs hs1 hε hN hu1 hη hη_bound hη_grad_bound  have hv_support : tsupport (moserRegTestCutoff η u ε N p) ⊆ Metric.ball (0 : E) s :=    moserRegTestCutoff_tsupport_subset (d := d) hη_sub_ball  have hv_compact : HasCompactSupport (moserRegTestCutoff η u ε N p) :=    hasCompactSupport_of_tsupport_subset_ball hv_support  have hv_memW01p : MemW01p (ENNReal.ofReal (2 : ℝ)) (moserRegTestCutoff η u ε N p)      (Metric.ball (0 : E) s) :=    memW01p_of_memW1p_of_tsupport_subset Metric.isOpen_ball (by norm_num : (1 : ℝ) < 2)      (by simpa using hwTest.memW1p) hv_compact hv_support  simpa using hv_memW01p