English
The finsum of the partition functions combines to yield the unity decomposition.
Русский
Сумма по индексу разложения единиц даёт разложение на единицу.
LaTeX
$$$\\text{finsum}_{i} \\; fs.toSmoothPartitionOfUnity i x = 1$$$
Lean4
/-- Let `V` be a vector bundle over a σ-compact Hausdorff finite-dimensional topological manifold
`M`. Let `t : M → Set (V x)` be a family of convex sets in the fibers of `V`.
Suppose that for each point `x₀ : M` there exists a neighborhood `U_x₀` of `x₀` and a local
section `s_loc : M → V x` such that `s_loc` is $C^∞$ smooth on `U_x₀` (when viewed as a map to
the total space of the bundle) and `s_loc y ∈ t y` for all `y ∈ U_x₀`.
Then there exists a global smooth section `s : Cₛ^∞⟮I_M; F_fiber, V⟯` such that
`s x ∈ t x` for all `x : M`.
-/
theorem exists_smooth_section_forall_mem_convex_of_local {F_fiber : Type*} [NormedAddCommGroup F_fiber]
[NormedSpace ℝ F_fiber] (V : M → Type*) [∀ x, NormedAddCommGroup (V x)] [∀ x, Module ℝ (V x)]
[TopologicalSpace (TotalSpace F_fiber V)] [FiberBundle F_fiber V] [VectorBundle ℝ F_fiber V] (t : ∀ x, Set (V x))
(ht_conv : ∀ x, Convex ℝ (t x))
(Hloc :
∀ x₀ : M,
∃ U_x₀ ∈ 𝓝 x₀,
∃ (s_loc : (x : M) → V x),
(ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) ∞ (fun x ↦ TotalSpace.mk' F_fiber x (s_loc x)) U_x₀) ∧
(∀ y ∈ U_x₀, s_loc y ∈ t y)) :
∃ s : Cₛ^∞⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x :=
exists_contMDiffOn_section_forall_mem_convex_of_local I V t ht_conv Hloc
