Theorem: AnalyticAt.cpow (Ray/Analytic/HolomorphicUpstream.lean)

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Tactic:
have fc : f c ≠ 0 := Complex.slitPlane_ne_zero m
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Tactic:
have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝 c] fun z ↦ Complex.exp (Complex.log (f z) * g z) := by
  refine (fa.continuousAt.eventually_ne fc).mp (Filter.eventually_of_forall ?_)
  intro z fz; simp only [fz, Complex.cpow_def, if_false]
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Tactic:
rw [analyticAt_congr e]
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => ((f z).log * g z).exp) c

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => ((f z).log * g z).exp) c
Tactic:
exact AnalyticAt.exp.comp ((fa.log m).mul ga)
State after:
no goals

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
Tactic:
refine (fa.continuousAt.eventually_ne fc).mp (Filter.eventually_of_forall ?_)
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ ∀ (x : E), f x ≠ 0 → (fun z => f z ^ g z) x = (fun z => ((f z).log * g z).exp) x

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ ∀ (x : E), f x ≠ 0 → (fun z => f z ^ g z) x = (fun z => ((f z).log * g z).exp) x
Tactic:
intro z fz
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
z : E
fz : f z ≠ 0
⊢ (fun z => f z ^ g z) z = (fun z => ((f z).log * g z).exp) z

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
z : E
fz : f z ≠ 0
⊢ (fun z => f z ^ g z) z = (fun z => ((f z).log * g z).exp) z
Tactic:
simp only [fz, Complex.cpow_def, if_false]
State after:
no goals