Theorem: CS.deriv_scale (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ (f.scale R).deriv = R⁻¹ • f.deriv.scale R
Tactic:
ext v
State after:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
⊢ (f.scale R).deriv.toFun v = (R⁻¹ • f.deriv.scale R).toFun v

State before:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
⊢ (f.scale R).deriv.toFun v = (R⁻¹ • f.deriv.scale R).toFun v
Tactic:
by_cases hR : R = 0 <;> simp [hR, scale]
State after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ { toFun := 0, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = 0

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : ¬R = 0
⊢ { toFun := fun x => funscale f.toFun R x, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = R⁻¹ • funscale f.deriv.toFun R v

State before:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ { toFun := 0, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = 0
Tactic:
simp [deriv, smul]
State after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ _root_.deriv 0 v = 0

State before:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ _root_.deriv 0 v = 0
Tactic:
exact deriv_const _ _
State after:
no goals

State before:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : ¬R = 0
⊢ { toFun := fun x => funscale f.toFun R x, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = R⁻¹ • funscale f.deriv.toFun R v
Tactic:
exact ((f.hasDerivAt (R⁻¹ • v)).scomp v (by simpa using (hasDerivAt_id v).const_smul R⁻¹)).deriv
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : ¬R = 0
⊢ HasDerivAt (HSMul.hSMul R⁻¹) R⁻¹ v
Tactic:
simpa using (hasDerivAt_id v).const_smul R⁻¹
State after:
no goals