English
If a SmoothBumpCovering is subordinate to U, then its smooth partition is subordinate to U via centers.
Русский
Если SmoothBumpCovering подчинён U, то его гладкое разбиение единиц подчинено U через центры.
LaTeX
$$$f.IsSubordinate U \\Rightarrow f.toSmoothPartitionOfUnity.IsSubordinate (\\lambda i, U(c(i)))$$$
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^n$ 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 $C^n$ smooth section `s : Cₛ^n⟮I_M; F_fiber, V⟯` such that
`s x ∈ t x` for all `x : M`.
-/
theorem exists_contMDiffOn_section_forall_mem_convex_of_local {F_fiber : Type*} [NormedAddCommGroup F_fiber]
[NormedSpace ℝ F_fiber] (V : M → Type*) [∀ x, AddCommGroup (V x)] [∀ x, TopologicalSpace (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)) n (fun x ↦ TotalSpace.mk' F_fiber x (s_loc x)) U_x₀) ∧
(∀ y ∈ U_x₀, s_loc y ∈ t y)) :
∃ s : Cₛ^n⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x :=
by
choose W h_nhds s_loc s_smooth h_mem_t using Hloc
let U (x : M) : Set M := interior (W x)
have hU_covers_univ : univ ⊆ ⋃ x, U x := by
intro x_pt _
simp only [mem_iUnion]
exact
⟨x_pt, mem_interior_iff_mem_nhds.mpr (h_nhds x_pt)⟩
-- Obtain a smooth partition of unity subordinate to this open cover.
obtain ⟨ρ, hρU⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ, ρ.IsSubordinate U :=
SmoothPartitionOfUnity.exists_isSubordinate I isClosed_univ U (fun x ↦ isOpen_interior) hU_covers_univ
let s x : V x := ∑ᶠ j, (ρ j x) • s_loc j x
have (j : M) : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n (fun x ↦ TotalSpace.mk' F_fiber x ((ρ j x) • (s_loc j x))) :=
by
refine ContMDiffOn.smul_section_of_tsupport ?_ isOpen_interior (hρU j) ((s_smooth j).mono interior_subset)
exact ((ρ j).contMDiff).of_le (sup_eq_left.mp rfl) |>.contMDiffOn
have hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n (fun x ↦ TotalSpace.mk' F_fiber x (s x)) :=
by
apply ContMDiff.finsum_section_of_locallyFinite ?_ this
apply ρ.locallyFinite.subset fun i x hx ↦ ?_
rw [support]
rw [mem_setOf_eq] at hx ⊢
exact left_ne_zero_of_smul hx
refine ⟨⟨s, hs⟩, fun x ↦ ?_⟩
apply (ht_conv x).finsum_mem (ρ.nonneg · x) (ρ.sum_eq_one (mem_univ x))
intro j h_ρjx_ne_zero
have h_x_in_tsupport_ρj : x ∈ tsupport (ρ j) := subset_closure (mem_support.mpr h_ρjx_ne_zero)
have h_x_in_Umap_j : x ∈ W j := interior_subset (hρU j h_x_in_tsupport_ρj)
exact h_mem_t j x h_x_in_Umap_j
