internlm/Lean-Github huggingface dataset:
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
z1t : z.2 ∈ closedBall c1 t
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
have z1r : z.2 ∈ closedBall c1 r1 := Metric.closedBall_subset_closedBall tr.le z1t
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
z1r : z.2 ∈ closedBall c1 r1
⊢ ‖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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
have ds : z.1 - c0 ∈ Metric.ball (0 : ℂ) s := by
  simp only [Complex.dist_eq] at zs
  simp only [zs.1, mem_ball_zero_iff, Complex.norm_eq_abs]
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
have ds' : z.1 - c0 ∈ EMetric.ball (0 : ℂ) (ENNReal.ofReal s) := by rwa [Metric.emetric_ball]
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal 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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
have hs := (u.has_series sp sr.le z1r).hasSum ds'
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (unevenSeries' u s z.2 n) fun x => z.1 - c0) (f (c0 + (z.1 - c0), z.2))
⊢ ‖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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (unevenSeries' u s z.2 n) fun x => z.1 - c0) (f (c0 + (z.1 - c0), z.2))
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
simp only [unevenSeries_eq u sp sr.le z1r,
  FormalMultilinearSeries.apply_eq_pow_smul_coeff, add_sub_cancel, Prod.mk.eta] at hs
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
⊢ ‖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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
set g := fun n : ℕ ↦ c * (s / t) ^ n
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
⊢ ‖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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
have gs : HasSum g (c * (1 - s / t)⁻¹) := HasSum.mul_left _
  (hasSum_geometric_of_lt_one (by bound) (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 : ℂ × ℂ
zs : dist z.1 c0 < s ∧ dist z.2 c1 < s
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
⊢ ‖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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
⊢ ‖f z‖ ≤ c * (1 - s / t)⁻¹
Tactic:
apply HasSum.norm_le_of_bounded hs gs
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
⊢ ∀ (i : ℕ), ‖(z.1 - c0) ^ i • (unevenSeries u z.2).coeff i‖ ≤ g i
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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
⊢ ∀ (i : ℕ), ‖(z.1 - c0) ^ i • (unevenSeries u z.2).coeff i‖ ≤ g i
Tactic:
intro n
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
⊢ ‖(z.1 - c0) ^ n • (unevenSeries u z.2).coeff n‖ ≤ g n
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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
⊢ ‖(z.1 - c0) ^ n • (unevenSeries u z.2).coeff n‖ ≤ g n
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs] at ds
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
z1r : z.2 ∈ closedBall c1 r1
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
ds : Complex.abs (z.1 - c0) < s
⊢ ‖(z.1 - c0) ^ n • (unevenSeries u z.2).coeff n‖ ≤ g n
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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
ds : Complex.abs (z.1 - c0) < s
⊢ ‖(z.1 - c0) ^ n • (unevenSeries u z.2).coeff n‖ ≤ g n
Tactic:
simp only [norm_smul, Complex.norm_eq_abs, Complex.abs_pow,
  ←FormalMultilinearSeries.norm_apply_eq_norm_coef]
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
z1r : z.2 ∈ closedBall c1 r1
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
ds : Complex.abs (z.1 - c0) < s
⊢ Complex.abs (z.1 - c0) ^ n * ‖unevenSeries u z.2 n‖ ≤ g n
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
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
ds : Complex.abs (z.1 - c0) < s
⊢ Complex.abs (z.1 - c0) ^ n * ‖unevenSeries u z.2 n‖ ≤ g n
Tactic:
calc abs (z.1 - c0) ^ n * ‖unevenSeries u z.2 n‖
  _ ≤ s ^ n * (c * t⁻¹ ^ n) := by bound [ch n _ z1t]
  _ = c * (s ^ n * t⁻¹ ^ n) := by ring_nf
  _ = c * (s / t) ^ n := by rw [← mul_pow, ← div_eq_mul_inv]
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
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
⊢ c * (1 - s / t)⁻¹ ≥ 0
Tactic:
bound
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
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
⊢ z.2 ∈ closedBall c1 t
Tactic:
simp only [Metric.mem_closedBall]
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
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
⊢ dist z.2 c1 ≤ t
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
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
⊢ dist z.2 c1 ≤ t
Tactic:
exact le_trans zs.2.le ts.le
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
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
z1r : z.2 ∈ closedBall c1 r1
⊢ z.1 - c0 ∈ ball 0 s
Tactic:
simp only [Complex.dist_eq] at zs
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
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 : Complex.abs (z.1 - c0) < s ∧ Complex.abs (z.2 - c1) < s
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
⊢ z.1 - c0 ∈ ball 0 s
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
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 : Complex.abs (z.1 - c0) < s ∧ Complex.abs (z.2 - c1) < s
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
⊢ z.1 - c0 ∈ ball 0 s
Tactic:
simp only [zs.1, mem_ball_zero_iff, Complex.norm_eq_abs]
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
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
⊢ z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
Tactic:
rwa [Metric.emetric_ball]
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
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
⊢ 0 ≤ s / t
Tactic:
bound
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
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
z1r : z.2 ∈ closedBall c1 r1
ds : z.1 - c0 ∈ ball 0 s
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
⊢ s / t < 1
Tactic:
bound
Proof state after:
no goals