internlm/Lean-Github huggingface dataset:
Theorem: deriv_ne_zero_of_orderAt_eq_one
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
o : p.order = 1
fp : HasFPowerSeriesAt f p c
⊢ p.order ≠ 0
Tactic:
rw [o]
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
o : p.order = 1
fp : HasFPowerSeriesAt f p c
⊢ 1 ≠ 0
Theorem: deriv_ne_zero_of_orderAt_eq_one
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
o : p.order = 1
fp : HasFPowerSeriesAt f p c
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
Proof state after:
no goals
Theorem: deriv_ne_zero_of_orderAt_eq_one
Proof state before:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
o : orderAt f c = 1
fa : ¬AnalyticAt 𝕜 f c
⊢ deriv f c ≠ 0
Tactic:
simp only [orderAt, fa] at o
Proof state after:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : (if h : False then (choose ⋯).order else 0) = 1
⊢ deriv f c ≠ 0
Theorem: deriv_ne_zero_of_orderAt_eq_one
Proof state before:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : (if h : False then (choose ⋯).order else 0) = 1
⊢ deriv f c ≠ 0
Tactic:
rw [dif_neg] at o
Proof state after:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : 0 = 1
⊢ deriv f c ≠ 0

case neg.hnc
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : (if h : False then (choose ⋯).order else 0) = 1
⊢ ¬False
Theorem: deriv_ne_zero_of_orderAt_eq_one
Proof state before:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : 0 = 1
⊢ deriv f c ≠ 0

case neg.hnc
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : (if h : False then (choose ⋯).order else 0) = 1
⊢ ¬False
Tactic:
norm_num at o
Proof state after:
case neg.hnc
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : (if h : False then (choose ⋯).order else 0) = 1
⊢ ¬False
Theorem: deriv_ne_zero_of_orderAt_eq_one
Proof state before:
case neg.hnc
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : ¬AnalyticAt 𝕜 f c
o : (if h : False then (choose ⋯).order else 0) = 1
⊢ ¬False
Tactic:
exact not_false
Proof state after:
no goals
Theorem: leadingCoeff_of_ne_zero
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
f0 : f c ≠ 0
⊢ leadingCoeff f c = f c
Tactic:
simp only [leadingCoeff, orderAt_eq_zero f0, Function.iterate_zero_apply]
Proof state after:
no goals
Theorem: AnalyticAt.leading_approx
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
⊢ (fun z => f z - (z - c) ^ orderAt f c • leadingCoeff f c) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Tactic:
rcases fa with ⟨p, fp⟩
Proof state after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ (fun z => f z - (z - c) ^ orderAt f c • leadingCoeff f c) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ (fun z => f z - (z - c) ^ orderAt f c • leadingCoeff f c) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Tactic:
generalize ha : leadingCoeff f c = a
Proof state after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
⊢ (fun z => f z - (z - c) ^ orderAt f c • a) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
⊢ (fun z => f z - (z - c) ^ orderAt f c • a) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Tactic:
generalize hd : orderAt f c = d
Proof state after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
have ha' : (Function.swap dslope c)^[d] f c = a := by rw [← ha, ← hd, leadingCoeff]
Proof state after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
have e := fp.eq_pow_order_mul_iterate_dslope
Proof state after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ p.order • (Function.swap dslope c)^[p.order] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ p.order • (Function.swap dslope c)^[p.order] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
simp_rw [← fp.orderAt_unique, hd] at e
Proof state after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
apply Asymptotics.IsLittleO.of_isBigOWith
Proof state after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → Asymptotics.IsBigOWith c_1 (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → Asymptotics.IsBigOWith c_1 (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d
Tactic:
intro k kp
Proof state after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ Asymptotics.IsBigOWith k (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ Asymptotics.IsBigOWith k (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d
Tactic:
rw [Asymptotics.isBigOWith_iff]
Proof state after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
apply e.mp
Proof state after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
have dc : ContinuousAt ((Function.swap dslope c)^[d] f) c :=
  (fp.has_fpower_series_iterate_dslope_fslope d).analyticAt.continuousAt
Proof state after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