Theorem: W1.integrable_iteratedDeriv_Schwarz (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : 𝓢(ℝ, ℂ)
⊢ Integrable (iteratedDeriv n ⇑f) volume
Tactic:
induction n generalizing f with
| zero => exact f.integrable
| succ n ih => simpa [iteratedDeriv_succ'] using ih (f := SchwartzMap.derivCLM ℝ f)
State after:
no goals

State before:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : 𝓢(ℝ, ℂ)
⊢ Integrable (iteratedDeriv 0 ⇑f) volume
Tactic:
exact f.integrable
State after:
no goals

State before:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih : ∀ {f : 𝓢(ℝ, ℂ)}, Integrable (iteratedDeriv n ⇑f) volume
f : 𝓢(ℝ, ℂ)
⊢ Integrable (iteratedDeriv (n + 1) ⇑f) volume
Tactic:
simpa [iteratedDeriv_succ'] using ih (f := SchwartzMap.derivCLM ℝ f)
State after:
no goals