English
If f is a bump cover subordinate to an index family and each f i is C^∞, then each component f.toPartitionOfUnity i is C^∞.
Русский
Если покрытие из подъядер состоит из гладких функций f_i и подчинено индексу, то каждая компонента f.toPartitionOfUnity i гладкая бесконечно дифференцируемая.
LaTeX
$$\forall i, \ ContMDiff I 𝓘(ℝ) ∞ (f^{\mathrm{PU}}_i).$$
Lean4
theorem contMDiff_toPartitionOfUnity {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH}
[TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M}
(f : BumpCovering ι M s) (hf : ∀ i, ContMDiff I 𝓘(ℝ) ∞ (f i)) (i : ι) :
ContMDiff I 𝓘(ℝ) ∞ (f.toPartitionOfUnity i) :=
(hf i).mul <|
(contMDiff_finprod_cond fun j _ => contMDiff_const.sub (hf j)) <|
by
simp only [mulSupport_one_sub]
exact f.locallyFinite
