internlm/Lean-Github huggingface dataset:
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
h : ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
z : ℂ
zs : z ∈ closedBall c1 s
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n
Tactic:
specialize h z zs
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n
Tactic:
rw [unevenSeries_norm]
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
rw [unevenLog, inv_mul_le_iff (Nat.cast_pos.mpr np : 0 < (n : ℝ))] at h
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
simp only [norm_smul, abs_of_pos u.r1p, norm_pow, Real.norm_eq_abs] at h
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
have a := le_of_maxLog_le h
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ (↑n * (r1 / s).log).exp
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ (↑n * (r1 / s).log).exp
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
rw [Real.exp_nat_mul, Real.exp_log (div_pos u.r1p sp), div_eq_mul_inv, mul_pow] at a
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * s⁻¹ ^ n
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * s⁻¹ ^ n
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
exact (mul_le_mul_left (by bound)).mp a
Proof state after:
no goals
Theorem: unevenSeries_strong_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ closedBall c1 s ⊆ interior (closedBall c1 t)
Tactic:
rw [interior_closedBall _ tp.ne']
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ closedBall c1 s ⊆ ball c1 t
Theorem: unevenSeries_strong_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ closedBall c1 s ⊆ ball c1 t
Tactic:
exact Metric.closedBall_subset_ball ts
Proof state after:
no goals
Theorem: unevenSeries_strong_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ d > 0, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ d
⊢ (r1 / s).log > 0
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_strong_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * s⁻¹ ^ n
⊢ 0 < r1 ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_strong_bound'
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
rcases Filter.eventually_atTop.mp (unevenSeries_strong_bound u sp sr) with ⟨n, h⟩
Proof state after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_strong_bound'
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
set g := fun z1 ↦ partialSups (fun k ↦ s ^ k * ‖unevenSeries u z1 k‖) n
Proof state after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_strong_bound'
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
have gc : ContinuousOn g (closedBall c1 s) := by
  apply ContinuousOn.partialSups; intro n; apply ContinuousOn.mul continuousOn_const
  apply ContinuousOn.norm
  exact (unevenSeries_analytic u n).continuousOn.mono (Metric.closedBall_subset_ball sr)
Proof state after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_strong_bound'
Proof state before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
rcases ((isCompact_closedBall _ _).bddAbove_image gc).exists_ge 0 with ⟨b, bp, gb⟩
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ y ∈ g '' closedBall c1 s, y ≤ b
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_strong_bound'
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ y ∈ g '' closedBall c1 s, y ≤ b
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
simp only [Set.forall_mem_image, partialSups_le_iff, g] at gb
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_strong_bound'
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
⊢ ∃ c ≥ 0, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
use max 1 b, le_max_of_le_right bp
Proof state after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ max 1 b * s⁻¹ ^ n
Theorem: unevenSeries_strong_bound'
Proof state before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ max 1 b * s⁻¹ ^ n
Tactic:
intro k z zs
Proof state after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k
Theorem: unevenSeries_strong_bound'
Proof state before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k
Tactic:
by_cases kn : k ≤ n
Proof state after:
case pos
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k

case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr : s < r1
n : ℕ
h : ∀ b ≥ n, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 b‖ ≤ s⁻¹ ^ b
g : ℂ → ℝ := fun z1 => (partialSups fun k => s ^ k * ‖unevenSeries u z1 k‖) n
gc : ContinuousOn g (closedBall c1 s)
b : ℝ
bp : 0 ≤ b
gb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 s → ∀ k ≤ n, s ^ k * ‖unevenSeries u x k‖ ≤ b
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : ¬k ≤ n
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k