internlm/Lean-Github huggingface dataset:
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ -1 ≤ 0

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ 0 ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))

case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Tactic:
norm_num
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ 0 ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))

case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ 0 ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))

case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Tactic:
bound
Proof state after:
case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Theorem: unevenLog_uniform_bound
Proof state before:
case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Tactic:
simp only [norm_smul, abs_of_pos u.r1p, norm_pow, Real.norm_eq_abs]
Proof state after:
case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * ‖unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Theorem: unevenLog_uniform_bound
Proof state before:
case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * ‖unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Tactic:
trans r1 ^ n * (c * a ^ n)
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * (c * a ^ n)

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * (c * a ^ n)

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Tactic:
bound
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Tactic:
rw [Real.exp_nat_mul]
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Tactic:
trans (r1 * (max 1 c * a)) ^ n
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (r1 * (max 1 c * a)) ^ n

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (r1 * (max 1 c * a)) ^ n ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ (r1 * (max 1 c * a)) ^ n

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (r1 * (max 1 c * a)) ^ n ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Tactic:
simp only [mul_pow]
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ r1 ^ n * (max 1 c ^ n * a ^ n)

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (r1 * (max 1 c * a)) ^ n ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ r1 ^ n * (c * a ^ n) ≤ r1 ^ n * (max 1 c ^ n * a ^ n)

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (r1 * (max 1 c * a)) ^ n ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Tactic:
gcongr
Proof state after:
case a0
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ 0 ≤ r1 ^ n

case h.h
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ c ≤ max 1 c ^ n

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (r1 * (max 1 c * a)) ^ n ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Theorem: unevenLog_uniform_bound
Proof state before:
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : n = 0
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
simp only [n0, CharP.cast_eq_zero, inv_zero, pow_zero, one_smul, zero_mul, ge_iff_le, le_maxLog]
Proof state after:
no goals
Theorem: unevenLog_uniform_bound
Proof state before:
case a0
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ 0 ≤ r1 ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: unevenLog_uniform_bound
Proof state before:
case h.h
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ c ≤ max 1 c ^ n
Tactic:
trans max 1 c ^ 1
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ c ≤ max 1 c ^ 1

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ max 1 c ^ 1 ≤ max 1 c ^ n
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ c ≤ max 1 c ^ 1
Tactic:
simp only [pow_one, le_max_iff, le_refl, or_true_iff]
Proof state after:
no goals
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ max 1 c ^ 1 ≤ max 1 c ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: unevenLog_uniform_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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (r1 * (max 1 c * a)) ^ n ≤ (maxLog 0 (r1 * (max 1 c * a))).exp ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: unevenLog_nonuniform_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
z1s : z1 ∈ closedBall c1 r1
⊢ ∀ d > 0, ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
intro d dp
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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
rcases exists_between dp with ⟨e, ep, ed⟩
Proof state after:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
Proof state before:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
set s := r1 / e.exp
Proof state after:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
Proof state before:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
have sp : s > 0 := by bound
Proof state after:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
Proof state before:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
have sr : s < r1 := by bound
Proof state after:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
Proof state before:
case 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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
rcases unevenSeries_nonuniform_bound u sp sr z1s with ⟨c, cp, us⟩
Proof state after:
case intro.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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
Proof state before:
case intro.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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
rcases exists_nat_gt (max 1 (c.log / (d - e))) with ⟨m, mb⟩
Proof state after:
case intro.intro.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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d