Theorem: unevenSeries_nonuniform_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 : 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
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

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
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

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)
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

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)
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

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
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

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
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

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⟩
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

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
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

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)
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

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)
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

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
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
Tactic:
intro n
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

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
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
Tactic:
specialize th n
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 : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n

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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Tactic:
rw [unevenSeries_eq u u.r1p (le_refl _) z1s] at th
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 : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n

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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Tactic:
generalize hy : ‖unevenSeries u z1 n‖ = y
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 : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
y : ℝ
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n

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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
y : ℝ
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n
Tactic:
rw [hy] at th
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 : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n

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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n
Tactic:
have tnz : (t : ℝ) ^ n ≠ 0 := pow_ne_zero _ (lt_trans sp st').ne'
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 : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y ≤ max 1 c * s⁻¹ ^ n

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
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y ≤ max 1 c * s⁻¹ ^ n
Tactic:
calc
  y = y * (↑t ^ n * (↑t ^ n)⁻¹) := by simp only [mul_inv_cancel tnz, mul_one]
  _ = y * ↑t ^ n * (↑t ^ n)⁻¹ := by ring
  _ ≤ c * (↑t ^ n)⁻¹ := by bound
  _ ≤ c * (s ^ n)⁻¹ := by bound
  _ = c * s⁻¹ ^ n := by simp only [inv_pow]
  _ ≤ max 1 c * s⁻¹ ^ n := by 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 : 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
⊢ s < ↑t
Tactic:
rw [← ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_lt_ofReal_iff_of_nonneg sp.le] at st
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
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : s < ↑t
⊢ s < ↑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 : 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 : s < ↑t
⊢ s < ↑t
Tactic:
exact st
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 : 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
⊢ ‖unevenSeries' u r1 z1 0‖ * ↑t ^ 0 ≥ 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 : 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
⊢ 0 < 1
Tactic:
norm_num
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 : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y = y * (↑t ^ n * (↑t ^ n)⁻¹)
Tactic:
simp only [mul_inv_cancel tnz, mul_one]
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 : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y * (↑t ^ n * (↑t ^ n)⁻¹) = y * ↑t ^ n * (↑t ^ n)⁻¹
Tactic:
ring
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 : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y * ↑t ^ n * (↑t ^ n)⁻¹ ≤ c * (↑t ^ n)⁻¹
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 : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ c * (↑t ^ n)⁻¹ ≤ c * (s ^ n)⁻¹
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 : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ c * (s ^ n)⁻¹ = c * s⁻¹ ^ n
Tactic:
simp only [inv_pow]
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 : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ c * s⁻¹ ^ n ≤ max 1 c * s⁻¹ ^ n
Tactic:
bound
State after:
no goals