Theorem: unevenSeries_strong_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 : ℝ
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⟩
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

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

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

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

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

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

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

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

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
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
⊢ ContinuousOn g (closedBall c1 s)
Tactic:
apply ContinuousOn.partialSups
State after:
case fc
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
⊢ ∀ (n : ℕ), ContinuousOn (fun x => s ^ n * ‖unevenSeries u x n‖) (closedBall c1 s)

State before:
case fc
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
⊢ ∀ (n : ℕ), ContinuousOn (fun x => s ^ n * ‖unevenSeries u x n‖) (closedBall c1 s)
Tactic:
intro n
State after:
case fc
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✝
n : ℕ
⊢ ContinuousOn (fun x => s ^ n * ‖unevenSeries u x n‖) (closedBall c1 s)

State before:
case fc
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✝
n : ℕ
⊢ ContinuousOn (fun x => s ^ n * ‖unevenSeries u x n‖) (closedBall c1 s)
Tactic:
apply ContinuousOn.mul continuousOn_const
State after:
case fc
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✝
n : ℕ
⊢ ContinuousOn (fun x => ‖unevenSeries u x n‖) (closedBall c1 s)

State before:
case fc
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✝
n : ℕ
⊢ ContinuousOn (fun x => ‖unevenSeries u x n‖) (closedBall c1 s)
Tactic:
apply ContinuousOn.norm
State after:
case fc.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 : ℝ
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✝
n : ℕ
⊢ ContinuousOn (fun x => unevenSeries u x n) (closedBall c1 s)

State before:
case fc.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 : ℝ
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✝
n : ℕ
⊢ ContinuousOn (fun x => unevenSeries u x n) (closedBall c1 s)
Tactic:
exact (unevenSeries_analytic u n).continuousOn.mono (Metric.closedBall_subset_ball sr)
State after:
no goals

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 : ℝ
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
Tactic:
specialize gb zs k kn
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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k

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 : ℝ
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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k
Tactic:
calc ‖unevenSeries u z k‖
  _ = s⁻¹ ^ k * (s ^ k * ‖unevenSeries u z k‖) := by ring_nf; field_simp [(pow_pos sp _).ne']
  _ ≤ s⁻¹ ^ k * b := by bound
  _ = b * s⁻¹ ^ k := by ring_nf
  _ ≤ max 1 b * s⁻¹ ^ k := by 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 : ℝ
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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ ‖unevenSeries u z k‖ = s⁻¹ ^ k * (s ^ k * ‖unevenSeries u z k‖)
Tactic:
ring_nf
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 : 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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ ‖unevenSeries u z k‖ = s ^ k * s⁻¹ ^ k * ‖unevenSeries u z k‖

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
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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ ‖unevenSeries u z k‖ = s ^ k * s⁻¹ ^ k * ‖unevenSeries u z k‖
Tactic:
field_simp [(pow_pos sp _).ne']
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 : ℝ
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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ s⁻¹ ^ k * (s ^ k * ‖unevenSeries u z k‖) ≤ s⁻¹ ^ k * b
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 : ℝ
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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ s⁻¹ ^ k * b = b * s⁻¹ ^ k
Tactic:
ring_nf
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 : ℝ
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
k : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
kn : k ≤ n
gb : s ^ k * ‖unevenSeries u z k‖ ≤ b
⊢ b * s⁻¹ ^ k ≤ max 1 b * s⁻¹ ^ k
Tactic:
bound
State after:
no goals

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 : ℝ
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
Tactic:
simp only [not_le] at kn
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 : ℝ
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 : n < k
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k

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 : ℝ
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 : n < k
⊢ ‖unevenSeries u z k‖ ≤ max 1 b * s⁻¹ ^ k
Tactic:
apply le_trans (h k kn.le z zs)
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 : ℝ
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 : n < k
⊢ s⁻¹ ^ k ≤ max 1 b * s⁻¹ ^ k

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 : ℝ
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 : n < k
⊢ s⁻¹ ^ k ≤ max 1 b * s⁻¹ ^ k
Tactic:
calc s⁻¹ ^ k
  _ = 1 * s⁻¹ ^ k := by simp only [one_mul]
  _ ≤ max 1 b * s⁻¹ ^ k := by 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 : ℝ
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 : n < k
⊢ s⁻¹ ^ k = 1 * s⁻¹ ^ k
Tactic:
simp only [one_mul]
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 : ℝ
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 : n < k
⊢ 1 * s⁻¹ ^ k ≤ max 1 b * s⁻¹ ^ k
Tactic:
bound
State after:
no goals