internlm/Lean-Github huggingface dataset:
Theorem: unevenTerm_eq
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
have p0 := u.has_series rp rr1 z1s
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Theorem: unevenTerm_eq
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
have p1 := u.has_series u.r1p (by rfl) z1s
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Theorem: unevenTerm_eq
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
have h := HasFPowerSeriesAt.eq_formalMultilinearSeries p0.hasFPowerSeriesAt p1.hasFPowerSeriesAt
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Theorem: unevenTerm_eq
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
clear p0 p1
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Theorem: unevenTerm_eq
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
simp only [unevenTerm, ←unevenSeries_apply, h]
Proof state after:
no goals
Theorem: unevenTerm_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 : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
⊢ r1 ≤ r1
Tactic:
rfl
Proof state after:
no goals
Theorem: unevenSeries_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 : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
⊢ z1 ∈ closedBall c1 r1 → unevenSeries' u r z1 = unevenSeries u z1
Tactic:
intro z1s
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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenSeries' u r z1 = unevenSeries u z1
Theorem: unevenSeries_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 : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenSeries' u r z1 = unevenSeries u z1
Tactic:
funext
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = unevenSeries u z1 x✝
Theorem: unevenSeries_eq
Proof 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
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = unevenSeries u z1 x✝
Tactic:
simp_rw [unevenSeries, unevenSeries', unevenTerm_eq u rp rr1 z1s,
  unevenTerm_eq u u.r1p (le_refl _) z1s]
Proof state after:
no goals
Theorem: unevenSeries_norm
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
n : ℕ
⊢ ‖unevenSeries u z1 n‖ = ‖unevenTerm u z1 n‖
Tactic:
rw [unevenSeries, unevenSeries', unevenTerm, ContinuousMultilinearMap.norm_mkPiRing]
Proof state after:
no goals
Theorem: unevenSeries_uniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Tactic:
rcases (((isCompact_sphere _ _).prod (isCompact_closedBall _ _)).bddAbove_image
  fc.norm).exists_ge 0 with ⟨b, bp, fb⟩
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ y ∈ (fun x => ‖f x‖) '' sphere c0 (r0 / 2) ×ˢ closedBall c1 s, y ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Theorem: unevenSeries_uniform_bound
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ y ∈ (fun x => ‖f x‖) '' sphere c0 (r0 / 2) ×ˢ closedBall c1 s, y ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Tactic:
simp only [Set.forall_mem_image] at fb
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Theorem: unevenSeries_uniform_bound
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Tactic:
use b + 1, (r0 / 2)⁻¹, lt_of_le_of_lt bp (lt_add_one _), inv_pos.mpr (half_pos u.r0p)
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
intro n z1 z1s
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have r0hp : r0 / 2 > 0 := by linarith [u.r0p]
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have r0hr1 : r0 / 2 ≤ r1 := _root_.trans (by linarith [u.r0p]) u.r01
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
set g := fun z0 ↦ f (z0, z1)
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have gc : ContinuousOn g (sphere c0 (r0 / 2)) :=
  ContinuousOn.comp fc (ContinuousOn.prod continuousOn_id continuousOn_const) fun z0 z0s ↦
    Set.mk_mem_prod z0s z1s
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have gb : ∀ z0, z0 ∈ sphere c0 (r0 / 2) → ‖g z0‖ ≤ b := fun z0 z0s ↦ fb (Set.mk_mem_prod z0s z1s)
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have cb := cauchy1_bound' r0hp b gc gb 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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
clear bp gc gb
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Theorem: unevenSeries_uniform_bound
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have e : (2 * π * I : ℂ)⁻¹ • (∮ z0 in C(c0, r0 / 2), (z0 - c0)⁻¹ ^ n • (z0 - c0)⁻¹ • g z0) =
    unevenTerm' u (r0 / 2) z1 n := rfl
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 : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
e : ((2 * ↑π * I)⁻¹ • ∮ (z0 : ℂ) in C(c0, r0 / 2), (z0 - c0)⁻¹ ^ n • (z0 - c0)⁻¹ • g z0) = unevenTerm' u (r0 / 2) z1 n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n