feat: require that the range of a real or complex model with corners is convex (#25824)

This is important to ensure that the distance coming from a Riemannian metric generates the same topology as the original one.

See Zulip discussion at [#mathlib4 > Fixing the definition of models with corners @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Fixing.20the.20definition.20of.20models.20with.20corners/near/522572964)



Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: sgouezel

Mathlib/Geometry/Manifold/Diffeomorph.lean

@@ -399,16 +399,25 @@ variable (I) (e : E ≃L[𝕜] E')
 def transContinuousLinearEquiv : ModelWithCorners 𝕜 E' H where
   toPartialEquiv := I.toPartialEquiv.trans e.toEquiv.toPartialEquiv
   source_eq := by simp
-  uniqueDiffOn' := by simp [I.uniqueDiffOn]
-  target_subset_closure_interior := by
-    simp only [PartialEquiv.trans_target, Equiv.toPartialEquiv_target,
-      Equiv.toPartialEquiv_symm_apply, target_eq, univ_inter]
-    change e.toHomeomorph.symm ⁻¹' _ ⊆ closure (interior (e.toHomeomorph.symm ⁻¹' (range I)))
-    rw [← e.toHomeomorph.symm.isOpenMap.preimage_interior_eq_interior_preimage
-      e.toHomeomorph.continuous_symm,
-      ← e.toHomeomorph.symm.isOpenMap.preimage_closure_eq_closure_preimage
-      e.toHomeomorph.continuous_symm]
-    exact preimage_mono I.range_subset_closure_interior
+  convex_range' := by
+    split_ifs with h
+    · simp only [PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply, LinearEquiv.coe_toEquiv,
+      ContinuousLinearEquiv.coe_toLinearEquiv, toPartialEquiv_coe]
+      rw [range_comp]
+      letI := h.rclike
+      letI := NormedSpace.restrictScalars ℝ 𝕜 E
+      letI := NormedSpace.restrictScalars ℝ 𝕜 E'
+      let eR : E →L[ℝ] E' := ContinuousLinearMap.restrictScalars ℝ (e : E →L[𝕜] E')
+      change Convex ℝ (⇑eR '' range ↑I)
+      apply I.convex_range.linear_image
+    · simp [range_eq_univ_of_not_isRCLikeNormedField I h, range_comp]
+  nonempty_interior' := by
+    simp only [PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply, LinearEquiv.coe_toEquiv,
+      ContinuousLinearEquiv.coe_toLinearEquiv, toPartialEquiv_coe, range_comp,
+      ContinuousLinearEquiv.image_eq_preimage]
+    apply Nonempty.mono (preimage_interior_subset_interior_preimage e.symm.continuous)
+    rw [← ContinuousLinearEquiv.image_eq_preimage]
+    simpa using I.nonempty_interior
   continuous_toFun := e.continuous.comp I.continuous
   continuous_invFun := I.continuous_symm.comp e.symm.continuous
 

Mathlib/Geometry/Manifold/Instances/Real.lean

@@ -46,7 +46,7 @@ noncomputable section
 
 open Set Function
 
-open scoped Manifold ContDiff
+open scoped Manifold ContDiff ENNReal
 
 /-- The half-space in `ℝ^n`, used to model manifolds with boundary. We only define it when
 `1 ≤ n`, as the definition only makes sense in this case.
@@ -115,10 +115,9 @@ instance : LocPathConnectedSpace (EuclideanQuadrant n) :=
   EuclideanQuadrant.convex.locPathConnectedSpace
 
 theorem range_euclideanHalfSpace (n : ℕ) [NeZero n] :
-    (range fun x : EuclideanHalfSpace n => x.val) = { y | 0 ≤ y 0 } :=
+    range (Subtype.val : EuclideanHalfSpace n → _) = { y | 0 ≤ y 0 } :=
   Subtype.range_val
 
-open ENNReal in
 @[simp]
 theorem interior_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
     interior { y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i } = { y | a < y i } := by
@@ -129,7 +128,6 @@ theorem interior_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
 
 @[deprecated (since := "2024-11-12")] alias interior_halfspace := interior_halfSpace
 
-open ENNReal in
 @[simp]
 theorem closure_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
     closure { y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i } = { y | a ≤ y i } := by
