Theorem: W21.hf'' (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ f : W21
⊢ Integrable (deriv (deriv f.toFun)) volume
Tactic:
simpa [iteratedDeriv_succ] using f.integrable le_rfl
State after:
no goals