[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ HasStrictFDerivAt b (deriv h p) p
[PROOFSTEP]
simp only [HasStrictFDerivAt]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ (fun p_1 => b p_1.fst - b p_1.snd - ↑(deriv h p) (p_1.fst - p_1.snd)) =o[𝓝 (p, p)] fun p => p.fst - p.snd
[PROOFSTEP]
simp only [← map_add_left_nhds_zero (p, p), isLittleO_map]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ ((fun p_1 => b p_1.fst - b p_1.snd - ↑(deriv h p) (p_1.fst - p_1.snd)) ∘ fun x => (p, p) + x) =o[𝓝 0]
    ((fun p => p.fst - p.snd) ∘ fun x => (p, p) + x)
[PROOFSTEP]
set T := (E × F) × E × F
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ ((fun p_1 => b p_1.fst - b p_1.snd - ↑(deriv h p) (p_1.fst - p_1.snd)) ∘ fun x => (p, p) + x) =o[𝓝 0]
    ((fun p => p.fst - p.snd) ∘ fun x => (p, p) + x)
[PROOFSTEP]
calc
  _ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) :=
    by
    ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
    rcases p with ⟨x, y⟩
    simp [h.add_left, h.add_right, h.deriv_apply, h.map_sub_left, h.map_sub_right]
    abel
      -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
          --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
          -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
  _ =o[𝓝 (0 : T)] fun x ↦ x.1 - x.2 := by
    -- TODO : add 2 `calc` steps instead of the next 3 lines
    refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
    suffices : (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1
    · simpa only [mul_one, isLittleO_norm_right] using this
    refine
      (isBigO_refl _ _).mul_isLittleO
        ((isLittleO_one_iff _).2 ?_)
          -- TODO: `continuity` fails
    exact (continuous_snd.fst.prod_mk continuous_fst.snd).norm.tendsto' _ _ (by simp)
  _ = _ := by simp [(· ∘ ·)]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ ((fun p_1 => b p_1.fst - b p_1.snd - ↑(deriv h p) (p_1.fst - p_1.snd)) ∘ fun x => (p, p) + x) = fun x =>
    ↑(deriv h (x.fst - x.snd)) (x.snd.fst, x.fst.snd)
[PROOFSTEP]
ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
[GOAL]
case h.mk.mk.mk
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
⊢ ((fun p_1 => b p_1.fst - b p_1.snd - ↑(deriv h p) (p_1.fst - p_1.snd)) ∘ fun x => (p, p) + x) ((x₁, y₁), x₂, y₂) =
    ↑(deriv h (((x₁, y₁), x₂, y₂).fst - ((x₁, y₁), x₂, y₂).snd))
      (((x₁, y₁), x₂, y₂).snd.fst, ((x₁, y₁), x₂, y₂).fst.snd)
[PROOFSTEP]
rcases p with ⟨x, y⟩
[GOAL]
case h.mk.mk.mk.mk
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
x : E
y : F
⊢ ((fun p => b p.fst - b p.snd - ↑(deriv h (x, y)) (p.fst - p.snd)) ∘ fun x_1 => ((x, y), x, y) + x_1)
      ((x₁, y₁), x₂, y₂) =
    ↑(deriv h (((x₁, y₁), x₂, y₂).fst - ((x₁, y₁), x₂, y₂).snd))
      (((x₁, y₁), x₂, y₂).snd.fst, ((x₁, y₁), x₂, y₂).fst.snd)
[PROOFSTEP]
simp [h.add_left, h.add_right, h.deriv_apply, h.map_sub_left, h.map_sub_right]
[GOAL]
case h.mk.mk.mk.mk
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
x : E
y : F
⊢ b (x, y) + b (x₁, y) + (b (x, y₁) + b (x₁, y₁)) - (b (x, y) + b (x₂, y) + (b (x, y₂) + b (x₂, y₂))) -
      (b (x, y) + b (x, y₁) + (b (x, y) + b (x₁, y)) - (b (x, y) + b (x, y₂) + (b (x, y) + b (x₂, y)))) =
    b (x₁, y₁) - b (x₂, y₂)
[PROOFSTEP]
abel
  -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
      --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
      -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
[GOAL]
case h.mk.mk.mk.mk
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
x : E
y : F
⊢ b (x, y) + b (x₁, y) + (b (x, y₁) + b (x₁, y₁)) - (b (x, y) + b (x₂, y) + (b (x, y₂) + b (x₂, y₂))) -
      (b (x, y) + b (x, y₁) + (b (x, y) + b (x₁, y)) - (b (x, y) + b (x, y₂) + (b (x, y) + b (x₂, y)))) =
    b (x₁, y₁) - b (x₂, y₂)
[PROOFSTEP]
abel
  -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
      --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
      -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => ↑(deriv h (x.fst - x.snd)) (x.snd.fst, x.fst.snd)) =o[𝓝 0] fun x => x.fst - x.snd
