Theorem: contDiffAt_iff_analytic_at2 (Ray/Analytic/Holomorphic.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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ ContDiffAt ℂ n f x ↔ AnalyticAt ℂ f x
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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ ContDiffAt ℂ n f x → AnalyticAt ℂ f x

case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ AnalyticAt ℂ f x → ContDiffAt ℂ n f x

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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ ContDiffAt ℂ n f x → AnalyticAt ℂ f x
Tactic:
intro d
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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d : ContDiffAt ℂ n f x
⊢ AnalyticAt ℂ f x

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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d : ContDiffAt ℂ n f x
⊢ AnalyticAt ℂ f x
Tactic:
rcases d.contDiffOn n1 with ⟨u, un, d⟩
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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
⊢ AnalyticAt ℂ f x

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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
⊢ AnalyticAt ℂ f x
Tactic:
rcases mem_nhds_iff.mp un with ⟨v, uv, vo, vx⟩
State after:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ AnalyticAt ℂ f x

State before:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ AnalyticAt ℂ f x
Tactic:
refine (differentiable_iff_analytic2 vo).mp ?_ _ vx
State after:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ DifferentiableOn ℂ f v

State before:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ DifferentiableOn ℂ f v
Tactic:
exact (d.mono uv).differentiableOn (by norm_num)
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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ 1 ≤ ↑One.one
Tactic:
norm_num
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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ AnalyticAt ℂ f x → ContDiffAt ℂ n f x
Tactic:
intro a
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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
a : AnalyticAt ℂ f x
⊢ ContDiffAt ℂ n f x

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
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
a : AnalyticAt ℂ f x
⊢ ContDiffAt ℂ n f x
Tactic:
exact a.contDiffAt.of_le le_top
State after:
no goals