Theorem: unevenSeries_strong_bound (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
rcases exists_between sr with ⟨t, ts, tr⟩
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have tp : t > 0 := _root_.trans ts sp
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have trs : closedBall c1 t ⊆ ball c1 r1 := Metric.closedBall_subset_ball tr
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have cs : closedBall c1 t ⊆ closedBall c1 r1 :=
  Metric.closedBall_subset_closedBall tr.le
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have ks : closedBall c1 s ⊆ interior (closedBall c1 t) := by
  rw [interior_closedBall _ tp.ne']; exact Metric.closedBall_subset_ball ts
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
rcases unevenLog_uniform_bound u tr with ⟨b, fb⟩
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have H := SubharmonicOn.hartogs (fun n ↦ (uneven_nonuniform_subharmonic u n).mono trs) fb
    (fun z zs ↦ unevenLog_nonuniform_bound u (cs zs)) (isCompact_closedBall _ _) ks
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ d > 0, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ d
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ d > 0, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ d
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
specialize H (r1 / s).log (by bound)
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
refine H.mp ((Filter.eventually_gt_atTop 0).mp (Filter.eventually_of_forall ?_))
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ (x : ℕ),
    0 < x →
      (∀ z ∈ closedBall c1 s, unevenLog u x z ≤ (r1 / s).log) → ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 x‖ ≤ s⁻¹ ^ x

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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ (x : ℕ),
    0 < x →
      (∀ z ∈ closedBall c1 s, unevenLog u x z ≤ (r1 / s).log) → ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 x‖ ≤ s⁻¹ ^ x
Tactic:
intro n np h z zs
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
h : ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
z : ℂ
zs : z ∈ closedBall c1 s
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
h : ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
z : ℂ
zs : z ∈ closedBall c1 s
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n
Tactic:
specialize h z zs
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n
Tactic:
rw [unevenSeries_norm]
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : unevenLog u n z ≤ (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
rw [unevenLog, inv_mul_le_iff (Nat.cast_pos.mpr np : 0 < (n : ℝ))] at h
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
simp only [norm_smul, abs_of_pos u.r1p, norm_pow, Real.norm_eq_abs] at h
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
have a := le_of_maxLog_le h
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ (↑n * (r1 / s).log).exp
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ (↑n * (r1 / s).log).exp
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
rw [Real.exp_nat_mul, Real.exp_log (div_pos u.r1p sp), div_eq_mul_inv, mul_pow] at a
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * s⁻¹ ^ n
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * s⁻¹ ^ n
⊢ ‖unevenTerm u z n‖ ≤ s⁻¹ ^ n
Tactic:
exact (mul_le_mul_left (by bound)).mp a
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ closedBall c1 s ⊆ interior (closedBall c1 t)
Tactic:
rw [interior_closedBall _ tp.ne']
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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ closedBall c1 s ⊆ ball c1 t

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 : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ closedBall c1 s ⊆ ball c1 t
Tactic:
exact Metric.closedBall_subset_ball ts
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ d > 0, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ d
⊢ (r1 / s).log > 0
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
z : ℂ
zs : z ∈ closedBall c1 s
h : maxLog (-1) (r1 ^ n * ‖unevenTerm u z n‖) ≤ ↑n * (r1 / s).log
a : r1 ^ n * ‖unevenTerm u z n‖ ≤ r1 ^ n * s⁻¹ ^ n
⊢ 0 < r1 ^ n
Tactic:
bound
State after:
no goals