English
Let n be a (possibly infinite) index, and consider a family of maps φ i: E → F' i with i ranging over a finite index set. Then HasFTaylorSeriesUpToOn n (λ x i, φ i x) (λ x m, π-map of p' i x m) on s holds if and only if HasFTaylorSeriesUpToOn n (φ i) (p' i) on s for every i.
Русский
Пусть имеется семейство отображений φ_i: E → F'_i (для конечного множества индексов). Тогда HasFTaylorSeriesUpToOn n (функция-из-индексов) на s эквивалентно HasFTaylorSeriesUpToOn n для каждого компонента φ_i и p'_i на s.
LaTeX
$$$ HasFTaylorSeriesUpToOn n (\lambda x i. \phi i x) (\lambda x m. ContinuousMultilinearMap.pi (\lambda i. p' i x m)) s \ \Longleftrightarrow\ \forall i, HasFTaylorSeriesUpToOn n (\lambda x. \phi i x) (p' i) s $$$
Lean4
theorem hasFTaylorSeriesUpToOn_pi {n : WithTop ℕ∞} :
HasFTaylorSeriesUpToOn n (fun x i => φ i x) (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
∀ i, HasFTaylorSeriesUpToOn n (φ i) (p' i) s :=
by
set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
set L : ∀ m : ℕ, (∀ i, E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] ∀ i, F' i := fun m => ContinuousMultilinearMap.piₗᵢ _ _
refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
· exact h.continuousLinearMap_comp (pr i)
· ext1 i
exact (h i).zero_eq x hx
· intro m hm x hx
exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <| hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx
· intro m hm
exact (L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm
