internlm/Lean-Github huggingface dataset:
Theorem: AnalyticManifold.punctured_nhds_neBot
Proof state before:
𝕜 : Type
inst✝²⁸ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : CompleteSpace E
inst✝²⁴ : TopologicalSpace A
F B : Type
inst✝²³ : NormedAddCommGroup F
inst✝²² : NormedSpace 𝕜 F
inst✝²¹ : CompleteSpace F
inst✝²⁰ : TopologicalSpace B
G C : Type
inst✝¹⁹ : NormedAddCommGroup G
inst✝¹⁸ : NormedSpace 𝕜 G
inst✝¹⁷ : TopologicalSpace C
H D : Type
inst✝¹⁶ : NormedAddCommGroup H
inst✝¹⁵ : NormedSpace 𝕜 H
inst✝¹⁴ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹³ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹² : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹¹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁰ : TopologicalSpace P
inst✝⁹ : I✝.Boundaryless
inst✝⁸ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝⁷ : J.Boundaryless
inst✝⁶ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁵ : K.Boundaryless
inst✝⁴ : ChartedSpace C O
co : AnalyticManifold K O
inst✝³ : L.Boundaryless
inst✝² : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝¹ : I.Boundaryless
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ¬↑(extChartAt I x).symm y ≠ x
⊢ ¬y ≠ ↑(extChartAt I x) x
Tactic:
simp only [not_not] at m h ⊢
Proof state after:
𝕜 : Type
inst✝²⁸ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : CompleteSpace E
inst✝²⁴ : TopologicalSpace A
F B : Type
inst✝²³ : NormedAddCommGroup F
inst✝²² : NormedSpace 𝕜 F
inst✝²¹ : CompleteSpace F
inst✝²⁰ : TopologicalSpace B
G C : Type
inst✝¹⁹ : NormedAddCommGroup G
inst✝¹⁸ : NormedSpace 𝕜 G
inst✝¹⁷ : TopologicalSpace C
H D : Type
inst✝¹⁶ : NormedAddCommGroup H
inst✝¹⁵ : NormedSpace 𝕜 H
inst✝¹⁴ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹³ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹² : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹¹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁰ : TopologicalSpace P
inst✝⁹ : I✝.Boundaryless
inst✝⁸ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝⁷ : J.Boundaryless
inst✝⁶ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁵ : K.Boundaryless
inst✝⁴ : ChartedSpace C O
co : AnalyticManifold K O
inst✝³ : L.Boundaryless
inst✝² : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝¹ : I.Boundaryless
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) x
Theorem: AnalyticManifold.punctured_nhds_neBot
Proof state before:
𝕜 : Type
inst✝²⁸ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : CompleteSpace E
inst✝²⁴ : TopologicalSpace A
F B : Type
inst✝²³ : NormedAddCommGroup F
inst✝²² : NormedSpace 𝕜 F
inst✝²¹ : CompleteSpace F
inst✝²⁰ : TopologicalSpace B
G C : Type
inst✝¹⁹ : NormedAddCommGroup G
inst✝¹⁸ : NormedSpace 𝕜 G
inst✝¹⁷ : TopologicalSpace C
H D : Type
inst✝¹⁶ : NormedAddCommGroup H
inst✝¹⁵ : NormedSpace 𝕜 H
inst✝¹⁴ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹³ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹² : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹¹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁰ : TopologicalSpace P
inst✝⁹ : I✝.Boundaryless
inst✝⁸ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝⁷ : J.Boundaryless
inst✝⁶ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁵ : K.Boundaryless
inst✝⁴ : ChartedSpace C O
co : AnalyticManifold K O
inst✝³ : L.Boundaryless
inst✝² : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝¹ : I.Boundaryless
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) x
Tactic:
nth_rw 2 [← h]
Proof state after:
𝕜 : Type
inst✝²⁸ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : CompleteSpace E
inst✝²⁴ : TopologicalSpace A
F B : Type
inst✝²³ : NormedAddCommGroup F
inst✝²² : NormedSpace 𝕜 F
inst✝²¹ : CompleteSpace F
inst✝²⁰ : TopologicalSpace B
G C : Type
inst✝¹⁹ : NormedAddCommGroup G
inst✝¹⁸ : NormedSpace 𝕜 G
inst✝¹⁷ : TopologicalSpace C
H D : Type
inst✝¹⁶ : NormedAddCommGroup H
inst✝¹⁵ : NormedSpace 𝕜 H
inst✝¹⁴ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹³ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹² : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹¹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁰ : TopologicalSpace P
inst✝⁹ : I✝.Boundaryless
inst✝⁸ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝⁷ : J.Boundaryless
inst✝⁶ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁵ : K.Boundaryless
inst✝⁴ : ChartedSpace C O
co : AnalyticManifold K O
inst✝³ : L.Boundaryless
inst✝² : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝¹ : I.Boundaryless
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) (↑(extChartAt I x).symm y)
Theorem: AnalyticManifold.punctured_nhds_neBot
Proof state before:
𝕜 : Type
inst✝²⁸ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : CompleteSpace E
inst✝²⁴ : TopologicalSpace A
F B : Type
inst✝²³ : NormedAddCommGroup F
inst✝²² : NormedSpace 𝕜 F
inst✝²¹ : CompleteSpace F
inst✝²⁰ : TopologicalSpace B
G C : Type
inst✝¹⁹ : NormedAddCommGroup G
inst✝¹⁸ : NormedSpace 𝕜 G
inst✝¹⁷ : TopologicalSpace C
H D : Type
inst✝¹⁶ : NormedAddCommGroup H
inst✝¹⁵ : NormedSpace 𝕜 H
inst✝¹⁴ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹³ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹² : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹¹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁰ : TopologicalSpace P
inst✝⁹ : I✝.Boundaryless
inst✝⁸ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝⁷ : J.Boundaryless
inst✝⁶ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁵ : K.Boundaryless
inst✝⁴ : ChartedSpace C O
co : AnalyticManifold K O
inst✝³ : L.Boundaryless
inst✝² : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝¹ : I.Boundaryless
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) (↑(extChartAt I x).symm y)
Tactic:
rw [PartialEquiv.right_inv _ m]
Proof state after:
no goals
Theorem: mfderiv_comp'
Proof state before:
case hf
𝕜✝ : Type
inst✝³⁹ : NontriviallyNormedField 𝕜✝
E✝ A : Type
inst✝³⁸ : NormedAddCommGroup E✝
inst✝³⁷ : NormedSpace 𝕜✝ E✝
inst✝³⁶ : CompleteSpace E✝
inst✝³⁵ : TopologicalSpace A
F B : Type
inst✝³⁴ : NormedAddCommGroup F
inst✝³³ : NormedSpace 𝕜✝ F
inst✝³² : CompleteSpace F
inst✝³¹ : TopologicalSpace B
G C : Type
inst✝³⁰ : NormedAddCommGroup G
inst✝²⁹ : NormedSpace 𝕜✝ G
inst✝²⁸ : TopologicalSpace C
H✝ D : Type
inst✝²⁷ : NormedAddCommGroup H✝
inst✝²⁶ : NormedSpace 𝕜✝ H✝
inst✝²⁵ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜✝ E✝ A
inst✝²⁴ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜✝ F B
inst✝²³ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜✝ G C
inst✝²² : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜✝ H✝ D
inst✝²¹ : TopologicalSpace P
inst✝²⁰ : I✝.Boundaryless
inst✝¹⁹ : ChartedSpace A M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁸ : J.Boundaryless
inst✝¹⁷ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝¹⁶ : K.Boundaryless
inst✝¹⁵ : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹⁴ : L.Boundaryless
inst✝¹³ : ChartedSpace D P
cp : AnalyticManifold L P
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type
inst✝⁸ : TopologicalSpace M
cs : ChartedSpace H M
E' : Type
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type
inst✝⁴ : TopologicalSpace M'
cs' : ChartedSpace H' M'
E'' : Type
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
H'' : Type
inst✝¹ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type
inst✝ : TopologicalSpace M''
cs'' : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
sm : SmoothManifoldWithCorners I M
sm' : SmoothManifoldWithCorners I' M'
sm'' : SmoothManifoldWithCorners I'' M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ MDifferentiableAt I I' (fun x => f x) x
Tactic:
assumption
Proof state after:
no goals
Theorem: analyticOn_iff_differentiableOn
Proof 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
s : Set ℂ
o : IsOpen s
⊢ AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s
Tactic:
constructor
Proof 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
s : Set ℂ
o : IsOpen s
⊢ AnalyticOn ℂ f s → DifferentiableOn ℂ f s

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
s : Set ℂ
o : IsOpen s
⊢ DifferentiableOn ℂ f s → AnalyticOn ℂ f s
Theorem: analyticOn_iff_differentiableOn
Proof 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
s : Set ℂ
o : IsOpen s
⊢ AnalyticOn ℂ f s → DifferentiableOn ℂ f s
Tactic:
exact AnalyticOn.differentiableOn
Proof state after:
no goals
Theorem: analyticOn_iff_differentiableOn
Proof 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
s : Set ℂ
o : IsOpen s
⊢ DifferentiableOn ℂ f s → AnalyticOn ℂ f s
Tactic:
intro d z zs
Proof 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
s : Set ℂ
o : IsOpen s
d : DifferentiableOn ℂ f s
z : ℂ
zs : z ∈ s
⊢ AnalyticAt ℂ f z
Theorem: analyticOn_iff_differentiableOn
Proof 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
s : Set ℂ
o : IsOpen s
d : DifferentiableOn ℂ f s
z : ℂ
zs : z ∈ s
⊢ AnalyticAt ℂ f z
Tactic:
exact DifferentiableOn.analyticAt d (o.mem_nhds zs)
Proof state after:
no goals
Theorem: analyticOn_univ_iff_differentiable
Proof 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
⊢ AnalyticOn ℂ f univ ↔ Differentiable ℂ f
Tactic:
simp only [←  differentiableOn_univ]
Proof 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
⊢ AnalyticOn ℂ f univ ↔ DifferentiableOn ℂ f univ
Theorem: analyticOn_univ_iff_differentiable
Proof 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
⊢ AnalyticOn ℂ f univ ↔ DifferentiableOn ℂ f univ
Tactic:
exact analyticOn_iff_differentiableOn isOpen_univ
Proof state after:
no goals
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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⟩
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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)
Proof state after:
no goals
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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⟩
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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)
Proof state after:
no goals
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof 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
Theorem: analyticAt_iff_eventually_differentiableAt
Proof 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
Proof state after:
no goals
Theorem: AnalyticOn.exp
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
⊢ AnalyticOn ℂ Complex.exp univ
Tactic:
rw [analyticOn_univ_iff_differentiable]
Proof state after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
⊢ Differentiable ℂ Complex.exp
Theorem: AnalyticOn.exp
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
⊢ Differentiable ℂ Complex.exp
Tactic:
exact Complex.differentiable_exp
Proof state after:
no goals
Theorem: analyticAt_log
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ AnalyticAt ℂ log c
Tactic:
rw [analyticAt_iff_eventually_differentiableAt]
Proof state after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ log z
Theorem: analyticAt_log
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ log z
Tactic:
filter_upwards [Complex.isOpen_slitPlane.eventually_mem m]
Proof state after:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ a ∈ Complex.slitPlane, DifferentiableAt ℂ log a
Theorem: analyticAt_log
Proof state before:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ a ∈ Complex.slitPlane, DifferentiableAt ℂ log a
Tactic:
intro z m
Proof state after:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m✝ : c ∈ Complex.slitPlane
z : ℂ
m : z ∈ Complex.slitPlane
⊢ DifferentiableAt ℂ log z
Theorem: analyticAt_log
Proof state before:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m✝ : c ∈ Complex.slitPlane
z : ℂ
m : z ∈ Complex.slitPlane
⊢ DifferentiableAt ℂ log z
Tactic:
exact differentiableAt_id.clog m
Proof state after:
no goals