English
For all f, s, x, y, analyticWithinAt 𝕜 f (insert y s) x is equivalent to analyticWithinAt 𝕜 f s x.
Русский
Для всех f, s, x, y: AnalyticWithinAt 𝕜 f (insert y s) x эквивалентно AnalyticWithinAt 𝕜 f s x.
LaTeX
$$$\text{AnalyticWithinAt}_{\mathcal{K}}(f,\text{insert } y\,s, x) \iff \text{AnalyticWithinAt}_{\mathcal{K}}(f,s,x)$$$
Lean4
/-- If a function admits a power series expansion within a ball, then the partial sums
`p.partialSum n z` converge to `f (x + y)` as `n → ∞` and `z → y`. Note that `x + z` doesn't need
to belong to the set where the power series expansion holds. -/
theorem tendsto_partialSum_prod {y : E} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hy : y ∈ EMetric.ball (0 : E) r)
(h'y : x + y ∈ insert x s) : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y))) :=
by
have A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y))) := by
apply (hf.tendsto_partialSum hy h'y).comp tendsto_fst
suffices Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 0) by
simpa using A.add this
apply Metric.tendsto_nhds.2 (fun ε εpos ↦ ?_)
obtain ⟨r', yr', r'r⟩ : ∃ (r' : ℝ≥0), ‖y‖₊ < r' ∧ r' < r :=
by
simp at hy
simpa using ENNReal.lt_iff_exists_nnreal_btwn.1 hy
have yr'_2 : ‖y‖ < r' := by simpa [← coe_nnnorm] using yr'
have S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n := p.summable_norm_mul_pow (r'r.trans_le hf.r_le)
obtain ⟨k, hk⟩ : ∃ k, ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4 :=
by
have : Tendsto (fun k ↦ ∑' n, ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0) := by
apply _root_.tendsto_sum_nat_add (f := fun n ↦ ‖p n‖ * ↑r' ^ n)
exact ((tendsto_order.1 this).2 _ (by linarith)).exists
have A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4 :=
by
have : ContinuousAt (fun z ↦ p.partialSum k z) y := (p.partialSum_continuous k).continuousAt
exact tendsto_snd (Metric.tendsto_nhds.1 this.tendsto (ε / 4) (by linarith))
have B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r' :=
by
suffices ∀ᶠ (z : E) in 𝓝 y, ‖z‖₊ < r' from tendsto_snd this
have : Metric.ball 0 r' ∈ 𝓝 y := Metric.isOpen_ball.mem_nhds (by simpa using yr'_2)
filter_upwards [this] with a ha using by simpa [← coe_nnnorm] using ha
have C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1 := tendsto_fst (Ici_mem_atTop _)
filter_upwards [A, B, C]
rintro ⟨n, z⟩ hz h'z hkn
simp only [dist_eq_norm, sub_zero] at hz ⊢
have I (w : E) (hw : ‖w‖₊ < r') : ‖∑ i ∈ Ico k n, p i (fun _ ↦ w)‖ ≤ ε / 4 :=
calc
‖∑ i ∈ Ico k n, p i (fun _ ↦ w)‖
_ = ‖∑ i ∈ range (n - k), p (i + k) (fun _ ↦ w)‖ :=
by
rw [sum_Ico_eq_sum_range]
congr with i
rw [add_comm k]
_ ≤ ∑ i ∈ range (n - k), ‖p (i + k) (fun _ ↦ w)‖ := (norm_sum_le _ _)
_ ≤ ∑ i ∈ range (n - k), ‖p (i + k)‖ * ‖w‖ ^ (i + k) := by gcongr with i _hi;
exact ((p (i + k)).le_opNorm _).trans_eq (by simp)
_ ≤ ∑ i ∈ range (n - k), ‖p (i + k)‖ * ↑r' ^ (i + k) := by gcongr with i _hi; simpa [← coe_nnnorm] using hw.le
_ ≤ ∑' i, ‖p (i + k)‖ * ↑r' ^ (i + k) :=
by
apply Summable.sum_le_tsum _ (fun i _hi ↦ by positivity)
apply ((_root_.summable_nat_add_iff k).2 S)
_ ≤ ε / 4 := hk.le
calc
‖p.partialSum n z - p.partialSum n y‖
_ = ‖∑ i ∈ range n, p i (fun _ ↦ z) - ∑ i ∈ range n, p i (fun _ ↦ y)‖ := rfl
_ =
‖(∑ i ∈ range k, p i (fun _ ↦ z) + ∑ i ∈ Ico k n, p i (fun _ ↦ z)) -
(∑ i ∈ range k, p i (fun _ ↦ y) + ∑ i ∈ Ico k n, p i (fun _ ↦ y))‖ :=
by simp [sum_range_add_sum_Ico _ hkn]
_ =
‖(p.partialSum k z - p.partialSum k y) + (∑ i ∈ Ico k n, p i (fun _ ↦ z)) +
(-∑ i ∈ Ico k n, p i (fun _ ↦ y))‖ :=
by
congr 1
simp only [FormalMultilinearSeries.partialSum]
abel
_ ≤ ‖p.partialSum k z - p.partialSum k y‖ + ‖∑ i ∈ Ico k n, p i (fun _ ↦ z)‖ + ‖-∑ i ∈ Ico k n, p i (fun _ ↦ y)‖ :=
norm_add₃_le
_ ≤ ε / 4 + ε / 4 + ε / 4 := by
gcongr
· exact I _ h'z
· simp only [norm_neg]; exact I _ yr'
_ < ε := by linarith
