English
Let f be a smooth partition of unity subordinate to an open cover U_i, and for each i, g_i is C^n on U_i. Then the finsum x ↦ ∑_i f_i(x) g_i(x) is C^n on the whole manifold.
Русский
Пусть f — гладкое разбиение единиц, подчинённое открытым множествам U_i, а для каждого i функция g_i гладна порядка n на U_i. Тогда x ↦ ∑_i f_i(x) g_i(x) гладна порядка n по всей многообразности.
LaTeX
$$If f.IsSubordinate U and each g_i is ContMDiffOn of order n on U_i, then ContMDiff I n (x -> ∑_i f_i(x) g_i(x)).$$
Lean4
/-- If `f` is a smooth partition of unity on a set `s : Set M` subordinate to a family of open sets
`U : ι → Set M` and `g : ι → M → F` is a family of functions such that `g i` is $C^n$ smooth on
`U i`, then the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is $C^n$ smooth on the whole manifold. -/
theorem contMDiff_finsum_smul {g : ι → M → F} (hf : f.IsSubordinate U) (ho : ∀ i, IsOpen (U i))
(hg : ∀ i, ContMDiffOn I 𝓘(ℝ, F) n (g i) (U i)) : ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ i, f i x • g i x :=
f.contMDiff_finsum_smul fun i _ hx => (hg i).contMDiffAt <| (ho i).mem_nhds (hf i hx)
