case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r' : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ (fun y => f (x + y) - FormalMultilinearSeries.partialSum p n y) =O[𝓝 0] fun y => ‖y‖ ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesAt f p x
n : ℕ
⊢ (fun y => f (x + y) - FormalMultilinearSeries.partialSum p n y) =O[𝓝 0] fun y => ‖y‖ ^ n
rcases hf with ⟨r, hf⟩
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ (fun y => f (x + y) - FormalMultilinearSeries.partialSum p n y) =O[𝓝 0] fun y => ‖y‖ ^ n
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r' : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ (fun y => f (x + y) - FormalMultilinearSeries.partialSum p n y) =O[𝓝 0] fun y => ‖y‖ ^ n
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ (fun y => f (x + y) - FormalMultilinearSeries.partialSum p n y) =O[𝓝 0] fun y => ‖y‖ ^ n
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ (fun y => f (x + y) - FormalMultilinearSeries.partialSum p n y) =O[𝓝 0] fun y => ‖y‖ ^ n
obtain ⟨a, -, C, -, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
    ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
  hf.uniform_geometric_approx' h
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - FormalMultilinearSeries.partialSum p n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ (fun y => f (x + y) - FormalMultilinearSeries.partialSum p n y) =O[𝓝 0] fun y => ‖y‖ ^ n
refine' isBigO_iff.2 ⟨C * (a / r') ^ n, _⟩
case r'0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ 0 < ↑r'

case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
r'0 : 0 < ↑r'
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - FormalMultilinearSeries.partialSum p n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - FormalMultilinearSeries.partialSum p n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖
replace r'0 : 0 < (r' : ℝ)
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
r'0 : 0 < ↑r'
y : E
hy : y ∈ Metric.ball 0 ↑r'
⊢ ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a / ↑r') ^ n * ‖‖y‖ ^ n‖
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
r'0 : 0 < ↑r'
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - FormalMultilinearSeries.partialSum p n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖
filter_upwards [Metric.ball_mem_nhds (0 : E) r'0] with y hy
no goals
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
r'0 : 0 < ↑r'
y : E
hy : y ∈ Metric.ball 0 ↑r'
⊢ ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a / ↑r') ^ n * ‖‖y‖ ^ n‖
simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div] using hp y hy n
no goals
case r'0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.718032
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r✝ r'✝ : ℝ≥0∞
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp :
  ∀ (y : E),
    y ∈ Metric.ball 0 ↑r' →
      ∀ (n : ℕ), ‖f (x + y) - FormalMultilinearSeries.partialSum p n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ 0 < ↑r'
exact_mod_cast r'0