English
For a continuous multilinear map, changing origin yields a new formal multilinear series equal to the original derivative series.
Русский
Для непрерывной многочленных карты изменение источника приводит к новому серийному разложению, совпадающему с исходной производной.
LaTeX
$$$ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries : (f.toFormalMultilinearSeries.changeOrigin x 1) = f.linearDeriv x$$$
Lean4
theorem changeOrigin_toFormalMultilinearSeries [DecidableEq ι] :
continuousMultilinearCurryFin1 𝕜 (∀ i, E i) F (f.toFormalMultilinearSeries.changeOrigin x 1) = f.linearDeriv x :=
by
ext y
rw [continuousMultilinearCurryFin1_apply, linearDeriv_apply, changeOrigin, FormalMultilinearSeries.sum]
cases isEmpty_or_nonempty ι
· have (l : _) : 1 + l ≠ Fintype.card ι := by rw [add_comm, Fintype.card_eq_zero]; exact Nat.succ_ne_zero _
simp_rw [Fintype.sum_empty, changeOriginSeries_support _ (this _), zero_apply _, tsum_zero]; rfl
rw [tsum_eq_single (Fintype.card ι - 1), changeOriginSeries]; swap
· intro m hm
rw [Ne, eq_tsub_iff_add_eq_of_le (by exact Fintype.card_pos), add_comm] at hm
rw [f.changeOriginSeries_support hm, zero_apply]
rw [sum_apply, ContinuousMultilinearMap.sum_apply, Fin.snoc_zero]
simp_rw [changeOriginSeriesTerm_apply]
refine
(Fintype.sum_bijective (?_ ∘ Fintype.equivFinOfCardEq (Nat.add_sub_of_le Fintype.card_pos).symm)
(.comp ?_ <| Equiv.bijective _) _ _ fun i ↦ ?_).symm
· exact (⟨{·}ᶜ, by rw [card_compl, Fintype.card_fin, Finset.card_singleton, Nat.add_sub_cancel_left]⟩)
· use fun _ _ ↦ (singleton_injective <| compl_injective <| Subtype.ext_iff.mp ·)
intro ⟨s, hs⟩
have h : #sᶜ = 1 := by rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
obtain ⟨a, ha⟩ := card_eq_one.mp h
exact ⟨a, Subtype.ext (compl_eq_comm.mp ha)⟩
rw [Function.comp_apply, Subtype.coe_mk, compl_singleton, piecewise_erase_univ, toFormalMultilinearSeries,
dif_pos (Nat.add_sub_of_le Fintype.card_pos).symm]
simp_rw [domDomCongr_apply, compContinuousLinearMap_apply, ContinuousLinearMap.proj_apply, Function.update_apply,
(Equiv.injective _).eq_iff, ite_apply]
congr
grind [Function.update_self, Function.update_of_ne]
