Theorem: analyticAt_iff_eventually_differentiableAt (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 : ℂ → E
c : ℂ
⊢ AnalyticAt ℂ f c ↔ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
Tactic:
constructor
State after:
case mp
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
⊢ AnalyticAt ℂ f c → ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z

case mpr
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
⊢ (∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z) → AnalyticAt ℂ f c

State before:
case mp
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
⊢ AnalyticAt ℂ f c → ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
Tactic:
intro fa
State after:
case mp
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
fa : AnalyticAt ℂ f c
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z

State before:
case mp
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
fa : AnalyticAt ℂ f c
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
Tactic:
rcases fa.exists_ball_analyticOn with ⟨r, rp, fa⟩
State after:
case mp.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z

State before:
case mp.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
Tactic:
exact fa.differentiableOn.eventually_differentiableAt (Metric.ball_mem_nhds _ rp)
State after:
no goals

State before:
case mpr
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
⊢ (∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z) → AnalyticAt ℂ f c
Tactic:
intro d
State after:
case mpr
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
⊢ AnalyticAt ℂ f c

State before:
case mpr
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
⊢ AnalyticAt ℂ f c
Tactic:
rcases Metric.eventually_nhds_iff.mp d with ⟨r, rp, d⟩
State after:
case mpr.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
⊢ AnalyticAt ℂ f c

State before:
case mpr.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
⊢ AnalyticAt ℂ f c
Tactic:
have dr : DifferentiableOn ℂ f (ball c r) := by
  intro z zs; simp only [Metric.mem_ball] at zs; exact (d zs).differentiableWithinAt
State after:
case mpr.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
dr : DifferentiableOn ℂ f (ball c r)
⊢ AnalyticAt ℂ f c

State before:
case mpr.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
dr : DifferentiableOn ℂ f (ball c r)
⊢ AnalyticAt ℂ f c
Tactic:
rw [← analyticOn_iff_differentiableOn isOpen_ball] at dr
State after:
case mpr.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
dr : AnalyticOn ℂ f (ball c r)
⊢ AnalyticAt ℂ f c

State before:
case mpr.intro.intro
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
dr : AnalyticOn ℂ f (ball c r)
⊢ AnalyticAt ℂ f c
Tactic:
exact dr _ (Metric.mem_ball_self rp)
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 : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
⊢ DifferentiableOn ℂ f (ball c r)
Tactic:
intro z zs
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 : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
z : ℂ
zs : z ∈ ball c r
⊢ DifferentiableWithinAt ℂ f (ball c r) 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 : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
z : ℂ
zs : z ∈ ball c r
⊢ DifferentiableWithinAt ℂ f (ball c r) z
Tactic:
simp only [Metric.mem_ball] at zs
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 : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
z : ℂ
zs : dist z c < r
⊢ DifferentiableWithinAt ℂ f (ball c r) 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 : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
r : ℝ
rp : r > 0
d : ∀ ⦃y : ℂ⦄, dist y c < r → DifferentiableAt ℂ f y
z : ℂ
zs : dist z c < r
⊢ DifferentiableWithinAt ℂ f (ball c r) z
Tactic:
exact (d zs).differentiableWithinAt
State after:
no goals