internlm/Lean-Github huggingface dataset:
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
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
Tactic:
rw [e] at cb
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 : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ 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
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 : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ 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
Tactic:
clear e g
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
cb : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ 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
cb : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
rw [unevenTerm_eq u r0hp r0hr1 (Metric.closedBall_subset_closedBall sr.le z1s)] at cb
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
cb : ‖unevenTerm u z1 n‖ ≤ 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
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
rw [unevenSeries_norm u]
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
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenTerm 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
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenTerm u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
apply _root_.trans cb
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
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ b * (r0 / 2)⁻¹ ^ 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
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ b * (r0 / 2)⁻¹ ^ n ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
bound
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
⊢ ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
Tactic:
suffices fa' : AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s) by exact fa'.continuousOn
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 : ℝ
sr : s < r1
⊢ AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
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
⊢ AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
Tactic:
refine u.a.mono (Set.prod_mono ?_ ?_)
Proof state after:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0

case refine_2
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
⊢ closedBall c1 s ⊆ ball c1 r1
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
fa' : AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
⊢ ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
Tactic:
exact fa'.continuousOn
Proof state after:
no goals
Theorem: unevenSeries_uniform_bound
Proof state before:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0
Tactic:
have rh : r0 / 2 < r0 := by linarith [u.r0p]
Proof state after:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
rh : r0 / 2 < r0
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0
Theorem: unevenSeries_uniform_bound
Proof state before:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
rh : r0 / 2 < r0
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0
Tactic:
exact _root_.trans Metric.sphere_subset_closedBall (Metric.closedBall_subset_ball rh)
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
⊢ r0 / 2 < r0
Tactic:
linarith [u.r0p]
Proof state after:
no goals
Theorem: unevenSeries_uniform_bound
Proof state before:
case refine_2
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
⊢ closedBall c1 s ⊆ ball c1 r1
Tactic:
exact Metric.closedBall_subset_ball (by linarith [u.r1p])
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
⊢ s < r1
Tactic:
linarith [u.r1p]
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)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
⊢ r0 / 2 > 0
Tactic:
linarith [u.r0p]
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)
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
⊢ r0 / 2 ≤ r0
Tactic:
linarith [u.r0p]
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
have h := (Uneven.has_series u u.r1p (le_refl _) z1s).r_le
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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
h : ENNReal.ofReal r1 ≤ (unevenSeries' u r1 z1).radius
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
h : ENNReal.ofReal r1 ≤ (unevenSeries' u r1 z1).radius
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
rw [FormalMultilinearSeries.radius, le_iSup_iff] at h
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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
h :
  ∀ (b : ℝ≥0∞),
    (∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ b) → ENNReal.ofReal r1 ≤ b
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
h :
  ∀ (b : ℝ≥0∞),
    (∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ b) → ENNReal.ofReal r1 ≤ b
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
have sr := not_le_of_lt ((ENNReal.ofReal_lt_ofReal_iff_of_nonneg sp.le).mpr sr1)
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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
h :
  ∀ (b : ℝ≥0∞),
    (∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ b) → ENNReal.ofReal r1 ≤ b
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
h :
  ∀ (b : ℝ≥0∞),
    (∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ b) → ENNReal.ofReal r1 ≤ b
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
specialize h (ENNReal.ofReal s)
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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
h :
  (∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ ENNReal.ofReal s) →
    ENNReal.ofReal r1 ≤ ENNReal.ofReal s
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
h :
  (∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ ENNReal.ofReal s) →
    ENNReal.ofReal r1 ≤ ENNReal.ofReal s
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
rw [imp_iff_not sr] at h
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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
h : ¬∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ ENNReal.ofReal s
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
h : ¬∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑i ^ n ≤ C), ↑i ≤ ENNReal.ofReal s
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
simp only [not_forall, not_le, lt_iSup_iff] at h
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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
h : ∃ x i, ∃ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑x ^ n ≤ i), ENNReal.ofReal s < ↑x
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
h : ∃ x i, ∃ (_ : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑x ^ n ≤ i), ENNReal.ofReal s < ↑x
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
rcases h with ⟨t, c, th, st⟩
Proof 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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof 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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
have st' : s < ↑t := by
  rw [← ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_lt_ofReal_iff_of_nonneg sp.le] at st
  exact st
Proof 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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof 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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
have cp : c ≥ 0 := ge_trans (th 0) (by bound)
Proof 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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof 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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
⊢ ∃ c > 0, ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
Tactic:
use max 1 c, lt_of_lt_of_le (by norm_num) (le_max_left 1 c)
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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
⊢ ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n