English
A variant asserting analytic-within-at for the uncurry map with a linear component.
Русский
Вариант аналитичности внутри для uncurry с линейной частью.
LaTeX
$$$AnalyticWithinAt\ 𝕜\ (\lambda p \mapsto p.2.compContinuousLinearMap p.1) t q$$$
Lean4
theorem mk' {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ℝ≥0∞}
(finite : ∀ (m : ℕ), n ≤ m → p m = 0) (pos : 0 < r)
(sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, p i fun _ ↦ y) = f (x + y)) :
HasFiniteFPowerSeriesOnBall f p x n r
where
r_le := p.radius_eq_top_of_eventually_eq_zero (Filter.eventually_atTop.mpr ⟨n, finite⟩) ▸ le_top
r_pos := pos
hasSum
hy :=
sum_eq _ hy ▸ hasSum_sum_of_ne_finset_zero fun m hm ↦ by rw [Finset.mem_range, not_lt] at hm; rw [finite m hm]; rfl
finite := finite
