From d675989c0935a2b323077f5ffa608862daa7bd14 Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Fri, 16 May 2025 19:46:15 -0400 Subject: [PATCH 01/13] add existence of global C^n smooth section for nontrivial bundles --- .../Geometry/Manifold/PartitionOfUnity.lean | 135 +++++++++++++++++- 1 file changed, 133 insertions(+), 2 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index a648b429e2fae5..1c9960443b149e 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -5,6 +5,7 @@ Authors: Yury Kudryashov -/ import Mathlib.Geometry.Manifold.Algebra.Structures import Mathlib.Geometry.Manifold.BumpFunction +import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection import Mathlib.Topology.MetricSpace.PartitionOfUnity import Mathlib.Topology.ShrinkingLemma @@ -58,7 +59,7 @@ smooth bump function, partition of unity universe uι uE uH uM uF -open Function Filter Module Set +open Bundle Function Filter Module Set open scoped Topology Manifold ContDiff noncomputable section @@ -588,7 +589,7 @@ variable [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞} /-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood `U ∈ 𝓝 x` and a function `g : M → F` such that `g` is $C^n$ smooth on `U` and `g y ∈ t y` for all -`y ∈ U`. Then there exists a $C^n$ smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` +`y ∈ U`. Then there exists a $C^n$ smooth function `g : C^n⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. See also `exists_smooth_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local_const`. -/ theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) @@ -625,6 +626,136 @@ theorem exists_smooth_forall_mem_convex_of_local_const (ht : ∀ x, Convex ℝ ( let ⟨c, hc⟩ := Hloc x ⟨_, hc, fun _ => c, contMDiffOn_const, fun _ => id⟩ +/-- 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`. + +This theorem is a version of `exists_contMDiffOn_forall_mem_convex_of_local` for sections of a +vector bundle. It uses a partition of unity to glue together local sections. +-/ +theorem exists_contMDiff_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)) n + (fun x => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) 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 U_map h_nhds s_loc h_smooth_s_loc h_mem_t using Hloc + + -- Construct an open cover from the interiors of the given neighborhoods. + let U_open_cover (x : M) : Set M := interior (U_map x) + have hU_isOpen : ∀ x, IsOpen (U_open_cover x) := fun x ↦ isOpen_interior + have hU_covers_univ : univ ⊆ ⋃ x, U_open_cover x := by + intro x_pt _ + simp only [mem_iUnion, mem_univ] + 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ρ_subord⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ, + ρ.IsSubordinate U_open_cover := + SmoothPartitionOfUnity.exists_isSubordinate + I isClosed_univ U_open_cover hU_isOpen hU_covers_univ + + -- Define the global section `s_val` by taking a weighted sum of the local sections. + let s_val (x : M) : V x := ∑ᶠ (j : M), (ρ j x) • (s_loc j x) + + -- Prove that `s_val`, when viewed as a map to the total space, is smooth. + have hs_val_tot_space_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n + (fun x => (TotalSpace.mk x (s_val x) : TotalSpace F_fiber V)) := by + intro x₀ + -- To show `s_val` is smooth at `x₀`, we show its representation in a trivialization is smooth. + apply (Bundle.contMDiffAt_section s_val x₀).mpr + let e₀ := trivializationAt F_fiber V x₀ + apply ContMDiffAt.congr_of_eventuallyEq + -- First, show that the sum defining `s_val` (composed with the trivialization) is smooth. + -- This follows from the smoothness of each `ρ j • s_loc j` in its chart. + · apply ρ.contMDiffAt_finsum + intro j h_x₀_in_tsupport_ρj + have h_x₀_in_Umap_j_interior : x₀ ∈ interior (U_map j) := hρ_subord j h_x₀_in_tsupport_ρj + have h_x₀_in_Umap_j : x₀ ∈ U_map j := interior_subset h_x₀_in_Umap_j_interior + + have h_slocj_smooth_at_x₀ : ContMDiffAt I (I.prod 𝓘(ℝ, F_fiber)) n + (fun x => (TotalSpace.mk x (s_loc j x) : TotalSpace F_fiber V)) x₀ := + (h_smooth_s_loc j).contMDiffAt + (mem_interior_iff_mem_nhds.mp (hρ_subord j h_x₀_in_tsupport_ρj)) + -- The local section `s_loc j` is smooth on `U_map j`, which contains `x₀`. + exact (contMDiffAt_section (s_loc j) x₀).mp h_slocj_smooth_at_x₀ + -- Second, show that `(e₀ ⟨x, s_val x⟩).2` is eventually equal to the sum of trivialized local + -- sections. This relies on the linearity of the trivialization map `e₀` on its base set. + · have : (fun x ↦ (e₀ ⟨x, s_val x⟩).2) + =ᶠ[𝓝 x₀] + fun x ↦ ∑ᶠ i, ρ i x • (e₀ ⟨x, s_loc i x⟩).2 := by + -- `x₀` is in `e₀.baseSet`, which is open. + have h_base : {x : M | x ∈ e₀.baseSet} ∈ (𝓝 x₀) := + e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀) + -- Shrink to a neighborhood where: + -- 1. Only finitely many `ρ i x` (those in `ρ.finsupport x₀`) are non-zero. + -- 2. `x` is in `e₀.baseSet` (for linearity of `e₀`). + filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x hx_subset hx_base + -- The map `y ↦ (e₀ ⟨x, y⟩).2` is linear on the fiber at `x`. + have hlin : IsLinearMap ℝ (fun y ↦ (e₀ ⟨x, y⟩).2) := e₀.linear ℝ hx_base + -- The set of indices `i` for which `ρ i x • s_loc i x` is non-zero is finite. + have hfin : {i | (ρ i x • s_loc i x) ≠ 0}.Finite := by + refine (ρ.locallyFinite.point_finite x).subset ?_ + intro i hi + by_cases hρ_eq_zero : ρ i x = 0 + · simp only [ne_eq, smul_eq_zero, not_or, mem_setOf_eq, hρ_eq_zero, not_true_eq_false, + false_and] at hi + · exact hρ_eq_zero + -- Construct the linear map explicitly to use `map_finsum`. + let Llin : V x →ₗ[ℝ] F_fiber := + { toFun := fun y ↦ (e₀ ⟨x, y⟩).2 + map_add' := by intro u v; simpa using hlin.map_add u v + map_smul' := by intro c u; simpa using hlin.map_smul c u } + -- Push the sum through the linear map. + have h_map : + (fun y ↦ (e₀ ⟨x, y⟩).2) (∑ᶠ i, ρ i x • s_loc i x) = + ∑ᶠ i, ρ i x • (fun y ↦ (e₀ ⟨x, y⟩).2) (s_loc i x) := by + simpa only [LinearMap.toAddMonoidHom_coe, map_smul] using + Llin.toAddMonoidHom.map_finsum hfin + exact h_map + exact this + + -- Construct the smooth section and prove it lies in the convex sets `t x`. + refine ⟨⟨s_val, hs_val_tot_space_smooth⟩, fun x => ?_⟩ + apply (ht_conv x).finsum_mem (fun j => ρ.nonneg j 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 ∈ U_map j := interior_subset (hρ_subord j h_x_in_tsupport_ρj) + exact h_mem_t j x h_x_in_Umap_j + +/-- 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`. + +This theorem is a version of `exists_smooth_forall_mem_convex_of_local` for sections of a +vector bundle. It uses a partition of unity to glue together local sections. +-/ +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 => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_x₀) ∧ + (∀ y ∈ U_x₀, s_loc y ∈ t y)) : + ∃ s : Cₛ^∞⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x := + exists_contMDiff_section_forall_mem_convex_of_local I V t ht_conv Hloc + /-- Let `M` be a smooth σ-compact manifold with extended distance. Let `K : ι → Set M` be a locally finite family of closed sets, let `U : ι → Set M` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there exists a positive smooth function `δ : M → ℝ≥0` such that for any `i` and From 367368da958c78c0916354d539d8f4e450d67dda Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Fri, 16 May 2025 19:57:08 -0400 Subject: [PATCH 02/13] remove unused haves --- Mathlib/Geometry/Manifold/PartitionOfUnity.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 1c9960443b149e..08cbe54fd7561c 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -679,9 +679,6 @@ theorem exists_contMDiff_section_forall_mem_convex_of_local -- This follows from the smoothness of each `ρ j • s_loc j` in its chart. · apply ρ.contMDiffAt_finsum intro j h_x₀_in_tsupport_ρj - have h_x₀_in_Umap_j_interior : x₀ ∈ interior (U_map j) := hρ_subord j h_x₀_in_tsupport_ρj - have h_x₀_in_Umap_j : x₀ ∈ U_map j := interior_subset h_x₀_in_Umap_j_interior - have h_slocj_smooth_at_x₀ : ContMDiffAt I (I.prod 𝓘(ℝ, F_fiber)) n (fun x => (TotalSpace.mk x (s_loc j x) : TotalSpace F_fiber V)) x₀ := (h_smooth_s_loc j).contMDiffAt From a8f43206d9a14ae69cb90c088a7c0e5e35d17fe2 Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Fri, 16 May 2025 23:34:48 -0400 Subject: [PATCH 03/13] let's actually pull this result out --- .../Geometry/Manifold/PartitionOfUnity.lean | 111 ++++++++++-------- 1 file changed, 60 insertions(+), 51 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 08cbe54fd7561c..aa1ec70cd8a689 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -582,6 +582,61 @@ theorem exists_isSubordinate_chartAt_source : apply exists_isSubordinate _ isClosed_univ _ (fun i ↦ (chartAt H _).open_source) (fun x _ ↦ ?_) exact mem_iUnion_of_mem x (mem_chart_source H x) +/-- +Let `ρ` be a smooth partition of unity subordinate to an open cover `U`. +Let `s_loc` be a family of local sections, where each `s_loc i` is $C^n$ smooth on `U i` +(when viewed as a map to the total space of the bundle). +Then the global section `x ↦ ∑ᶠ i, ρ i x • s_loc i x`, when viewed as a map to the total space, +is $C^n$ smooth. +-/ +theorem contMDiff_totalSpace_weighted_sum_of_local_sections + {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] + {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} + [TopologicalSpace M] [ChartedSpace H M] + {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] + {n : ℕ∞} {ι : Type*} (ρ : SmoothPartitionOfUnity ι I M univ) (s_loc : ι → ((x : M) → V x)) + (U : ι → Set M) (hU_isOpen : ∀ i, IsOpen (U i)) (hρ_subord : ρ.IsSubordinate U) + (h_smooth_s_loc : ∀ i, ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) n + (fun x => (TotalSpace.mk x (s_loc i x) : TotalSpace F_fiber V)) (U i)) : + ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n + (fun x => (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by + let s_val (x : M) : V x := ∑ᶠ (j : ι), (ρ j x) • (s_loc j x) + intro x₀ + apply (Bundle.contMDiffAt_section s_val x₀).mpr + let e₀ := trivializationAt F_fiber V x₀ + apply ContMDiffAt.congr_of_eventuallyEq + · apply ρ.contMDiffAt_finsum + · intro j h_x₀_in_tsupport_ρj + have h_slocj_smooth_at_x₀ : ContMDiffAt I (I.prod 𝓘(ℝ, F_fiber)) n + (fun x => (TotalSpace.mk x (s_loc j x) : TotalSpace F_fiber V)) x₀ := + (h_smooth_s_loc j).contMDiffAt ((hU_isOpen j).mem_nhds (hρ_subord j h_x₀_in_tsupport_ρj)) + exact (contMDiffAt_section (s_loc j) x₀).mp h_slocj_smooth_at_x₀ + · have : (fun x ↦ (e₀ ⟨x, s_val x⟩).2) + =ᶠ[𝓝 x₀] + fun x ↦ ∑ᶠ i, ρ i x • (e₀ ⟨x, s_loc i x⟩).2 := by + have h_base : {x : M | x ∈ e₀.baseSet} ∈ (𝓝 x₀) := + e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀) + filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x _ hx_base + have hlin : IsLinearMap ℝ (fun y ↦ (e₀ ⟨x, y⟩).2) := e₀.linear ℝ hx_base + have hfin : {i : ι | (ρ i x • s_loc i x) ≠ 0}.Finite := by + refine (ρ.locallyFinite.point_finite x).subset fun i hi_smul_ne_zero => ?_ + contrapose! hi_smul_ne_zero + simp [hi_smul_ne_zero] + exact fun a ↦ False.elim (hi_smul_ne_zero a) + let Llin : V x →ₗ[ℝ] F_fiber := + { toFun := fun y ↦ (e₀ ⟨x, y⟩).2 + map_add' := by intro u v; simpa using hlin.map_add u v + map_smul' := by intro c u; simpa using hlin.map_smul c u } + have h_map : + (fun y ↦ (e₀ ⟨x, y⟩).2) (∑ᶠ i, ρ i x • s_loc i x) = + ∑ᶠ i, ρ i x • (fun y ↦ (e₀ ⟨x, y⟩).2) (s_loc i x) := by + simpa only [LinearMap.toAddMonoidHom_coe, map_smul] using + Llin.toAddMonoidHom.map_finsum hfin + exact h_map + exact this + end SmoothPartitionOfUnity variable [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞} @@ -648,7 +703,7 @@ theorem exists_contMDiff_section_forall_mem_convex_of_local (fun x => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) 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 U_map h_nhds s_loc h_smooth_s_loc h_mem_t using Hloc + choose U_map h_nhds s_loc h_smooth_s_loc_on_U_map h_mem_t using Hloc -- Construct an open cover from the interiors of the given neighborhoods. let U_open_cover (x : M) : Set M := interior (U_map x) @@ -670,56 +725,10 @@ theorem exists_contMDiff_section_forall_mem_convex_of_local -- Prove that `s_val`, when viewed as a map to the total space, is smooth. have hs_val_tot_space_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n (fun x => (TotalSpace.mk x (s_val x) : TotalSpace F_fiber V)) := by - intro x₀ - -- To show `s_val` is smooth at `x₀`, we show its representation in a trivialization is smooth. - apply (Bundle.contMDiffAt_section s_val x₀).mpr - let e₀ := trivializationAt F_fiber V x₀ - apply ContMDiffAt.congr_of_eventuallyEq - -- First, show that the sum defining `s_val` (composed with the trivialization) is smooth. - -- This follows from the smoothness of each `ρ j • s_loc j` in its chart. - · apply ρ.contMDiffAt_finsum - intro j h_x₀_in_tsupport_ρj - have h_slocj_smooth_at_x₀ : ContMDiffAt I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x => (TotalSpace.mk x (s_loc j x) : TotalSpace F_fiber V)) x₀ := - (h_smooth_s_loc j).contMDiffAt - (mem_interior_iff_mem_nhds.mp (hρ_subord j h_x₀_in_tsupport_ρj)) - -- The local section `s_loc j` is smooth on `U_map j`, which contains `x₀`. - exact (contMDiffAt_section (s_loc j) x₀).mp h_slocj_smooth_at_x₀ - -- Second, show that `(e₀ ⟨x, s_val x⟩).2` is eventually equal to the sum of trivialized local - -- sections. This relies on the linearity of the trivialization map `e₀` on its base set. - · have : (fun x ↦ (e₀ ⟨x, s_val x⟩).2) - =ᶠ[𝓝 x₀] - fun x ↦ ∑ᶠ i, ρ i x • (e₀ ⟨x, s_loc i x⟩).2 := by - -- `x₀` is in `e₀.baseSet`, which is open. - have h_base : {x : M | x ∈ e₀.baseSet} ∈ (𝓝 x₀) := - e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀) - -- Shrink to a neighborhood where: - -- 1. Only finitely many `ρ i x` (those in `ρ.finsupport x₀`) are non-zero. - -- 2. `x` is in `e₀.baseSet` (for linearity of `e₀`). - filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x hx_subset hx_base - -- The map `y ↦ (e₀ ⟨x, y⟩).2` is linear on the fiber at `x`. - have hlin : IsLinearMap ℝ (fun y ↦ (e₀ ⟨x, y⟩).2) := e₀.linear ℝ hx_base - -- The set of indices `i` for which `ρ i x • s_loc i x` is non-zero is finite. - have hfin : {i | (ρ i x • s_loc i x) ≠ 0}.Finite := by - refine (ρ.locallyFinite.point_finite x).subset ?_ - intro i hi - by_cases hρ_eq_zero : ρ i x = 0 - · simp only [ne_eq, smul_eq_zero, not_or, mem_setOf_eq, hρ_eq_zero, not_true_eq_false, - false_and] at hi - · exact hρ_eq_zero - -- Construct the linear map explicitly to use `map_finsum`. - let Llin : V x →ₗ[ℝ] F_fiber := - { toFun := fun y ↦ (e₀ ⟨x, y⟩).2 - map_add' := by intro u v; simpa using hlin.map_add u v - map_smul' := by intro c u; simpa using hlin.map_smul c u } - -- Push the sum through the linear map. - have h_map : - (fun y ↦ (e₀ ⟨x, y⟩).2) (∑ᶠ i, ρ i x • s_loc i x) = - ∑ᶠ i, ρ i x • (fun y ↦ (e₀ ⟨x, y⟩).2) (s_loc i x) := by - simpa only [LinearMap.toAddMonoidHom_coe, map_smul] using - Llin.toAddMonoidHom.map_finsum hfin - exact h_map - exact this + apply SmoothPartitionOfUnity.contMDiff_totalSpace_weighted_sum_of_local_sections I V ρ s_loc + U_open_cover hU_isOpen hρ_subord + intro j + exact (h_smooth_s_loc_on_U_map j).mono interior_subset -- Construct the smooth section and prove it lies in the convex sets `t x`. refine ⟨⟨s_val, hs_val_tot_space_smooth⟩, fun x => ?_⟩ From 2025fc6685136a4bf4e63954c139879694b68469 Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Sat, 17 May 2025 01:02:18 -0400 Subject: [PATCH 04/13] replace with simp only here --- Mathlib/Geometry/Manifold/PartitionOfUnity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index aa1ec70cd8a689..2c90576f363006 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -623,7 +623,7 @@ theorem contMDiff_totalSpace_weighted_sum_of_local_sections have hfin : {i : ι | (ρ i x • s_loc i x) ≠ 0}.Finite := by refine (ρ.locallyFinite.point_finite x).subset fun i hi_smul_ne_zero => ?_ contrapose! hi_smul_ne_zero - simp [hi_smul_ne_zero] + simp only [ne_eq, smul_eq_zero, not_or, mem_setOf_eq, not_and, not_not] exact fun a ↦ False.elim (hi_smul_ne_zero a) let Llin : V x →ₗ[ℝ] F_fiber := { toFun := fun y ↦ (e₀ ⟨x, y⟩).2 From ed2c6d376e429f5f5a132871b745e99f098b4f6e Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Sat, 17 May 2025 10:47:58 -0400 Subject: [PATCH 05/13] redo proof of exists_contMDiffOn_forall_mem_convex_of_local --- .../Geometry/Manifold/PartitionOfUnity.lean | 101 ++++++++++-------- 1 file changed, 55 insertions(+), 46 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 2c90576f363006..508fd3f02c188e 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -641,46 +641,6 @@ end SmoothPartitionOfUnity variable [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞} -/-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` -be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood -`U ∈ 𝓝 x` and a function `g : M → F` such that `g` is $C^n$ smooth on `U` and `g y ∈ t y` for all -`y ∈ U`. Then there exists a $C^n$ smooth function `g : C^n⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` -for all `x`. See also `exists_smooth_forall_mem_convex_of_local` and -`exists_smooth_forall_mem_convex_of_local_const`. -/ -theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) - (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) : - ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by - choose U hU g hgs hgt using Hloc - obtain ⟨f, hf⟩ := - SmoothPartitionOfUnity.exists_isSubordinate I isClosed_univ (fun x => interior (U x)) - (fun x => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩ - refine ⟨⟨fun x => ∑ᶠ i, f i x • g i x, - hf.contMDiff_finsum_smul (fun i => isOpen_interior) fun i => (hgs i).mono interior_subset⟩, - fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ ?_) (ht _)⟩ - exact interior_subset (hf _ <| subset_closure hi) - -/-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` -be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood -`U ∈ 𝓝 x` and a function `g : M → F` such that `g` is smooth on `U` and `g y ∈ t y` for all `y ∈ U`. -Then there exists a smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. -See also `exists_contMDiffOn_forall_mem_convex_of_local` and -`exists_smooth_forall_mem_convex_of_local_const`. -/ -theorem exists_smooth_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) - (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) ∞ g U ∧ ∀ y ∈ U, g y ∈ t y) : - ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := - exists_contMDiffOn_forall_mem_convex_of_local I ht Hloc - -/-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be -a family of convex sets. Suppose that for each point `x : M` there exists a vector `c : F` such that -for all `y` in a neighborhood of `x` we have `c ∈ t y`. Then there exists a smooth function -`g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. See also -`exists_contMDiffOn_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local`. -/ -theorem exists_smooth_forall_mem_convex_of_local_const (ht : ∀ x, Convex ℝ (t x)) - (Hloc : ∀ x : M, ∃ c : F, ∀ᶠ y in 𝓝 x, c ∈ t y) : ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := - exists_smooth_forall_mem_convex_of_local I ht fun x => - let ⟨c, hc⟩ := Hloc x - ⟨_, hc, fun _ => c, contMDiffOn_const, fun _ => id⟩ - /-- 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 @@ -688,9 +648,6 @@ section `s_loc : M → V x` such that `s_loc` is $C^n$ smooth on `U_x₀` (when 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`. - -This theorem is a version of `exists_contMDiffOn_forall_mem_convex_of_local` for sections of a -vector bundle. It uses a partition of unity to glue together local sections. -/ theorem exists_contMDiff_section_forall_mem_convex_of_local {F_fiber : Type*} [NormedAddCommGroup F_fiber] [NormedSpace ℝ F_fiber] @@ -745,9 +702,6 @@ section `s_loc : M → V x` such that `s_loc` is $C^∞$ smooth on `U_x₀` (whe 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`. - -This theorem is a version of `exists_smooth_forall_mem_convex_of_local` for sections of a -vector bundle. It uses a partition of unity to glue together local sections. -/ theorem exists_smooth_section_forall_mem_convex_of_local {F_fiber : Type*} [NormedAddCommGroup F_fiber] [NormedSpace ℝ F_fiber] @@ -762,6 +716,61 @@ theorem exists_smooth_section_forall_mem_convex_of_local ∃ s : Cₛ^∞⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x := exists_contMDiff_section_forall_mem_convex_of_local I V t ht_conv Hloc +/-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` +be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood +`U ∈ 𝓝 x` and a function `g : M → F` such that `g` is $C^n$ smooth on `U` and `g y ∈ t y` for all +`y ∈ U`. Then there exists a $C^n$ smooth function `g : C^n⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` +for all `x`. + +This is a special case of `exists_contMDiff_section_forall_mem_convex_of_local` where `V` is the +trivial bundle. See also `exists_smooth_forall_mem_convex_of_local` and +`exists_smooth_forall_mem_convex_of_local_const`. -/ +theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) + (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) : + ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by + let V : M → Type _ := fun _ ↦ F + have Hloc' : + ∀ x₀, ∃ U ∈ 𝓝 x₀, ∃ s : (x : M) → V x, + ContMDiffOn I (I.prod 𝓘(ℝ, F)) n (fun x ↦ (⟨x, s x⟩ : TotalSpace F V)) U ∧ + ∀ y ∈ U, s y ∈ t y := by + intro x₀ + rcases Hloc x₀ with ⟨U, hU, g, hgs, hgt⟩ + have hgs' : + ContMDiffOn I (I.prod 𝓘(ℝ, F)) n (fun x ↦ (⟨x, g x⟩: TotalSpace F V)) U := by + intro x hx + simpa using ((Bundle.contMDiffWithinAt_section g U x).mpr (hgs x hx)) + exact ⟨U, hU, g, hgs', hgt⟩ + rcases exists_contMDiff_section_forall_mem_convex_of_local I V t ht Hloc' with ⟨s, hs⟩ + refine ⟨⟨fun x ↦ (s x : F), by + intro x + simpa using + (Bundle.contMDiffAt_section (fun y ↦ (s y : F)) x).mp + (s.contMDiff x)⟩, fun x ↦ by simpa using hs x⟩ + +/-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` +be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood +`U ∈ 𝓝 x` and a function `g : M → F` such that `g` is smooth on `U` and `g y ∈ t y` for all `y ∈ U`. +Then there exists a smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. + +This is a special case of `exists_contMDiff_section_forall_mem_convex_of_local` where `V` is the +trivial bundle. See also `exists_contMDiffOn_forall_mem_convex_of_local` and +`exists_smooth_forall_mem_convex_of_local_const`. -/ +theorem exists_smooth_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) + (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) ∞ g U ∧ ∀ y ∈ U, g y ∈ t y) : + ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := + exists_contMDiffOn_forall_mem_convex_of_local I ht Hloc + +/-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be +a family of convex sets. Suppose that for each point `x : M` there exists a vector `c : F` such that +for all `y` in a neighborhood of `x` we have `c ∈ t y`. Then there exists a smooth function +`g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. See also +`exists_contMDiffOn_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local`. -/ +theorem exists_smooth_forall_mem_convex_of_local_const (ht : ∀ x, Convex ℝ (t x)) + (Hloc : ∀ x : M, ∃ c : F, ∀ᶠ y in 𝓝 x, c ∈ t y) : ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := + exists_smooth_forall_mem_convex_of_local I ht fun x => + let ⟨c, hc⟩ := Hloc x + ⟨_, hc, fun _ => c, contMDiffOn_const, fun _ => id⟩ + /-- Let `M` be a smooth σ-compact manifold with extended distance. Let `K : ι → Set M` be a locally finite family of closed sets, let `U : ι → Set M` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there exists a positive smooth function `δ : M → ℝ≥0` such that for any `i` and From 431101839c3390b777a32e6e75e0de03164ace40 Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Sat, 17 May 2025 11:06:13 -0400 Subject: [PATCH 06/13] golf it further --- .../Geometry/Manifold/PartitionOfUnity.lean | 31 ++++++++----------- 1 file changed, 13 insertions(+), 18 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 508fd3f02c188e..076478bac5e0e0 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -728,24 +728,19 @@ trivial bundle. See also `exists_smooth_forall_mem_convex_of_local` and theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) : ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by - let V : M → Type _ := fun _ ↦ F - have Hloc' : - ∀ x₀, ∃ U ∈ 𝓝 x₀, ∃ s : (x : M) → V x, - ContMDiffOn I (I.prod 𝓘(ℝ, F)) n (fun x ↦ (⟨x, s x⟩ : TotalSpace F V)) U ∧ - ∀ y ∈ U, s y ∈ t y := by - intro x₀ - rcases Hloc x₀ with ⟨U, hU, g, hgs, hgt⟩ - have hgs' : - ContMDiffOn I (I.prod 𝓘(ℝ, F)) n (fun x ↦ (⟨x, g x⟩: TotalSpace F V)) U := by - intro x hx - simpa using ((Bundle.contMDiffWithinAt_section g U x).mpr (hgs x hx)) - exact ⟨U, hU, g, hgs', hgt⟩ - rcases exists_contMDiff_section_forall_mem_convex_of_local I V t ht Hloc' with ⟨s, hs⟩ - refine ⟨⟨fun x ↦ (s x : F), by - intro x - simpa using - (Bundle.contMDiffAt_section (fun y ↦ (s y : F)) x).mp - (s.contMDiff x)⟩, fun x ↦ by simpa using hs x⟩ + let V (_ : M) : Type _ := F + rcases exists_contMDiff_section_forall_mem_convex_of_local I V t ht + (fun x₀ ↦ by + rcases Hloc x₀ with ⟨U, hU, g, hgs, hgt⟩ + refine ⟨U, hU, g, ?_, hgt⟩ + intro y hy + rw [@Bundle.contMDiffWithinAt_section] + apply hgs y hy) + with ⟨s, hs⟩ + refine ⟨⟨fun x ↦ (s x : F), fun x₀ ↦ ?_⟩, hs⟩ + have := s.contMDiff x₀ + rw [Bundle.contMDiffAt_section] at this + exact this /-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood From 7a76c1b7f9693aa3e3194367dca39bbe0ba0874a Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Sat, 17 May 2025 11:10:15 -0400 Subject: [PATCH 07/13] let's fix the nomenclature here --- Mathlib/Geometry/Manifold/PartitionOfUnity.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 076478bac5e0e0..0933a7bcb65a50 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -649,7 +649,7 @@ 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_contMDiff_section_forall_mem_convex_of_local +theorem exists_contMDiffOn_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] @@ -729,7 +729,7 @@ theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) : ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by let V (_ : M) : Type _ := F - rcases exists_contMDiff_section_forall_mem_convex_of_local I V t ht + rcases exists_contMDiffOn_section_forall_mem_convex_of_local I V t ht (fun x₀ ↦ by rcases Hloc x₀ with ⟨U, hU, g, hgs, hgt⟩ refine ⟨U, hU, g, ?_, hgt⟩ From 35d9cb7e4f8aac197a9fd63cb26b3aa2115e40a6 Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Sat, 17 May 2025 11:11:48 -0400 Subject: [PATCH 08/13] whoops, missed this one --- Mathlib/Geometry/Manifold/PartitionOfUnity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 0933a7bcb65a50..bef8b931b89bfe 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -722,7 +722,7 @@ be a family of convex sets. Suppose that for each point `x : M` there exists a n `y ∈ U`. Then there exists a $C^n$ smooth function `g : C^n⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. -This is a special case of `exists_contMDiff_section_forall_mem_convex_of_local` where `V` is the +This is a special case of `exists_contMDiffOn_section_forall_mem_convex_of_local` where `V` is the trivial bundle. See also `exists_smooth_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local_const`. -/ theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) From 4f19811f744b4c5fef13b301baa0d994745f1e61 Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Sat, 17 May 2025 11:13:59 -0400 Subject: [PATCH 09/13] missed this as well --- Mathlib/Geometry/Manifold/PartitionOfUnity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index bef8b931b89bfe..3225d3a4bf4fb3 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -714,7 +714,7 @@ theorem exists_smooth_section_forall_mem_convex_of_local (fun x => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_x₀) ∧ (∀ y ∈ U_x₀, s_loc y ∈ t y)) : ∃ s : Cₛ^∞⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x := - exists_contMDiff_section_forall_mem_convex_of_local I V t ht_conv Hloc + exists_contMDiffOn_section_forall_mem_convex_of_local I V t ht_conv Hloc /-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood From f57388020c0043600598951e799016179960c553 Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Sat, 17 May 2025 11:15:43 -0400 Subject: [PATCH 10/13] typo here --- Mathlib/Geometry/Manifold/PartitionOfUnity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 3225d3a4bf4fb3..3e2f2ff40ddb3e 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -747,7 +747,7 @@ be a family of convex sets. Suppose that for each point `x : M` there exists a n `U ∈ 𝓝 x` and a function `g : M → F` such that `g` is smooth on `U` and `g y ∈ t y` for all `y ∈ U`. Then there exists a smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. -This is a special case of `exists_contMDiff_section_forall_mem_convex_of_local` where `V` is the +This is a special case of `exists_smooth_section_forall_mem_convex_of_local` where `V` is the trivial bundle. See also `exists_contMDiffOn_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local_const`. -/ theorem exists_smooth_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) From b44160bee8e7d6a0edff37b587ea3e2e8edbe5bd Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Mon, 7 Jul 2025 13:14:13 -0400 Subject: [PATCH 11/13] address golfs from PatrickMassot --- .../Geometry/Manifold/PartitionOfUnity.lean | 108 ++++++------------ 1 file changed, 37 insertions(+), 71 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 179ca1d3589789..227765b5456d5d 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -587,43 +587,25 @@ theorem contMDiff_totalSpace_weighted_sum_of_local_sections {n : ℕ∞} {ι : Type*} (ρ : SmoothPartitionOfUnity ι I M univ) (s_loc : ι → ((x : M) → V x)) (U : ι → Set M) (hU_isOpen : ∀ i, IsOpen (U i)) (hρ_subord : ρ.IsSubordinate U) (h_smooth_s_loc : ∀ i, ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x => (TotalSpace.mk x (s_loc i x) : TotalSpace F_fiber V)) (U i)) : + (fun x ↦ (TotalSpace.mk x (s_loc i x) : TotalSpace F_fiber V)) (U i)) : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x => (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by - let s_val (x : M) : V x := ∑ᶠ (j : ι), (ρ j x) • (s_loc j x) + (fun x ↦ (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by intro x₀ - apply (Bundle.contMDiffAt_section s_val x₀).mpr + apply (Bundle.contMDiffAt_section _ x₀).mpr let e₀ := trivializationAt F_fiber V x₀ apply ContMDiffAt.congr_of_eventuallyEq · apply ρ.contMDiffAt_finsum - · intro j h_x₀_in_tsupport_ρj - have h_slocj_smooth_at_x₀ : ContMDiffAt I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x => (TotalSpace.mk x (s_loc j x) : TotalSpace F_fiber V)) x₀ := - (h_smooth_s_loc j).contMDiffAt ((hU_isOpen j).mem_nhds (hρ_subord j h_x₀_in_tsupport_ρj)) - exact (contMDiffAt_section (s_loc j) x₀).mp h_slocj_smooth_at_x₀ - · have : (fun x ↦ (e₀ ⟨x, s_val x⟩).2) - =ᶠ[𝓝 x₀] - fun x ↦ ∑ᶠ i, ρ i x • (e₀ ⟨x, s_loc i x⟩).2 := by - have h_base : {x : M | x ∈ e₀.baseSet} ∈ (𝓝 x₀) := - e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀) - filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x _ hx_base - have hlin : IsLinearMap ℝ (fun y ↦ (e₀ ⟨x, y⟩).2) := e₀.linear ℝ hx_base - have hfin : {i : ι | (ρ i x • s_loc i x) ≠ 0}.Finite := by - refine (ρ.locallyFinite.point_finite x).subset fun i hi_smul_ne_zero => ?_ - contrapose! hi_smul_ne_zero - simp only [ne_eq, smul_eq_zero, not_or, mem_setOf_eq, not_and, not_not] - exact fun a ↦ False.elim (hi_smul_ne_zero a) - let Llin : V x →ₗ[ℝ] F_fiber := - { toFun := fun y ↦ (e₀ ⟨x, y⟩).2 - map_add' := by intro u v; simpa using hlin.map_add u v - map_smul' := by intro c u; simpa using hlin.map_smul c u } - have h_map : - (fun y ↦ (e₀ ⟨x, y⟩).2) (∑ᶠ i, ρ i x • s_loc i x) = - ∑ᶠ i, ρ i x • (fun y ↦ (e₀ ⟨x, y⟩).2) (s_loc i x) := by - simpa only [LinearMap.toAddMonoidHom_coe, map_smul] using - Llin.toAddMonoidHom.map_finsum hfin - exact h_map - exact this + · intro j hx₀ + rw [← contMDiffAt_section (s_loc j)] + exact h_smooth_s_loc j |>.contMDiffAt <| (hU_isOpen j).mem_nhds <| hρ_subord j hx₀ + · have h_base : {x : M | x ∈ e₀.baseSet} ∈ 𝓝 x₀ := + e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀) + filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x _ hx_base + have hfin : {i : ι | (ρ i x • s_loc i x) ≠ 0}.Finite := by + refine (ρ.locallyFinite.point_finite x).subset fun i hi_smul_ne_zero => ?_ + have : ρ i x ≠ 0 ∧ s_loc i x ≠ 0 := by simpa using hi_smul_ne_zero + exact this.1 + simpa using e₀.linearEquivAt ℝ x hx_base |>.toAddMonoidHom.map_finsum hfin end SmoothPartitionOfUnity @@ -645,42 +627,35 @@ theorem exists_contMDiffOn_section_forall_mem_convex_of_local (Hloc : ∀ x₀ : M, ∃ U_x₀ ∈ 𝓝 x₀, ∃ (s_loc : (x : M) → V x), (ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_x₀) ∧ + (fun x ↦ (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) 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 U_map h_nhds s_loc h_smooth_s_loc_on_U_map h_mem_t using Hloc - + choose W h_nhds s_loc s_smooth h_mem_t using Hloc -- Construct an open cover from the interiors of the given neighborhoods. - let U_open_cover (x : M) : Set M := interior (U_map x) - have hU_isOpen : ∀ x, IsOpen (U_open_cover x) := fun x ↦ isOpen_interior - have hU_covers_univ : univ ⊆ ⋃ x, U_open_cover x := by + let U (x : M) : Set M := interior (W x) + have U_op : ∀ x, IsOpen (U x) := fun x ↦ isOpen_interior + have hU_covers_univ : univ ⊆ ⋃ x, U x := by intro x_pt _ simp only [mem_iUnion, mem_univ] 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ρ_subord⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ, - ρ.IsSubordinate U_open_cover := + obtain ⟨ρ, hρU⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ, + ρ.IsSubordinate U := SmoothPartitionOfUnity.exists_isSubordinate - I isClosed_univ U_open_cover hU_isOpen hU_covers_univ - - -- Define the global section `s_val` by taking a weighted sum of the local sections. - let s_val (x : M) : V x := ∑ᶠ (j : M), (ρ j x) • (s_loc j x) - - -- Prove that `s_val`, when viewed as a map to the total space, is smooth. - have hs_val_tot_space_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x => (TotalSpace.mk x (s_val x) : TotalSpace F_fiber V)) := by - apply SmoothPartitionOfUnity.contMDiff_totalSpace_weighted_sum_of_local_sections I V ρ s_loc - U_open_cover hU_isOpen hρ_subord - intro j - exact (h_smooth_s_loc_on_U_map j).mono interior_subset - + I isClosed_univ U U_op hU_covers_univ + -- Define the global section `s` by taking a weighted sum of the local sections. + let s x : V x := ∑ᶠ j, (ρ j x) • s_loc j x + -- Prove that `s`, when viewed as a map to the total space, is smooth. + have s_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n + (fun x ↦ (TotalSpace.mk x (s x) : TotalSpace F_fiber V)) := + ρ.contMDiff_totalSpace_weighted_sum_of_local_sections + I V s_loc U U_op hρU fun j ↦ (s_smooth j).mono interior_subset -- Construct the smooth section and prove it lies in the convex sets `t x`. - refine ⟨⟨s_val, hs_val_tot_space_smooth⟩, fun x => ?_⟩ - apply (ht_conv x).finsum_mem (fun j => ρ.nonneg j x) (ρ.sum_eq_one (mem_univ x)) + refine ⟨⟨s, s_smooth⟩, 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 ∈ U_map j := interior_subset (hρ_subord j h_x_in_tsupport_ρj) + 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 /-- Let `V` be a vector bundle over a σ-compact Hausdorff finite dimensional topological manifold @@ -715,20 +690,11 @@ trivial bundle. See also `exists_smooth_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local_const`. -/ theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x)) (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) : - ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by - let V (_ : M) : Type _ := F - rcases exists_contMDiffOn_section_forall_mem_convex_of_local I V t ht - (fun x₀ ↦ by - rcases Hloc x₀ with ⟨U, hU, g, hgs, hgt⟩ - refine ⟨U, hU, g, ?_, hgt⟩ - intro y hy - rw [@Bundle.contMDiffWithinAt_section] - apply hgs y hy) - with ⟨s, hs⟩ - refine ⟨⟨fun x ↦ (s x : F), fun x₀ ↦ ?_⟩, hs⟩ - have := s.contMDiff x₀ - rw [Bundle.contMDiffAt_section] at this - exact this + ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := + let ⟨s, hs⟩ := exists_contMDiffOn_section_forall_mem_convex_of_local I (fun _ ↦ F) t ht + (fun x₀ ↦ let ⟨U, hU, g, hgs, hgt⟩ := Hloc x₀ + ⟨U, hU, g, fun y hy ↦ Bundle.contMDiffWithinAt_section _ _ _ |>.mpr <| hgs y hy, hgt⟩) + ⟨⟨s, (Bundle.contMDiffAt_section _ _ |>.mp <| s.contMDiff ·)⟩, hs⟩ /-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood From a12e6ee9e7590bcbc43d45ed0afa76b9750c53db Mon Sep 17 00:00:00 2001 From: Michael Lee Date: Mon, 7 Jul 2025 13:43:45 -0400 Subject: [PATCH 12/13] address CI failure --- Mathlib/Geometry/Manifold/PartitionOfUnity.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 227765b5456d5d..7422ed299fc517 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -591,13 +591,13 @@ theorem contMDiff_totalSpace_weighted_sum_of_local_sections ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n (fun x ↦ (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by intro x₀ - apply (Bundle.contMDiffAt_section _ x₀).mpr + apply (Bundle.contMDiffAt_section x₀).mpr let e₀ := trivializationAt F_fiber V x₀ apply ContMDiffAt.congr_of_eventuallyEq · apply ρ.contMDiffAt_finsum · intro j hx₀ - rw [← contMDiffAt_section (s_loc j)] - exact h_smooth_s_loc j |>.contMDiffAt <| (hU_isOpen j).mem_nhds <| hρ_subord j hx₀ + have := h_smooth_s_loc j |>.contMDiffAt <| (hU_isOpen j).mem_nhds <| hρ_subord j hx₀ + rwa [Bundle.contMDiffAt_section] at this · have h_base : {x : M | x ∈ e₀.baseSet} ∈ 𝓝 x₀ := e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀) filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x _ hx_base @@ -636,7 +636,7 @@ theorem exists_contMDiffOn_section_forall_mem_convex_of_local have U_op : ∀ x, IsOpen (U x) := fun x ↦ isOpen_interior have hU_covers_univ : univ ⊆ ⋃ x, U x := by intro x_pt _ - simp only [mem_iUnion, mem_univ] + 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, @@ -693,8 +693,8 @@ theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := let ⟨s, hs⟩ := exists_contMDiffOn_section_forall_mem_convex_of_local I (fun _ ↦ F) t ht (fun x₀ ↦ let ⟨U, hU, g, hgs, hgt⟩ := Hloc x₀ - ⟨U, hU, g, fun y hy ↦ Bundle.contMDiffWithinAt_section _ _ _ |>.mpr <| hgs y hy, hgt⟩) - ⟨⟨s, (Bundle.contMDiffAt_section _ _ |>.mp <| s.contMDiff ·)⟩, hs⟩ + ⟨U, hU, g, fun y hy ↦ Bundle.contMDiffWithinAt_section |>.mpr <| hgs y hy, hgt⟩) + ⟨⟨s, (Bundle.contMDiffAt_section _ |>.mp <| s.contMDiff ·)⟩, hs⟩ /-- Let `M` be a σ-compact Hausdorff finite dimensional topological manifold. Let `t : M → Set F` be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood From 4c58a6379c88f43c640bbec94a86b3823c74f987 Mon Sep 17 00:00:00 2001 From: grunweg Date: Wed, 20 Aug 2025 19:35:30 +0200 Subject: [PATCH 13/13] Apply suggestions from code review --- .../Geometry/Manifold/PartitionOfUnity.lean | 20 ++++++++----------- 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 7422ed299fc517..898b62605db314 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -587,9 +587,9 @@ theorem contMDiff_totalSpace_weighted_sum_of_local_sections {n : ℕ∞} {ι : Type*} (ρ : SmoothPartitionOfUnity ι I M univ) (s_loc : ι → ((x : M) → V x)) (U : ι → Set M) (hU_isOpen : ∀ i, IsOpen (U i)) (hρ_subord : ρ.IsSubordinate U) (h_smooth_s_loc : ∀ i, ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x ↦ (TotalSpace.mk x (s_loc i x) : TotalSpace F_fiber V)) (U i)) : + (fun x ↦ TotalSpace.mk' F_fiber x (s_loc i x)) (U i)) : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x ↦ (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by + (fun x ↦ TotalSpace.mk' F_fiber x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x))) := by intro x₀ apply (Bundle.contMDiffAt_section x₀).mpr let e₀ := trivializationAt F_fiber V x₀ @@ -627,29 +627,26 @@ theorem exists_contMDiffOn_section_forall_mem_convex_of_local (Hloc : ∀ x₀ : M, ∃ U_x₀ ∈ 𝓝 x₀, ∃ (s_loc : (x : M) → V x), (ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x ↦ (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_x₀) ∧ + (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 -- Construct an open cover from the interiors of the given neighborhoods. let U (x : M) : Set M := interior (W x) - have U_op : ∀ x, IsOpen (U x) := fun x ↦ isOpen_interior 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 := + obtain ⟨ρ, hρU⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ, ρ.IsSubordinate U := SmoothPartitionOfUnity.exists_isSubordinate - I isClosed_univ U U_op hU_covers_univ + I isClosed_univ U (fun x ↦ isOpen_interior) hU_covers_univ -- Define the global section `s` by taking a weighted sum of the local sections. let s x : V x := ∑ᶠ j, (ρ j x) • s_loc j x -- Prove that `s`, when viewed as a map to the total space, is smooth. - have s_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n - (fun x ↦ (TotalSpace.mk x (s x) : TotalSpace F_fiber V)) := + have s_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n (fun x ↦ TotalSpace.mk' F_fiber x (s x)) := ρ.contMDiff_totalSpace_weighted_sum_of_local_sections - I V s_loc U U_op hρU fun j ↦ (s_smooth j).mono interior_subset + I V s_loc U (fun x ↦ isOpen_interior) hρU fun j ↦ (s_smooth j).mono interior_subset -- Construct the smooth section and prove it lies in the convex sets `t x`. refine ⟨⟨s, s_smooth⟩, fun x ↦ ?_⟩ apply (ht_conv x).finsum_mem (ρ.nonneg · x) (ρ.sum_eq_one (mem_univ x)) @@ -673,8 +670,7 @@ theorem exists_smooth_section_forall_mem_convex_of_local (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 => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_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