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

State before:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f g : ℝ → E
hf : ContDiff ℝ (↑0) f
hg : ContDiff ℝ (↑0) g
⊢ iteratedDeriv 0 (f - g) = iteratedDeriv 0 f - iteratedDeriv 0 g
Tactic:
rfl
State after:
no goals

State before:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Tactic:
have hf' : ContDiff ℝ n (deriv f) := hf.iterate_deriv' n 1
State after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g

State before:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Tactic:
have hg' : ContDiff ℝ n (deriv g) := hg.iterate_deriv' n 1
State after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g

State before:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
hfg : deriv (f - g) = deriv f - deriv g
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Tactic:
simp_rw [iteratedDeriv_succ', ← ih hf' hg', hfg]
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
⊢ deriv (f - g) = deriv f - deriv g
Tactic:
ext x
State after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ deriv (f - g) x = (deriv f - deriv g) x

State before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ deriv (f - g) x = (deriv f - deriv g) x
Tactic:
apply deriv_sub
State after:
case h.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ DifferentiableAt ℝ (fun y => f y) x

case h.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ DifferentiableAt ℝ (fun y => g y) x

State before:
case h.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ DifferentiableAt ℝ (fun y => f y) x
Tactic:
exact (hf.differentiable (by simp)).differentiableAt
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ 1 ≤ ↑(n + 1)
Tactic:
simp
State after:
no goals

State before:
case h.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ DifferentiableAt ℝ (fun y => g y) x
Tactic:
exact (hg.differentiable (by simp)).differentiableAt
State after:
no goals