case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
⊢ ∃ C r hC hr, ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
⊢ ∃ C r hC hr, ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨r, r0, rlt⟩
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
⊢ ∃ C r hC hr, ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
⊢ ∃ C r hC hr, ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
have rpos : 0 < (r : ℝ) := by simp [ENNReal.coe_pos.1 r0]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
⊢ ∃ C r hC hr, ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
⊢ ∃ C r hC hr, ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
rcases norm_le_div_pow_of_pos_of_lt_radius p rpos rlt with ⟨C, Cpos, hCp⟩
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C * (↑r)⁻¹ ^ n
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
⊢ ∃ C r hC hr, ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
refine' ⟨C, r⁻¹, Cpos, by simp only [inv_pos, rpos], fun n => _⟩
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C / ↑r ^ n
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C * (↑r)⁻¹ ^ n
rw [inv_pow, ← div_eq_mul_inv]
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C / ↑r ^ n
exact hCp n
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
⊢ 0 < ↑r
simp [ENNReal.coe_pos.1 r0]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.253075
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : 0 < radius p
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < radius p
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
⊢ 0 < (↑r)⁻¹
simp only [inv_pos, rpos]