@@ -140,7 +138,6 @@ theorem closure_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
 
 @[deprecated (since := "2024-11-12")] alias closure_halfspace := closure_halfSpace
 
-open ENNReal in
 @[simp]
 theorem closure_open_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
     closure { y : PiLp p (fun _ : Fin n ↦ ℝ) | a < y i } = { y | a ≤ y i } := by
@@ -151,7 +148,6 @@ theorem closure_open_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n)
 
 @[deprecated (since := "2024-11-12")] alias closure_open_halfspace := closure_open_halfSpace
 
-open ENNReal in
 @[simp]
 theorem frontier_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
     frontier { y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i } = { y | a = y i } := by
@@ -161,9 +157,22 @@ theorem frontier_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
 @[deprecated (since := "2024-11-12")] alias frontier_halfspace := frontier_halfSpace
 
 theorem range_euclideanQuadrant (n : ℕ) :
-    (range fun x : EuclideanQuadrant n => x.val) = { y | ∀ i : Fin n, 0 ≤ y i } :=
+    range (Subtype.val : EuclideanQuadrant n → _) = { y | ∀ i : Fin n, 0 ≤ y i } :=
   Subtype.range_val
 
+theorem interior_euclideanQuadrant (n : ℕ) (p : ℝ≥0∞) (a : ℝ) :
+    interior { y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a ≤ y i } =
+      { y | ∀ i : Fin n, a < y i } := by
+  let f : Fin n → (Π _ : Fin n, ℝ) →L[ℝ] ℝ := fun i ↦ ContinuousLinearMap.proj i
+  have h : { y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a ≤ y i } = ⋂ i, (f i )⁻¹' Ici a := by
+    ext; simp; rfl
+  have h' : { y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a < y i } = ⋂ i, (f i )⁻¹' Ioi a := by
+    ext; simp; rfl
+  rw [h, h', interior_iInter_of_finite]
+  apply iInter_congr fun i ↦ ?_
+  rw [(f i).interior_preimage, interior_Ici]
+  apply Function.surjective_eval
+
 end
 
 /--
@@ -183,12 +192,14 @@ def modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
     exact ⟨max_eq_left xprop, fun i _ => rfl⟩
   right_inv' _ hx := update_eq_iff.2 ⟨max_eq_left hx, fun _ _ => rfl⟩
   source_eq := rfl
-  uniqueDiffOn' := by
-    have : UniqueDiffOn ℝ _ :=
-      UniqueDiffOn.pi (Fin n) (fun _ => ℝ) _ _ fun i (_ : i ∈ ({0} : Set (Fin n))) =>
-        uniqueDiffOn_Ici 0
-    simpa only [singleton_pi] using this
-  target_subset_closure_interior := by simp
+  convex_range' := by
+    simp only [instIsRCLikeNormedField, ↓reduceDIte]
+    apply Convex.convex_isRCLikeNormedField
+    rw [range_euclideanHalfSpace n]
+    exact EuclideanHalfSpace.convex (n := n)
+  nonempty_interior' := by
+    rw [range_euclideanHalfSpace, interior_halfSpace]
+    refine ⟨fun i ↦ 1, by simp⟩
   continuous_toFun := continuous_subtype_val
   continuous_invFun := by
     exact (continuous_id.update 0 <| (continuous_apply 0).max continuous_const).subtype_mk _
@@ -207,16 +218,14 @@ def modelWithCornersEuclideanQuadrant (n : ℕ) :
   left_inv' x _ := by ext i; simp only [x.2 i, max_eq_left]
   right_inv' x hx := by ext1 i; simp only [hx i, max_eq_left]
   source_eq := rfl
-  uniqueDiffOn' := by
-    have this : UniqueDiffOn ℝ _ :=
-      UniqueDiffOn.univ_pi (Fin n) (fun _ => ℝ) _ fun _ => uniqueDiffOn_Ici 0
-    simpa only [pi_univ_Ici] using this
-  target_subset_closure_interior := by
-    have : {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x i}
-      = Set.pi univ (fun i ↦ Ici 0) := by aesop
-    simp only [this, interior_pi_set finite_univ]
-    rw [closure_pi_set]
-    simp
+  convex_range' := by
+    simp only [instIsRCLikeNormedField, ↓reduceDIte]
+    apply Convex.convex_isRCLikeNormedField
+    rw [range_euclideanQuadrant]
+    exact EuclideanQuadrant.convex
+  nonempty_interior' := by
+    rw [range_euclideanQuadrant, interior_euclideanQuadrant]
+    exact ⟨fun i ↦ 1, by simp⟩
   continuous_toFun := continuous_subtype_val
   continuous_invFun := Continuous.subtype_mk
     (continuous_pi fun i => (continuous_id.max continuous_const).comp (continuous_apply i)) _
@@ -505,7 +514,6 @@ section
 
 instance : ChartedSpace (EuclideanHalfSpace 1) (Icc (0 : ℝ) 1) := by infer_instance
 
-instance {n : WithTop ℕ∞} : IsManifold (𝓡∂ 1) n (Icc (0 : ℝ) 1) := by
-  infer_instance
+instance {n : WithTop ℕ∞} : IsManifold (𝓡∂ 1) n (Icc (0 : ℝ) 1) := by infer_instance
 
 end

Mathlib/Geometry/Manifold/IsManifold/Basic.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Normed.Module.Convex
+import Mathlib.Analysis.RCLike.TangentCone
 import Mathlib.Data.Bundle
 import Mathlib.Geometry.Manifold.ChartedSpace
 
@@ -135,39 +136,62 @@ open scoped Manifold Topology ContDiff
 
 /-! ### Models with corners. -/
 
-
+open scoped Classical in
 /-- A structure containing information on the way a space `H` embeds in a
 model vector space `E` over the field `𝕜`. This is all what is needed to
 define a `C^n` manifold with model space `H`, and model vector space `E`.
 
-We require two conditions `uniqueDiffOn'` and `target_subset_closure_interior`, which
-are satisfied in the relevant cases (where `range I = univ` or a half space or a quadrant) and
-useful for technical reasons. The former makes sure that manifold derivatives are uniquely
-defined, the latter ensures that for `C^2` maps the second derivatives are symmetric even for points
-on the boundary, as these are limit points of interior points where symmetry holds. If further
-conditions turn out to be useful, they can be added here.
+We require that, when the field is `ℝ` or `ℂ`, the range is `ℝ`-convex, as this is what is needed
+to do calculus and covers the standard examples of manifolds with boundary. Over other fields,
+we require that the range is `univ`, as there is no relevant notion of manifold of boundary there.
 -/
 @[ext]
 structure ModelWithCorners (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] (H : Type*) [TopologicalSpace H] extends
     PartialEquiv H E where
   source_eq : source = univ
-  uniqueDiffOn' : UniqueDiffOn 𝕜 toPartialEquiv.target
-  target_subset_closure_interior : toPartialEquiv.target ⊆ closure (interior toPartialEquiv.target)
+  /-- To check this condition when the space already has a real normed space structure,
+  use `Convex.convex_isRCLikeNormedField` which eliminates the `letI`s below, or the constructor
+  `ModelWithCorners.of_convex_range` -/
+  convex_range' :
+    if h : IsRCLikeNormedField 𝕜 then
+      letI := h.rclike 𝕜;
+      letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
+      Convex ℝ (range toPartialEquiv)
+    else range toPartialEquiv = univ
+  nonempty_interior' : (interior (range toPartialEquiv)).Nonempty
   continuous_toFun : Continuous toFun := by continuity
   continuous_invFun : Continuous invFun := by continuity
 
+lemma ModelWithCorners.range_eq_target {𝕜 E H : Type*} [NontriviallyNormedField 𝕜]
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) :
+    range I.toPartialEquiv = I.target := by
+  rw [← I.image_source_eq_target, I.source_eq, image_univ.symm]
+
+/-- If a model with corners has full range, the `convex_range'` condition is satisfied. -/
+def ModelWithCorners.of_target_univ (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
+    (φ : PartialEquiv H E) (hsource : φ.source = univ) (htarget : φ.target = univ)
+    (hcont : Continuous φ) (hcont_inv : Continuous φ.symm) : ModelWithCorners 𝕜 E H where
+  toPartialEquiv := φ
+  source_eq := hsource
+  convex_range' := by
+    have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
+    simp only [this, htarget, dite_else_true]
+    intro h
+    letI := h.rclike 𝕜
+    letI := NormedSpace.restrictScalars ℝ 𝕜 E
+    exact convex_univ
+  nonempty_interior' := by
+    have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
+    simp [this, htarget]
+
 attribute [simp, mfld_simps] ModelWithCorners.source_eq
 
 /-- A vector space is a model with corners, denoted as `𝓘(𝕜, E)` within the `Manifold` namespace. -/
 def modelWithCornersSelf (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ModelWithCorners 𝕜 E E where
-  toPartialEquiv := PartialEquiv.refl E
-  source_eq := rfl
-  uniqueDiffOn' := uniqueDiffOn_univ
-  target_subset_closure_interior := by simp
-  continuous_toFun := continuous_id
-  continuous_invFun := continuous_id
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ModelWithCorners 𝕜 E E :=
+  ModelWithCorners.of_target_univ 𝕜 (PartialEquiv.refl E) rfl rfl continuous_id continuous_id
 
 @[inherit_doc] scoped[Manifold] notation "𝓘(" 𝕜 ", " E ")" => modelWithCornersSelf 𝕜 E
 
@@ -252,12 +276,76 @@ theorem target_eq : I.target = range (I : H → E) := by
   rw [← image_univ, ← I.source_eq]
   exact I.image_source_eq_target.symm
 
-protected theorem uniqueDiffOn : UniqueDiffOn 𝕜 (range I) :=
-  I.target_eq ▸ I.uniqueDiffOn'
+theorem nonempty_interior : (interior (range I)).Nonempty :=
+  I.nonempty_interior'
+
+theorem range_eq_univ_of_not_isRCLikeNormedField (h : ¬ IsRCLikeNormedField 𝕜) :
+    range I = univ := by
+  simpa [h] using I.convex_range'
+
+/-- If a set is `ℝ`-convex for some normed space structure, then it is `ℝ`-convex for the
+normed space structure coming from an `IsRCLikeNormedField 𝕜`. Useful when constructing model
+spaces to avoid diamond issues when populating the field `convex_range'`. -/
+lemma _root_.Convex.convex_isRCLikeNormedField [NormedSpace ℝ E] [h : IsRCLikeNormedField 𝕜]
+    {s : Set E} (hs : Convex ℝ s) :
+    letI := h.rclike
+    letI := NormedSpace.restrictScalars ℝ 𝕜 E
+    Convex ℝ s := by
+  letI := h.rclike
+  letI := NormedSpace.restrictScalars ℝ 𝕜 E
+  simp only [Convex, StarConvex] at hs ⊢
+  intro u hu v hv a b ha hb hab
+  convert hs hu hv ha hb hab using 2
+  · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]
+  · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]
+
+/-- Construct a model with corners over `ℝ` from a continuous partial equiv with convex range. -/
+def of_convex_range
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H]
+    (φ : PartialEquiv H E) (hsource : φ.source = univ) (htarget : Convex ℝ φ.target)
+    (hcont : Continuous φ) (hcont_inv : Continuous φ.symm) (hint : (interior φ.target).Nonempty) :
+    ModelWithCorners ℝ E H where
+  toPartialEquiv := φ
+  source_eq := hsource
+  convex_range' := by
+    have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
+    simp only [instIsRCLikeNormedField, ↓reduceDIte, this]
+    exact htarget.convex_isRCLikeNormedField
+  nonempty_interior' := by
+    have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
+    simp [this, htarget, hint]
+
+theorem convex_range [NormedSpace ℝ E] : Convex ℝ (range I) := by
+  by_cases h : IsRCLikeNormedField 𝕜
+  · letI : RCLike 𝕜 := h.rclike
+    have W := I.convex_range'
+    simp only [h, ↓reduceDIte, toPartialEquiv_coe] at W
+    simp only [Convex, StarConvex] at W ⊢
+    intro u hu v hv a b ha hb hab
+    convert W hu hv ha hb hab using 2
+    · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
+      rfl
+    · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
+      rfl
+  · simp [range_eq_univ_of_not_isRCLikeNormedField I h, convex_univ]
+
+protected theorem uniqueDiffOn : UniqueDiffOn 𝕜 (range I) := by
+  by_cases h : IsRCLikeNormedField 𝕜
+  · letI := h.rclike 𝕜;
+    letI := NormedSpace.restrictScalars ℝ 𝕜 E
+    apply uniqueDiffOn_convex_of_isRCLikeNormedField _ I.nonempty_interior
+    simpa [h] using I.convex_range
+  · simp [range_eq_univ_of_not_isRCLikeNormedField I h, uniqueDiffOn_univ]
 
 theorem range_subset_closure_interior : range I ⊆ closure (interior (range I)) := by
