English
If the origin change is applied to k, then the evaluation of the origin-shifted series at y equals the original series evaluated at x+y, provided the radius condition holds.
Русский
Если выполнить перенос начала для k, то значение p.changeOrigin x при аргументе y равно p( x+y ), при условии, что радиус подходит.
LaTeX
$$p.changeOrigin x \\;\\text{ and } y: (p.changeOrigin x).sum y = p.sum (x+y)$$
Lean4
/-- Summing the series `p.changeOrigin x` at a point `y` gives back `p (x + y)`. -/
theorem changeOrigin_eval (h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius) : (p.changeOrigin x).sum y = p.sum (x + y) :=
by
have radius_pos : 0 < p.radius := lt_of_le_of_lt (zero_le _) h
have x_mem_ball : x ∈ EMetric.ball (0 : E) p.radius := mem_emetric_ball_zero_iff.2 ((le_add_right le_rfl).trans_lt h)
have y_mem_ball : y ∈ EMetric.ball (0 : E) (p.changeOrigin x).radius :=
by
refine mem_emetric_ball_zero_iff.2 (lt_of_lt_of_le ?_ p.changeOrigin_radius)
rwa [lt_tsub_iff_right, add_comm]
have x_add_y_mem_ball : x + y ∈ EMetric.ball (0 : E) p.radius :=
by
refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ h)
exact mod_cast nnnorm_add_le x y
set f : (Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) → F := fun s =>
p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ => x) fun _ => y
have hsf : Summable f := by
refine .of_nnnorm_bounded (p.changeOriginSeries_summable_aux₁ h) ?_
rintro ⟨k, l, s, hs⟩
dsimp only [Subtype.coe_mk]
exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _
have hf : HasSum f ((p.changeOrigin x).sum y) :=
by
refine HasSum.sigma_of_hasSum ((p.changeOrigin x).summable y_mem_ball).hasSum (fun k => ?_) hsf
· dsimp only [f]
refine ContinuousMultilinearMap.hasSum_eval ?_ _
have := (p.hasFPowerSeriesOnBall_changeOrigin k radius_pos).hasSum x_mem_ball
rw [zero_add] at this
refine HasSum.sigma_of_hasSum this (fun l => ?_) ?_
· simp only [changeOriginSeries, ContinuousMultilinearMap.sum_apply]
apply hasSum_fintype
· refine
.of_nnnorm_bounded (p.changeOriginSeries_summable_aux₂ (mem_emetric_ball_zero_iff.1 x_mem_ball) k) fun s => ?_
refine (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq ?_
simp
refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_)
refine
HasSum.sigma_of_hasSum (p.hasSum x_add_y_mem_ball) (fun n => ?_) (changeOriginIndexEquiv.symm.summable_iff.2 hsf)
rw [← Pi.add_def, (p n).map_add_univ (fun _ => x) fun _ => y]
simp_rw [← changeOriginSeriesTerm_changeOriginIndexEquiv_symm]
exact hasSum_fintype (fun c => f (changeOriginIndexEquiv.symm ⟨n, c⟩))