[PROOFSTEP]
refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => ‖x.fst - x.snd‖ * ‖(x.snd.fst, x.fst.snd)‖) =o[𝓝 0] fun x => x.fst - x.snd
[PROOFSTEP]
suffices : (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
this : (fun x => ‖x.fst - x.snd‖ * ‖(x.snd.fst, x.fst.snd)‖) =o[𝓝 0] fun x => ‖x.fst - x.snd‖ * 1
⊢ (fun x => ‖x.fst - x.snd‖ * ‖(x.snd.fst, x.fst.snd)‖) =o[𝓝 0] fun x => x.fst - x.snd
[PROOFSTEP]
simpa only [mul_one, isLittleO_norm_right] using this
[GOAL]
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => ‖x.fst - x.snd‖ * ‖(x.snd.fst, x.fst.snd)‖) =o[𝓝 0] fun x => ‖x.fst - x.snd‖ * 1
[PROOFSTEP]
refine
  (isBigO_refl _ _).mul_isLittleO
    ((isLittleO_one_iff _).2 ?_)
      -- TODO: `continuity` fails
[GOAL]
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ Tendsto (fun x => ‖(x.snd.fst, x.fst.snd)‖) (𝓝 0) (𝓝 0)
[PROOFSTEP]
exact (continuous_snd.fst.prod_mk continuous_fst.snd).norm.tendsto' _ _ (by simp)
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ ‖(0.snd.fst, 0.fst.snd)‖ = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => x.fst - x.snd) = (fun p => p.fst - p.snd) ∘ fun x => (p, p) + x
[PROOFSTEP]
simp [(· ∘ ·)]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderivWithin 𝕜 b u p = deriv h p
[PROOFSTEP]
rw [DifferentiableAt.fderivWithin (h.differentiableAt p) hxs]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderiv 𝕜 b p = deriv h p
[PROOFSTEP]
exact h.fderiv p


