-- Mathlib/Analysis/InnerProductSpace/NormPow.lean
theorem hasFDerivAt_norm_rpow (x : E) {p : ℝ} (hp : 1 < p) :
    HasFDerivAt (fun x : E ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • innerSL ℝ x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Tactic:
by_cases hx : x = 0

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x' => ‖x'‖ ^ p - ‖0‖ ^ p - 0 (x' - 0)) =o[𝓝 0] fun x' => x' - 0

Tactic:
calc (fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0)
    = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
  _ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
      ext x
      rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
      ring_nf
  _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
    refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by norm_num).mpr ?_
    convert continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
    simp [h2p.ne']
  _ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by
    simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]

Result:
no goals

Proof state:
case a.a.h.e'_12.h.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ p * ‖x‖ ^ (-2 + p) = p * (1 / 2) * ‖x‖ ^ (-2 + p) * 2

Tactic:
ring

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) 0 0

Tactic:
have h2p : 0 < p - 1 := sub_pos.mpr hp

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) 0 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x => ‖x‖ * ‖x‖ ^ (p - 1)) =o[𝓝 0] fun x => ‖x‖ * 1

Tactic:
refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by norm_num).mpr ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ Filter.Tendsto (fun x => ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x => ‖x‖ ^ p) = fun x => ‖x‖ * ‖x‖ ^ (p - 1)

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ * ‖x‖ ^ (p - 1)

Proof state:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (-2 + p)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * (1 / 2) * ‖x‖ ^ (-2 + p) * 2) • (innerSL ℝ) x) x

Tactic:
congr! 2

Result:
case a.a.h.e'_12.h.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ p * ‖x‖ ^ (-2 + p) = p * (1 / 2) * ‖x‖ ^ (-2 + p) * 2

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ 1 + (p - 1) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x => ‖x‖ ^ (↑2 * (p / 2))) ((p / 2 * ‖x‖ ^ (↑2 * (p / 2 - 1)) * ↑2) • (innerSL ℝ) x) x

Tactic:
ring_nf

Result:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (-2 + p)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * (1 / 2) * ‖x‖ ^ (-2 + p) * 2) • (innerSL ℝ) x) x

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))

Tactic:
ring_nf

Result:
no goals

Proof state:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x => (‖x‖ ^ 2) ^ (p / 2)) ((p / 2 * (‖x‖ ^ 2) ^ (p / 2 - 1)) • 2 • (innerSL ℝ) x) x

Tactic:
simp_rw [← Real.rpow_natCast_mul (norm_nonneg _), ← Nat.cast_smul_eq_nsmul ℝ, smul_smul]

Result:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x => ‖x‖ ^ (↑2 * (p / 2))) ((p / 2 * ‖x‖ ^ (↑2 * (p / 2 - 1)) * ↑2) • (innerSL ℝ) x) x

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ * ‖x‖ ^ (p - 1)

Tactic:
rw [← rpow_one_add' (norm_nonneg x) (by positivity)]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Tactic:
apply HasStrictFDerivAt.hasFDerivAt

Result:
case neg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x => ‖x‖ ^ p - ‖0‖ ^ p - 0) = fun x => ‖x‖ ^ p

Tactic:
simp [zero_lt_one.trans hp |>.ne']

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) 0 0

Tactic:
rw [HasFDerivAt, hasFDerivAtFilter_iff_isLittleO]

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x' => ‖x'‖ ^ p - ‖0‖ ^ p - 0 (x' - 0)) =o[𝓝 0] fun x' => x' - 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x => ‖x‖ * 1) =O[𝓝 0] fun x => x - 0

Tactic:
simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]

Result:
no goals

Proof state:
case neg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Tactic:
convert (hasStrictFDerivAt_norm_sq x).rpow_const (p := p / 2) (by simp [hx]) using 0

Result:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x => (‖x‖ ^ 2) ^ (p / 2)) ((p / 2 * (‖x‖ ^ 2) ^ (p / 2 - 1)) • 2 • (innerSL ℝ) x) x