English
The origin is a polynomial in the shifted series: CPolynomialAt 𝕜 (fun x => p.changeOrigin x k) 0.
Русский
Происхождение образует полином в лагере: CPolynomialAt 𝕜 (fun x => p.changeOrigin x k) 0.
LaTeX
$$CPolynomialAt 𝕜 (\\lambda x. p.changeOrigin x k) 0$$
Lean4
theorem changeOrigin_eval_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0)
(x y : E) : (p.changeOrigin x).sum y = p.sum (x + y) :=
by
let f (s : Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) : F :=
p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) fun _ ↦ y
have finsupp : f.support.Finite :=
by
apply Set.Finite.subset (s := changeOriginIndexEquiv ⁻¹' (Sigma.fst ⁻¹' {m | m < n}))
· apply Set.Finite.preimage (Equiv.injective _).injOn
simp_rw [← {m | m < n}.iUnion_of_singleton_coe, preimage_iUnion, ← range_sigmaMk]
exact finite_iUnion fun _ ↦ finite_range _
· refine fun s ↦ Not.imp_symm fun hs ↦ ?_
simp only [preimage_setOf_eq, changeOriginIndexEquiv_apply_fst, mem_setOf, not_lt] at hs
dsimp only [f]
rw [changeOriginSeriesTerm_bound p hn _ _ _ hs, ContinuousMultilinearMap.zero_apply,
ContinuousMultilinearMap.zero_apply]
have hfkl k l : HasSum (f ⟨k, l, ·⟩) (changeOriginSeries p k l (fun _ ↦ x) fun _ ↦ y) := by
simp_rw [changeOriginSeries, ContinuousMultilinearMap.sum_apply]; apply hasSum_fintype
have hfk k : HasSum (f ⟨k, ·⟩) (changeOrigin p x k fun _ ↦ y) :=
by
have (m) (hm : m ∉ Finset.range n) : changeOriginSeries p k m (fun _ ↦ x) = 0 :=
by
rw [Finset.mem_range, not_lt] at hm
rw [changeOriginSeries_finite_of_finite _ hn _ (le_add_of_le_right hm), ContinuousMultilinearMap.zero_apply]
rw [changeOrigin, FormalMultilinearSeries.sum, ContinuousMultilinearMap.tsum_eval (summable_of_ne_finset_zero this)]
refine
(summable_of_ne_finset_zero (s := Finset.range n) fun m hm ↦ ?_).hasSum.sigma_of_hasSum (hfkl k)
(summable_of_finite_support <| finsupp.preimage sigma_mk_injective.injOn)
rw [this m hm, ContinuousMultilinearMap.zero_apply]
have hf : HasSum f ((p.changeOrigin x).sum y) :=
((p.changeOrigin x).hasSum_of_finite (fun _ ↦ changeOrigin_finite_of_finite p hn) _) |>.sigma_of_hasSum hfk
(summable_of_finite_support finsupp)
refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_)
refine
(p.hasSum_of_finite hn (x + y)).sigma_of_hasSum (fun n ↦ ?_)
(changeOriginIndexEquiv.symm.summable_iff.2 hf.summable)
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⟩)