-  rw [← I.target_eq]
-  exact I.target_subset_closure_interior
+  by_cases h : IsRCLikeNormedField 𝕜
+  · letI := h.rclike 𝕜
+    letI := NormedSpace.restrictScalars ℝ 𝕜 E
+    rw [Convex.closure_interior_eq_closure_of_nonempty_interior (𝕜 := ℝ)]
+    · apply subset_closure
+    · apply I.convex_range
+    · apply I.nonempty_interior
+  · simp [range_eq_univ_of_not_isRCLikeNormedField I h]
 
 @[simp, mfld_simps]
 protected theorem left_inv (x : H) : I.symm (I x) = x := by refine I.left_inv' ?_; simp
@@ -398,10 +486,17 @@ def ModelWithCorners.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Ty
     invFun := fun x => (I.symm x.1, I'.symm x.2)
     source := { x | x.1 ∈ I.source ∧ x.2 ∈ I'.source }
     source_eq := by simp only [setOf_true, mfld_simps]
-    uniqueDiffOn' := I.uniqueDiffOn'.prod I'.uniqueDiffOn'
-    target_subset_closure_interior := by
-      simp only [PartialEquiv.prod_target, target_eq, interior_prod_eq, closure_prod_eq]
-      exact Set.prod_mono I.range_subset_closure_interior I'.range_subset_closure_interior
+    convex_range' := by
+      have : range (fun (x : ModelProd H H') ↦ (I x.1, I' x.2)) = range (Prod.map I I') := rfl
+      rw [this, Set.range_prodMap]
+      split_ifs with h
+      · letI := h.rclike;
+        letI := NormedSpace.restrictScalars ℝ 𝕜 E; letI := NormedSpace.restrictScalars ℝ 𝕜 E'
+        exact I.convex_range.prod I'.convex_range
+      · simp [range_eq_univ_of_not_isRCLikeNormedField, h]
+    nonempty_interior' := by
+      have : range (fun (x : ModelProd H H') ↦ (I x.1, I' x.2)) = range (Prod.map I I') := rfl
+      simp [this, interior_prod_eq, nonempty_interior]
     continuous_toFun := I.continuous_toFun.prodMap I'.continuous_toFun
     continuous_invFun := I.continuous_invFun.prodMap I'.continuous_invFun }
 
@@ -414,10 +509,16 @@ def ModelWithCorners.pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {ι : Typ
     ModelWithCorners 𝕜 (∀ i, E i) (ModelPi H) where
   toPartialEquiv := PartialEquiv.pi fun i => (I i).toPartialEquiv
   source_eq := by simp only [pi_univ, mfld_simps]
-  uniqueDiffOn' := UniqueDiffOn.pi ι E _ _ fun i _ => (I i).uniqueDiffOn'
-  target_subset_closure_interior := by
-    simp only [PartialEquiv.pi_target, target_eq, finite_univ, interior_pi_set, closure_pi_set]
-    exact Set.pi_mono (fun i _ ↦ (I i).range_subset_closure_interior)
+  convex_range' := by
+    rw [PartialEquiv.pi_apply, Set.range_piMap]
+    split_ifs with h
+    · letI := h.rclike;
+      letI := fun i ↦ NormedSpace.restrictScalars ℝ 𝕜 (E i);
+      exact convex_pi fun i _hi ↦ (I i).convex_range
+    · simp [range_eq_univ_of_not_isRCLikeNormedField, h]
+  nonempty_interior' := by
+    rw [PartialEquiv.pi_apply, Set.range_piMap]
+    simp [interior_pi_set finite_univ, univ_pi_nonempty_iff, nonempty_interior]
   continuous_toFun := continuous_pi fun i => (I i).continuous.comp (continuous_apply i)
   continuous_invFun := continuous_pi fun i => (I i).continuous_symm.comp (continuous_apply i)