Theorem: unevenLog_uniform_bound (Ray/Hartogs/Hartogs.lean)

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
⊢ ∃ b, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ b
Tactic:
rcases unevenSeries_uniform_bound u sr with ⟨c, a, _, ap, h⟩
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∃ b, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ b

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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∃ b, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ b
Tactic:
use maxLog 0 (r1 * (max 1 c * a))
State after:
case 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
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ maxLog 0 (r1 * (max 1 c * a))

State before:
case 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
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
intro n z zs
State after:
case 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
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))

State before:
case 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
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
specialize h n z zs
State after:
case 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 : ‖unevenSeries u z n‖ ≤ c * a ^ n
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))

State before:
case 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 : ‖unevenSeries u z n‖ ≤ c * a ^ n
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
simp_rw [unevenSeries_norm] at h
State after:
case 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
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))

State before:
case 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
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
rw [unevenLog]
State after:
case 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
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))

State before:
case 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
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
by_cases n0 : n = 0
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 : ℝ
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))

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 : ℝ
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))

State before:
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 : ℝ
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:
have np : n ≥ 1 := Nat.one_le_of_lt (Nat.pos_of_ne_zero n0)
State after:
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 : ℝ
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
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))

State before:
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 : ℝ
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
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
rw [inv_mul_le_iff (Nat.cast_pos.mpr (Nat.pos_of_ne_zero n0) : 0 < (n : ℝ))]
State after:
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 : ℝ
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
⊢ maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))

State before:
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 : ℝ
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
⊢ maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))
Tactic:
apply maxLog_le
State after:
case neg.yb
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 ≤ ↑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

State before:
case neg.yb
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 ≤ ↑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:
trans (0 : ℝ)
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
⊢ -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

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
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

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
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

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]
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

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)
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

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
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

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]
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

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
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

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]
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

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
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

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]
State after:
no goals

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
State after:
no goals

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
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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals