internlm/Lean-Github huggingface dataset:
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
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
Proof 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)
Theorem: unevenSeries_strong_bound'
Proof 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
Proof 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)
Theorem: unevenSeries_strong_bound'
Proof 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
Proof 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)
Theorem: unevenSeries_strong_bound'
Proof 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
Proof 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)
Theorem: unevenSeries_strong_bound'
Proof 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)
Proof state after:
no goals
Theorem: unevenSeries_strong_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 : ℝ
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
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
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
Theorem: unevenSeries_strong_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 : ℝ
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
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
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
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 : 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‖
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
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']
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
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
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
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
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
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
Proof state after:
no goals
Theorem: unevenSeries_strong_bound'
Proof 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
Proof 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
Theorem: unevenSeries_strong_bound'
Proof 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)
Proof 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
Theorem: unevenSeries_strong_bound'
Proof 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
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
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]
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
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
Proof state after:
no goals
Theorem: fst_snd_eq
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 : ℝ
A B : Type
p : A × B
⊢ (p.1, p.2) = p
Tactic:
simp only [Prod.mk.eta]
Proof state after:
no goals
Theorem: uneven_bounded
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
⊢ ∃ b ≥ 0, ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ b
Tactic:
rcases exists_between sr with ⟨t, ts, tr⟩
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
s : ℝ
sp : s > 0
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
⊢ ∃ b ≥ 0, ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ b
Theorem: uneven_bounded
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
s : ℝ
sp : s > 0
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
⊢ ∃ b ≥ 0, ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ b
Tactic:
have tp : t > 0 := _root_.trans ts sp
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
s : ℝ
sp : s > 0
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
⊢ ∃ b ≥ 0, ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ b
Theorem: uneven_bounded
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
s : ℝ
sp : s > 0
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
⊢ ∃ b ≥ 0, ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ b
Tactic:
rcases unevenSeries_strong_bound' u tp tr with ⟨c, cp, ch⟩
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
s : ℝ
sp : s > 0
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
⊢ ∃ b ≥ 0, ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ b
Theorem: uneven_bounded
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
s : ℝ
sp : s > 0
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
⊢ ∃ b ≥ 0, ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ b
Tactic:
use c * (1 - s / t)⁻¹, by bound
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
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
⊢ ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ c * (1 - s / t)⁻¹
Theorem: uneven_bounded
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
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
⊢ ∀ z ∈ ball (c0, c1) s, ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
intro 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
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : z ∈ ball (c0, c1) s
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Theorem: uneven_bounded
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
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : z ∈ ball (c0, c1) s
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
simp only [Prod.dist_eq, Metric.mem_ball, max_lt_iff] at 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
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : dist z.1 c0 < s ∧ dist z.2 c1 < s
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Theorem: uneven_bounded
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
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : dist z.1 c0 < s ∧ dist z.2 c1 < s
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
have z1t : z.2 ∈ closedBall c1 t := by
  simp only [Metric.mem_closedBall]; exact le_trans zs.2.le ts.le
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
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : dist z.1 c0 < s ∧ dist z.2 c1 < s
z1t : z.2 ∈ closedBall c1 t
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