Theorem: HasFPowerSeriesAt.const_smul (Ray/Analytic/Analytic.lean)

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ HasFPowerSeriesAt (fun z => a • f z) (fun n => a • p n) c
Tactic:
rw [hasFPowerSeriesAt_iff] at fp ⊢
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))
Tactic:
refine fp.mp (eventually_of_forall fun z h ↦ ?_)
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))
Tactic:
simp only [FormalMultilinearSeries.coeff, ContinuousMultilinearMap.smul_apply, smul_comm _ a]
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => a • z ^ n • (p n) 1) (a • f (c + z))

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => a • z ^ n • (p n) 1) (a • f (c + z))
Tactic:
exact h.const_smul a
State after:
no goals