[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
have A : p.1 ≠ 0 := by intro h; simp [h, lt_irrefl] at hp
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ p.fst ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
h : p.fst = 0
⊢ False
[PROOFSTEP]
simp [h, lt_irrefl] at hp
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
have : (fun x : ℂ × ℂ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
  ((isOpen_ne.preimage continuous_fst).eventually_mem A).mono fun p hp => cpow_def_of_ne_zero hp _
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
rw [cpow_sub _ _ A, cpow_one, mul_div_left_comm, mul_smul, mul_smul]
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    (p.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd))
    (p.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
simpa only [cpow_def_of_ne_zero A, div_eq_mul_inv, mul_smul, add_comm, smul_add] using
  ((hasStrictFDerivAt_fst.clog hp).mul hasStrictFDerivAt_snd).cexp
[GOAL]
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y
[PROOFSTEP]
rcases em (x = 0) with (rfl | hx)
[GOAL]
case inl
y : ℂ
h : 0 ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y
[PROOFSTEP]
replace h := h.neg_resolve_left rfl
[GOAL]
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y
[PROOFSTEP]
rw [log_zero, mul_zero]
[GOAL]
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) 0 y
[PROOFSTEP]
refine' (hasStrictDerivAt_const _ 0).congr_of_eventuallyEq _
[GOAL]
case inl
y : ℂ
h : y ≠ 0
⊢ (fun x => 0) =ᶠ[𝓝 y] fun y => 0 ^ y
[PROOFSTEP]
exact (isOpen_ne.eventually_mem h).mono fun y hy => (zero_cpow hy).symm
[GOAL]
case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y
[PROOFSTEP]
simpa only [cpow_def_of_ne_zero hx, mul_one] using ((hasStrictDerivAt_id y).const_mul (log x)).cexp
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
s : Set E
c : ℂ
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
[PROOFSTEP]
convert (@hasStrictFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prod hg)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
s : Set E
c : ℂ
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
[PROOFSTEP]
convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prod hg)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
s : Set E
c : ℂ
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x
[PROOFSTEP]
convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x (hf.prod hg)
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
⊢ ↑((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
          (f x ^ g x * log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1 =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g'
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.one_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.add_apply, Pi.smul_apply, ContinuousLinearMap.coe_smul']
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
[PROOFSTEP]
simpa using (hf.cpow hg h0).hasStrictDerivAt
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x
[PROOFSTEP]
simpa only [mul_zero, add_zero, mul_one] using (hasStrictDerivAt_id x).cpow (hasStrictDerivAt_const x c) h
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
[PROOFSTEP]
simpa only [aux] using (hf.hasFDerivAt.cpow hg h0).hasDerivAt
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
[PROOFSTEP]
simpa only [aux] using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ -1
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
rw [Ne.def, ← add_eq_zero_iff_eq_neg, ← Ne.def] at hr
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
rcases lt_or_gt_of_ne hx.symm with (hx | hx)
[GOAL]
case inl
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
apply HasDerivAt.comp_ofReal (e := fun y => (y : ℂ) ^ (r + 1) / (r + 1))
[GOAL]
case inl
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => y ^ (r + 1) / (r + 1)) (↑x ^ r) ↑x
[PROOFSTEP]
convert HasDerivAt.div_const (𝕜 := ℂ) ?_ (r + 1) using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r = ?inl.convert_3 / (r + 1)
[PROOFSTEP]
exact (mul_div_cancel _ hr).symm
[GOAL]
case inl.convert_4
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => y ^ (r + 1)) (↑x ^ r * (r + 1)) ↑x
[PROOFSTEP]
convert HasDerivAt.cpow_const ?_ ?_ using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r * (r + 1) = (r + 1) * ↑x ^ (r + 1 - 1) * ?inl.convert_4.convert_2
[PROOFSTEP]
rw [add_sub_cancel, mul_comm]
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (r + 1) * ↑x ^ r = (r + 1) * ↑x ^ r * ?inl.convert_4.convert_2
case inl.convert_4.convert_2
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ℂ
case inl.convert_4.convert_2 f g : ℂ → ℂ s : Set ℂ f' g' x✝ c : ℂ x : ℝ hx✝ : x ≠ 0 r : ℂ hr : r + 1 ≠ 0 hx : 0 < x ⊢ ℂ
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
case inl.convert_4.convert_5
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => y) 1 ↑x
[PROOFSTEP]
exact hasDerivAt_id (x : ℂ)
[GOAL]
case inl.convert_4.convert_6
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ 0 < (↑x).re ∨ (↑x).im ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
have : ∀ᶠ y : ℝ in nhds x, (y : ℂ) ^ (r + 1) / (r + 1) = (-y : ℂ) ^ (r + 1) * exp (π * I * (r + 1)) / (r + 1) :=
  by
  refine' Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => _
  rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
