internlm/Lean-Github huggingface dataset:
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
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‖
Tactic:
rcases Metric.continuousAt_iff.mp dc k kp with ⟨r, rp, rh⟩
Proof state after:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) ((Function.swap dslope c)^[d] f c) < 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.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) ((Function.swap dslope c)^[d] f c) < 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:
rw [ha'] at rh
Proof state after:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < 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.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < 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:
generalize hg : (Function.swap dslope c)^[d] f = g
Proof state after:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < k
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < k
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
rw [hg] at rh
Proof state after:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
rw [Metric.eventually_nhds_iff]
Proof state after:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∃ ε > 0, ∀ ⦃y : 𝕜⦄, dist y c < ε → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case intro.a.intro.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
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∃ ε > 0, ∀ ⦃y : 𝕜⦄, dist y c < ε → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
use r, rp
Proof state after:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ ⦃y : 𝕜⦄, dist y c < r → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ ⦃y : 𝕜⦄, dist y c < r → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
intro y yr fe
Proof state after:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
rw [fe]
Proof state after:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
specialize rh yr
Proof state after:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : dist (g y) a < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : dist (g y) a < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
rw [dist_eq_norm] at rh
Proof state after:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Theorem: AnalyticAt.leading_approx
Proof state before:
case right
𝕜 : 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
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
calc ‖(y - c) ^ d • g y - (y - c) ^ d • a‖
  _ = ‖(y - c) ^ d‖ * ‖g y - a‖ := by rw [←smul_sub, norm_smul]
  _ ≤ ‖(y - c) ^ d‖ * k := mul_le_mul_of_nonneg_left rh.le (norm_nonneg _)
  _ = k * ‖(y - c) ^ d‖ := by rw [mul_comm]
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 : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
⊢ (Function.swap dslope c)^[d] f c = a
Tactic:
rw [← ha, ← hd, leadingCoeff]
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 : 𝕜
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
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ = ‖(y - c) ^ d‖ * ‖g y - a‖
Tactic:
rw [←smul_sub, norm_smul]
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 : 𝕜
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
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d‖ * k = k * ‖(y - c) ^ d‖
Tactic:
rw [mul_comm]
Proof state after:
no goals