𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
⊢ ∀ (y : E), (↑(p k) fun x => y) = 0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n : ℕ
⊢ ∀ (y : E), (↑(p n) fun x => y) = 0
refine' Nat.strong_induction_on n fun k hk => _
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
psum_eq : FormalMultilinearSeries.partialSum p (k + 1) = fun y => ↑(p k) fun x => y
h :
  (fun y => OfNat.ofNat 0 (x + y) - FormalMultilinearSeries.partialSum p (Nat.succ k) y) =O[𝓝 0] fun y =>
    ‖y‖ ^ Nat.succ k
⊢ ∀ (y : E), (↑(p k) fun x => y) = 0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
psum_eq : FormalMultilinearSeries.partialSum p (k + 1) = fun y => ↑(p k) fun x => y
⊢ ∀ (y : E), (↑(p k) fun x => y) = 0
replace h := h.isBigO_sub_partialSum_pow k.succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
psum_eq : FormalMultilinearSeries.partialSum p (k + 1) = fun y => ↑(p k) fun x => y
h : (fun x => ↑(p k) fun x_1 => x) =O[𝓝 0] fun y => ‖y‖ ^ Nat.succ k
⊢ ∀ (y : E), (↑(p k) fun x => y) = 0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
psum_eq : FormalMultilinearSeries.partialSum p (k + 1) = fun y => ↑(p k) fun x => y
h :
  (fun y => OfNat.ofNat 0 (x + y) - FormalMultilinearSeries.partialSum p (Nat.succ k) y) =O[𝓝 0] fun y =>
    ‖y‖ ^ Nat.succ k
⊢ ∀ (y : E), (↑(p k) fun x => y) = 0
simp only [psum_eq, zero_sub, Pi.zero_apply, Asymptotics.isBigO_neg_left] at h
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
psum_eq : FormalMultilinearSeries.partialSum p (k + 1) = fun y => ↑(p k) fun x => y
h : (fun x => ↑(p k) fun x_1 => x) =O[𝓝 0] fun y => ‖y‖ ^ Nat.succ k
⊢ ∀ (y : E), (↑(p k) fun x => y) = 0
exact h.continuousMultilinearMap_apply_eq_zero
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
⊢ FormalMultilinearSeries.partialSum p (k + 1) z = ↑(p k) fun x => z
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
⊢ FormalMultilinearSeries.partialSum p (k + 1) = fun y => ↑(p k) fun x => y
funext z
case h.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
⊢ (↑(p b) fun x => z) = 0

case h.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
hn : ¬k ∈ Finset.range (k + 1)
⊢ (↑(p k) fun x => z) = 0
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
⊢ FormalMultilinearSeries.partialSum p (k + 1) z = ↑(p k) fun x => z
refine' Finset.sum_eq_single _ (fun b hb hnb => _) fun hn => _
case h.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
this : b ≤ k
⊢ (↑(p b) fun x => z) = 0
case h.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
⊢ (↑(p b) fun x => z) = 0
have := Finset.mem_range_succ_iff.mp hb
no goals
case h.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
this : b ≤ k
⊢ (↑(p b) fun x => z) = 0
simp only [hk b (this.lt_of_ne hnb), Pi.zero_apply]
no goals
case h.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1119376
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ (m : ℕ), m < k → ∀ (y : E), (↑(p m) fun x => y) = 0
z : E
hn : ¬k ∈ Finset.range (k + 1)
⊢ (↑(p k) fun x => z) = 0
exact False.elim (hn (Finset.mem_range.mpr (lt_add_one k)))