[PROOFSTEP]
refine' Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => _
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
y : ℝ
hy : y ∈ Set.Iio 0
⊢ ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
[PROOFSTEP]
rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
refine' HasDerivAt.congr_of_eventuallyEq _ this
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun x => (-↑x) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
rw [ofReal_cpow_of_nonpos (le_of_lt hx)]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun x => (-↑x) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)) ((-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
suffices HasDerivAt (fun y : ℝ => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
  by
  convert this.div_const (r + 1) using 1
  conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
⊢ HasDerivAt (fun x => (-↑x) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)) ((-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
convert this.div_const (r + 1) using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
⊢ (-↑x) ^ r * exp (↑π * I * r) = (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
rw [mul_add ((π : ℂ) * _), mul_one, exp_add, exp_pi_mul_I, mul_comm (_ : ℂ) (-1 : ℂ), neg_one_mul]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => (-↑y) ^ (r + 1) * -exp (↑π * I * r)) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
simp_rw [mul_neg, ← neg_mul, ← ofReal_neg]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => -↑(-y) ^ (r + 1) * exp (↑π * I * r)) ((r + 1) * ↑(-x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
suffices HasDerivAt (fun y : ℝ => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by convert this.neg.mul_const _ using 1;
  ring
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
⊢ HasDerivAt (fun y => -↑(-y) ^ (r + 1) * exp (↑π * I * r)) ((r + 1) * ↑(-x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
convert this.neg.mul_const _ using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
⊢ (r + 1) * ↑(-x) ^ r * exp (↑π * I * r) = -(-(r + 1) * ↑(-x) ^ r) * exp (↑π * I * r)
[PROOFSTEP]
ring
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
[PROOFSTEP]
suffices HasDerivAt (fun y : ℝ => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
  by
  convert @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
  rw [real_smul, ofReal_neg 1, ofReal_one]; ring
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
[PROOFSTEP]
convert @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 • ((r + 1) * ↑(-x) ^ r)
[PROOFSTEP]
rw [real_smul, ofReal_neg 1, ofReal_one]
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 * ((r + 1) * ↑(-x) ^ r)
[PROOFSTEP]
ring
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
[PROOFSTEP]
suffices HasDerivAt (fun y : ℂ => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x) by exact this.comp_ofReal
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
⊢ HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
[PROOFSTEP]
exact this.comp_ofReal
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
[PROOFSTEP]
conv in ↑_ ^ _ => rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
| y ^ (r + 1)
[PROOFSTEP]
rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
| y ^ (r + 1)
[PROOFSTEP]
rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
| y ^ (r + 1)
[PROOFSTEP]
rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
⊢ r = r + 1 - 1
[PROOFSTEP]
ring
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => y ^ (r + 1 - 1 + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
[PROOFSTEP]
convert HasDerivAt.cpow_const ?_ ?_ using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ (r + 1) * ↑(-x) ^ r = (r + 1 - 1 + 1) * ↑(-x) ^ (r + 1 - 1 + 1 - 1) * ?inr.convert_2
[PROOFSTEP]
rw [add_sub_cancel, add_sub_cancel]
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ (r + 1) * ↑(-x) ^ r = (r + 1) * ↑(-x) ^ r * ?inr.convert_2
case inr.convert_2
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ ℂ
case inr.convert_2
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ ℂ
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
case inr.convert_5
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => y) 1 ↑(-x)
[PROOFSTEP]
exact hasDerivAt_id ((-x : ℝ) : ℂ)
[GOAL]
case inr.convert_6
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ 0 < (↑(-x)).re ∨ (↑(-x)).im ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
  (continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd))
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
convert ((hasStrictFDerivAt_fst.log hp.ne').mul hasStrictFDerivAt_snd).exp using 1
[GOAL]
case h.e'_10
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ (p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    exp (log p.fst * p.snd) •
      (log p.fst • ContinuousLinearMap.snd ℝ ℝ ℝ + p.snd • p.fst⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
[PROOFSTEP]
rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm, div_eq_mul_inv, smul_smul,
  smul_smul, mul_assoc, add_comm]
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) * cos (x.2 * π) :=
  (continuousAt_fst.eventually (gt_mem_nhds hp)).mono fun p hp => rpow_def_of_neg hp _
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd) * cos (x.snd * π))
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
convert
  ((hasStrictFDerivAt_fst.log hp.ne).mul hasStrictFDerivAt_snd).exp.mul (hasStrictFDerivAt_snd.mul_const π).cos using 1
[GOAL]
case h.e'_10.h.h
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ (p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    exp (log p.fst * p.snd) • -sin (p.snd * π) • π • ContinuousLinearMap.snd ℝ ℝ ℝ +
      cos (p.snd * π) •
        exp (log p.fst * p.snd) •
          (log p.fst • ContinuousLinearMap.snd ℝ ℝ ℝ + p.snd • p.fst⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
[PROOFSTEP]
simp_rw [rpow_sub_one hp.ne, smul_add, ← add_assoc, smul_smul, ← add_smul, ← mul_assoc, mul_comm (cos _), ←
  rpow_def_of_neg hp]
[GOAL]
case h.e'_10.h.h
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ (p.snd * (p.fst ^ p.snd / p.fst)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (exp (log p.fst * p.snd) * -sin (p.snd * π) * π + p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.fst ^ p.snd * p.snd * p.fst⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
rw [div_eq_mul_inv, add_comm]
[GOAL]
case h.e'_10.h.h
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.snd * (p.fst ^ p.snd * p.fst⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ =
    (exp (log p.fst * p.snd) * -sin (p.snd * π) * π + p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.fst ^ p.snd * p.snd * p.fst⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_10.h.h.e_a.e_a
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π =
    exp (log p.fst * p.snd) * -sin (p.snd * π) * π + p.fst ^ p.snd * log p.fst
[PROOFSTEP]
ring
[GOAL]
case h.e'_10.h.h.e_a.e_a
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ p.snd * (p.fst ^ p.snd * p.fst⁻¹) = p.fst ^ p.snd * p.snd * p.fst⁻¹
[PROOFSTEP]
ring
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases' hp.lt_or_lt with hneg hpos
[GOAL]
case inl
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
hneg : p.fst < 0
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
case inr x y z : ℝ p : ℝ × ℝ hp : p.fst ≠ 0 n : ℕ∞ hpos : 0 < p.fst ⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
exacts
  [(((contDiffAt_fst.log hneg.ne).mul contDiffAt_snd).exp.mul
        (contDiffAt_snd.mul contDiffAt_const).cos).congr_of_eventuallyEq
    ((continuousAt_fst.eventually (gt_mem_nhds hneg)).mono fun p hp => rpow_def_of_neg hp _),
  ((contDiffAt_fst.log hpos.ne').mul contDiffAt_snd).exp.congr_of_eventuallyEq
    ((continuousAt_fst.eventually (lt_mem_nhds hpos)).mono fun p hp => rpow_def_of_pos hp _)]
[GOAL]
x y z : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x)) x
[PROOFSTEP]
convert (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x (hf.prod hg) using 1
[GOAL]
case h.e'_7
x y z : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x) =
    ↑((((fun x => (f x, g x)) x).snd * ((fun x => (f x, g x)) x).fst ^ (((fun x => (f x, g x)) x).snd - 1)) •
            ContinuousLinearMap.fst ℝ ℝ ℝ +
          (((fun x => (f x, g x)) x).fst ^ ((fun x => (f x, g x)) x).snd * log ((fun x => (f x, g x)) x).fst) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (f', g')
[PROOFSTEP]
simp [mul_assoc, mul_comm, mul_left_comm]
[GOAL]
x✝ y z x : ℝ
hx : x ≠ 0
p : ℝ
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
cases' hx.lt_or_lt with hx hx
[GOAL]
case inl
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
have :=
  (hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
    ((hasStrictDerivAt_id x).prod (hasStrictDerivAt_const _ _))
[GOAL]
case inl
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.fst ^ x.snd) ∘ fun x => (id x, p))
    (↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_7
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.fst ^ x.snd) ∘ fun x => (id x, p))
    (↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    ↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)
[PROOFSTEP]
simp
[GOAL]
case inr
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
simpa using (hasStrictDerivAt_id x).rpow (hasStrictDerivAt_const x p) hx
[GOAL]
x✝ y z a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a) x
[PROOFSTEP]
simpa using (hasStrictDerivAt_const _ _).rpow (hasStrictDerivAt_id x) ha
[GOAL]
x✝ y z a x : ℝ
ha : a < 0
⊢ HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a - exp (log a * x) * sin (x * π) * π) x
[PROOFSTEP]
simpa using
  (hasStrictFDerivAt_rpow_of_neg (a, x) ha).comp_hasStrictDerivAt x
    ((hasStrictDerivAt_const _ _).prod (hasStrictDerivAt_id _))
[GOAL]
z x✝ y x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
rcases ne_or_eq x 0 with (hx | rfl)
[GOAL]
case inl
z x✝ y x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
hx : x ≠ 0
⊢ HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
exact (hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt
[GOAL]
case inr
z x y p : ℝ
h : 0 ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0
[PROOFSTEP]
replace h : 1 ≤ p := h.neg_resolve_left rfl
[GOAL]
case inr
z x y p : ℝ
h : 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0
[PROOFSTEP]
apply hasDerivAt_of_hasDerivAt_of_ne fun x hx => (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt
[GOAL]
case inr.hf
z x y p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x => x ^ p) 0
case inr.hg z x y p : ℝ h : 1 ≤ p ⊢ ContinuousAt (fun x => p * x ^ (p - 1)) 0
[PROOFSTEP]
exacts [continuousAt_id.rpow_const (Or.inr (zero_le_one.trans h)),
  continuousAt_const.mul (continuousAt_id.rpow_const (Or.inr (sub_nonneg.2 h)))]
[GOAL]
z x y p : ℝ
n : ℕ
h : ↑n ≤ p
⊢ ContDiff ℝ ↑n fun x => x ^ p
[PROOFSTEP]
induction' n with n ihn generalizing p
[GOAL]
case zero
z x y p✝ : ℝ
n : ℕ
h✝ : ↑n ≤ p✝
p : ℝ
h : ↑Nat.zero ≤ p
⊢ ContDiff ℝ ↑Nat.zero fun x => x ^ p
[PROOFSTEP]
exact contDiff_zero.2 (continuous_id.rpow_const fun x => Or.inr <| by simpa using h)
[GOAL]
z x✝ y p✝ : ℝ
n : ℕ
h✝ : ↑n ≤ p✝
p : ℝ
h : ↑Nat.zero ≤ p
x : ℝ
⊢ 0 ≤ p
[PROOFSTEP]
simpa using h
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
[PROOFSTEP]
have h1 : 1 ≤ p := le_trans (by simp) h
[GOAL]
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
⊢ 1 ≤ ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
[PROOFSTEP]
rw [Nat.cast_succ, ← le_sub_iff_add_le] at h
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
[PROOFSTEP]
rw [contDiff_succ_iff_deriv, deriv_rpow_const' h1]
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)
[PROOFSTEP]
refine' ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩
[GOAL]
z x✝ y x p : ℝ
hx : x ≠ 0 ∨ 1 ≤ p
⊢ x ≠ 0 ∨ ↑One.one ≤ p
[PROOFSTEP]
rwa [← Nat.cast_one] at hx
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
c p : ℝ
n : ℕ∞
m : ℕ
hf : ContDiffAt ℝ (↑m) f x
h : ↑m ≤ p
⊢ ContDiffAt ℝ (↑m) (fun x => f x ^ p) x
[PROOFSTEP]
rw [← contDiffWithinAt_univ] at *
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
c p : ℝ
n : ℕ∞
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) Set.univ x
[PROOFSTEP]
exact hf.rpow_const_of_le h
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x
[PROOFSTEP]
convert (hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt using 1
[GOAL]
case h.e'_7
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    ↑((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
          (f x ^ g x * Real.log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_7
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * (1 * f') + f x ^ g x * Real.log (f x) * (1 * g')
[PROOFSTEP]
ring
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h : 0 < f x
⊢ HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hg : HasDerivWithinAt g g' Set.univ x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x
[PROOFSTEP]
exact hf.rpow hg h
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x
[PROOFSTEP]
convert (hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf using 1
[GOAL]
case h.e'_7
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'
[PROOFSTEP]
ring
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x
[PROOFSTEP]
exact hf.rpow_const hx
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =Θ[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
calc
  deriv (fun (x : ℝ) => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1) :=
    by
    filter_upwards [eventually_ne_atTop 0] with x hx
    rw [Real.deriv_rpow_const (Or.inl hx)]
  _ =Θ[atTop] fun x => x ^ (p - 1) := Asymptotics.IsTheta.const_mul_left hp Asymptotics.isTheta_rfl
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1)
[PROOFSTEP]
filter_upwards [eventually_ne_atTop 0] with x hx
[GOAL]
case h
f g : ℝ → ℝ
f' g' x✝ y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => x ^ p) x = p * x ^ (p - 1)
[PROOFSTEP]
rw [Real.deriv_rpow_const (Or.inl hx)]
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
rcases eq_or_ne p 0 with rfl | hp
[GOAL]
case inl
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)
case inr f g : ℝ → ℝ f' g' x y p✝ : ℝ s : Set ℝ p : ℝ hp : p ≠ 0 ⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
case inl => simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)
[PROOFSTEP]
case inl => simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)
[PROOFSTEP]
simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
[GOAL]
case inr
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
case inr => exact (isTheta_deriv_rpow_const_atTop hp).1
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
case inr => exact (isTheta_deriv_rpow_const_atTop hp).1
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
exact (isTheta_deriv_rpow_const_atTop hp).1
[GOAL]
t : ℝ
⊢ Tendsto (fun x => (1 + t / x) ^ x) atTop (𝓝 (exp t))
[PROOFSTEP]
apply ((Real.continuous_exp.tendsto _).comp (tendsto_mul_log_one_plus_div_atTop t)).congr' _
[GOAL]
t : ℝ
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
[PROOFSTEP]
have h₁ : (1 : ℝ) / 2 < 1 := by linarith
[GOAL]
t : ℝ
⊢ 1 / 2 < 1
[PROOFSTEP]
linarith
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
[PROOFSTEP]
have h₂ : Tendsto (fun x : ℝ => 1 + t / x) atTop (𝓝 1) := by
  simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
⊢ Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
[PROOFSTEP]
simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
[PROOFSTEP]
refine' (eventually_ge_of_tendsto_gt h₁ h₂).mono fun x hx => _
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
[PROOFSTEP]
have hx' : 0 < 1 + t / x := by linarith
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ 0 < 1 + t / x
[PROOFSTEP]
linarith
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
hx' : 0 < 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
[PROOFSTEP]
simp [mul_comm x, exp_mul, exp_log hx']
[GOAL]
t : ℝ
⊢ ∀ (x : ℕ), ((fun x => (1 + t / x) ^ x) ∘ Nat.cast) x = (1 + t / ↑x) ^ ↑x
[PROOFSTEP]
simp


[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ HasSum (fun n => 0 ^ n • a n) (a 0)
[PROOFSTEP]
convert hasSum_single (α := E) 0 fun b h => _
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0
[PROOFSTEP]
first
| simp [Nat.pos_of_ne_zero h]
| simp
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0
[PROOFSTEP]
simp [Nat.pos_of_ne_zero h]
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0
[PROOFSTEP]
simp
[GOAL]
case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
b : ℕ
h : b ≠ 0
⊢ 0 ^ b • a b = 0
[PROOFSTEP]
first
| simp [Nat.pos_of_ne_zero h]
| simp
[GOAL]
case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
b : ℕ
h : b ≠ 0
⊢ 0 ^ b • a b = 0
[PROOFSTEP]
simp [Nat.pos_of_ne_zero h]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
obtain rfl | hn := n.eq_zero_or_pos
[GOAL]
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < 0 → a k = 0
⊢ ∃ t, z ^ 0 • t = s ∧ HasSum (fun m => z ^ m • a (m + 0)) t
[PROOFSTEP]
simpa
[GOAL]
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
by_cases h : z = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
⊢ HasSum (fun m => z ^ m • a m) 0
[PROOFSTEP]
simpa [ha 0 hn, h] using hasSum_at_zero a
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
exact ⟨a n, by simp [h, hn, this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ z ^ n • a n = s
[PROOFSTEP]
simp [h, hn, this]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) (a n)
[PROOFSTEP]
simpa [h] using hasSum_at_zero fun m => a (m + n)
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
refine ⟨(z ^ n)⁻¹ • s, by field_simp [smul_smul], ?_⟩
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
⊢ z ^ n • (z ^ n)⁻¹ • s = s
[PROOFSTEP]
field_simp [smul_smul]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
[PROOFSTEP]
have h1 : ∑ i in Finset.range n, z ^ i • a i = 0 :=
  Finset.sum_eq_zero fun k hk => by simp [ha k (Finset.mem_range.mp hk)]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
k : ℕ
hk : k ∈ Finset.range n
⊢ z ^ k • a k = 0
[PROOFSTEP]
simp [ha k (Finset.mem_range.mp hk)]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
[PROOFSTEP]
have h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s := by simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m => z ^ (m + n) • a (m + n)) s
[PROOFSTEP]
simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
[PROOFSTEP]
convert h2.const_smul (z⁻¹ ^ n) using 1
[GOAL]
case h.e'_5
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (fun m => z ^ m • a (m + n)) = fun i => z⁻¹ ^ n • z ^ (i + n) • a (i + n)
[PROOFSTEP]
field_simp [pow_add, smul_smul]
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (z ^ n)⁻¹ • s = z⁻¹ ^ n • s
[PROOFSTEP]
simp only [inv_pow]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt (dslope f z₀) (fslope p) z₀
[PROOFSTEP]
have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hpd : deriv f z₀ = coeff p 1
⊢ HasFPowerSeriesAt (dslope f z₀) (fslope p) z₀
[PROOFSTEP]
have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
⊢ HasFPowerSeriesAt (dslope f z₀) (fslope p) z₀
[PROOFSTEP]
simp only [hasFPowerSeriesAt_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + z))
[PROOFSTEP]
refine hp.mono fun x hx => ?_
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
convert hasSum_single (α := E) 0 _
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • coeff p (0 + 1)
[PROOFSTEP]
intros
[GOAL]
case pos.convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ ∀ (b' : ℕ), b' ≠ 0 → x ^ b' • coeff p (b' + 1) = 0
[PROOFSTEP]
intros
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • coeff p (0 + 1)
[PROOFSTEP]
simp [*]
[GOAL]
case pos.convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
b'✝ : ℕ
x✝ : b'✝ ≠ 0
⊢ x ^ b'✝ • coeff p (b'✝ + 1) = 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by field_simp [h, _root_.pow_succ']
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n✝ : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
n : ℕ
⊢ x⁻¹ * x ^ (n + 1) = x ^ n
[PROOFSTEP]
field_simp [h, _root_.pow_succ']
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
suffices HasSum (fun n => x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)) by
  simpa [dslope, slope, h, smul_smul, hxx] using this
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
this : HasSum (fun n => x⁻¹ • x ^ (n + 1) • coeff p (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
simpa [dslope, slope, h, smul_smul, hxx] using this
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n => x⁻¹ • x ^ (n + 1) • coeff p (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
[PROOFSTEP]
simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n✝ : ℕ
z z₀ : 𝕜
n : ℕ
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀
[PROOFSTEP]
induction' n with n ih generalizing f p
[GOAL]
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f✝ g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp✝ : HasFPowerSeriesAt f✝ p✝ z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[zero] f) (fslope^[zero] p) z₀
[PROOFSTEP]
exact hp
[GOAL]
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f✝ g : 𝕜 → E
n✝ : ℕ
z z₀ : 𝕜
hp✝ : HasFPowerSeriesAt f✝ p✝ z₀
n : ℕ
ih :
  ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E},
    HasFPowerSeriesAt f p z₀ → HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[succ n] f) (fslope^[succ n] p) z₀
[PROOFSTEP]
simpa using ih (has_fpower_series_dslope_fslope hp)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ (swap dslope z₀)^[order p] f z₀ ≠ 0
[PROOFSTEP]
rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ↑(fslope^[order p] p 0) 1 ≠ 0
[PROOFSTEP]
simpa [coeff_eq_zero] using apply_order_ne_zero h
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ order p • (swap dslope z₀)^[order p] f z
[PROOFSTEP]
have hq := hasFPowerSeriesAt_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ order p • (swap dslope z₀)^[order p] f z
[PROOFSTEP]
filter_upwards [hq, hasFPowerSeriesAt_iff'.mp hp] with x hx1 hx2
[GOAL]
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
⊢ f x = (x - z₀) ^ order p • (swap dslope z₀)^[order p] f x
[PROOFSTEP]
have : ∀ k < p.order, p.coeff k = 0 := fun k hk => by simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
k : ℕ
hk : k < order p
⊢ coeff p k = 0
[PROOFSTEP]
simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk
[GOAL]
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
⊢ f x = (x - z₀) ^ order p • (swap dslope z₀)^[order p] f x
[PROOFSTEP]
obtain ⟨s, hs1, hs2⟩ := HasSum.exists_hasSum_smul_of_apply_eq_zero hx2 this
[GOAL]
case h.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
s : E
hs1 : (x - z₀) ^ order p • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • coeff p (m + order p)) s
⊢ f x = (x - z₀) ^ order p • (swap dslope z₀)^[order p] f x
[PROOFSTEP]
convert hs1.symm
[GOAL]
case h.e'_3.h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
s : E
hs1 : (x - z₀) ^ order p • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • coeff p (m + order p)) s
⊢ (swap dslope z₀)^[order p] f x = s
[PROOFSTEP]
simp only [coeff_iterate_fslope] at hx1
[GOAL]
case h.e'_3.h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
s : E
hs1 : (x - z₀) ^ order p • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • coeff p (m + order p)) s
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff p (n + order p)) ((swap dslope z₀)^[order p] f x)
⊢ (swap dslope z₀)^[order p] f x = s
[PROOFSTEP]
exact hx1.unique hs2
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
rw [eventually_nhdsWithin_iff]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
[PROOFSTEP]
have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).continuousAt
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
h2 : ContinuousAt ((swap dslope z₀)^[order p] f) z₀
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
[PROOFSTEP]
have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
h2 : ContinuousAt ((swap dslope z₀)^[order p] f) z₀
h3 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (swap dslope z₀)^[order p] f z ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
[PROOFSTEP]
filter_upwards [eq_pow_order_mul_iterate_dslope hp, h3] with z e1 e2 e3
[GOAL]
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z✝ z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
h2 : ContinuousAt ((swap dslope z₀)^[order p] f) z₀
h3 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (swap dslope z₀)^[order p] f z ≠ 0
z : 𝕜
e1 : f z = (z - z₀) ^ order p • (swap dslope z₀)^[order p] f z
e2 : (swap dslope z₀)^[order p] f z ≠ 0
e3 : z ∈ {z₀}ᶜ
⊢ f z ≠ 0
[PROOFSTEP]
simpa [e1, e2, e3] using pow_ne_zero p.order (sub_ne_zero.mpr e3)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ HasFPowerSeriesAt (fun z => f z) 0 z₀
[PROOFSTEP]
rwa [h] at hp
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
rcases hf with ⟨p, hp⟩
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
by_cases h : p = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp ))
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ HasFPowerSeriesAt (fun z => f z) 0 z₀
[PROOFSTEP]
rwa [h] at hp
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : ¬p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
exact Or.inr (hp.locally_ne_zero h)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ g z
[PROOFSTEP]
simpa [sub_eq_zero] using (hf.sub hg).eventually_eq_zero_or_eventually_ne_zero
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z
[PROOFSTEP]
simpa [sub_eq_zero] using frequently_zero_iff_eventually_zero (hf.sub hg)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOn 𝕜 f U
hg : AnalyticOn 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z
⊢ EqOn f g U
[PROOFSTEP]
have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 := hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z✝ z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOn 𝕜 f U
hg : AnalyticOn 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z
z : 𝕜
h : f z = g z
⊢ (f - g) z = 0
[PROOFSTEP]
rw [Pi.sub_apply, h, sub_self]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOn 𝕜 f U
hg : AnalyticOn 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z
hfg' : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, (f - g) z = 0
⊢ EqOn f g U
[PROOFSTEP]
simpa [sub_eq_zero] using fun z hz => (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz