English
Derivative of the uncurry map fx ↦ f.fx.· is sum of two parts: derivative in first coordinate and derivative in slots of second coordinate.
Русский
Производная раскрученного отображения fx ↦ f.fx. обеспечивается суммой производной по первой координате и по слотовам второй координаты.
LaTeX
$$$\text{HasStrictFDerivAt}\bigl( fx \mapsto f.fx.\bigr) = \text{(sum of parts)}$$$
Lean4
/-- A continuous multilinear function `f` admits a Taylor series, whose successive terms are given
by `f.iteratedFDeriv n`. This is the point of the definition of `f.iteratedFDeriv`. -/
theorem hasFTaylorSeriesUpTo_iteratedFDeriv : HasFTaylorSeriesUpTo ⊤ f (fun v n ↦ f.iteratedFDeriv n v) := by
classical
constructor
· simp [ContinuousMultilinearMap.iteratedFDeriv]
· rintro n - x
suffices H :
curryLeft (f.iteratedFDeriv (Nat.succ n) x) =
(∑ e : Fin n ↪ ι,
((iteratedFDerivComponent f e.toEquivRange).linearDeriv (Pi.compRightL 𝕜 _ Subtype.val x)) ∘L
(Pi.compRightL 𝕜 _ Subtype.val))
by
have A :
HasFDerivAt (f.iteratedFDeriv n)
(∑ e : Fin n ↪ ι,
((iteratedFDerivComponent f e.toEquivRange).linearDeriv (Pi.compRightL 𝕜 _ Subtype.val x)) ∘L
(Pi.compRightL 𝕜 _ Subtype.val))
x :=
by
apply HasFDerivAt.fun_sum (fun s _hs ↦ ?_)
exact (ContinuousMultilinearMap.hasFDerivAt _ _).comp x (ContinuousLinearMap.hasFDerivAt _)
rwa [← H] at A
ext v m
simp only [ContinuousMultilinearMap.iteratedFDeriv, curryLeft_apply, sum_apply, iteratedFDerivComponent_apply,
Finset.univ_sigma_univ, Pi.compRightL_apply, ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
Finset.sum_apply, Function.comp_apply, linearDeriv_apply, Finset.sum_sigma']
rw [← (Equiv.embeddingFinSucc n ι).sum_comp]
congr with e
congr with k
by_cases hke : k ∈ Set.range e
· simp only [hke, ↓reduceDIte]
split_ifs with hkf
· simp only [← Equiv.succ_embeddingFinSucc_fst_symm_apply e hkf hke, Fin.cons_succ]
· obtain rfl : k = e 0 := by
rcases hke with ⟨j, rfl⟩
simpa using hkf
simp only [Function.Embedding.toEquivRange_symm_apply_self, Fin.cons_zero, Function.update, Pi.compRightL_apply]
split_ifs with h
· congr!
· exfalso
apply h
simp_rw [← Equiv.embeddingFinSucc_snd e]
· have hkf : k ∉ Set.range (Equiv.embeddingFinSucc n ι e).1 :=
by
contrapose! hke
rw [Equiv.embeddingFinSucc_fst] at hke
exact Set.range_comp_subset_range _ _ hke
simp only [hke, hkf, ↓reduceDIte, Pi.compRightL, ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
rw [Function.update_of_ne]
contrapose! hke
rw [show k = _ from Subtype.ext_iff.1 hke, Equiv.embeddingFinSucc_snd e]
exact Set.mem_range_self _
· rintro n -
apply continuous_finset_sum _ (fun e _ ↦ ?_)
exact (ContinuousMultilinearMap.coe_continuous _).comp (ContinuousLinearMap.continuous _)
