Theorem: cauchy_on_cball_radius (Ray/Analytic/Uniform.lean)

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑r) z ↑r
Tactic:
have hd : DifferentiableOn ℂ f (closedBall z r) := by
  intro x H; exact AnalyticAt.differentiableWithinAt (h x H)
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑r) z ↑r

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑r) z ↑r
Tactic:
set p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries f z r
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries f z ↑r
⊢ HasFPowerSeriesOnBall f p z ↑r

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries f z ↑r
⊢ HasFPowerSeriesOnBall f p z ↑r
Tactic:
exact DifferentiableOn.hasFPowerSeriesOnBall hd rp
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
⊢ DifferentiableOn ℂ f (closedBall z ↑r)
Tactic:
intro x H
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
x : ℂ
H : x ∈ closedBall z ↑r
⊢ DifferentiableWithinAt ℂ f (closedBall z ↑r) x

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
x : ℂ
H : x ∈ closedBall z ↑r
⊢ DifferentiableWithinAt ℂ f (closedBall z ↑r) x
Tactic:
exact AnalyticAt.differentiableWithinAt (h x H)
State after:
no goals