From 1b87bc29a20c73cfaad6f1f8fdc70b392ac18b15 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 8 Feb 2024 13:29:01 +0000
Subject: [PATCH] feat(Analysis/Convex): lemmas about low-dimensional
 `stdSimplex`es (#10325)

Forward-port of leanprover-community/mathlib#19101
Motivated by https://github.com/Shamrock-Frost/BrouwerFixedPoint

Co-authored-by: @Shamrock-Frost
---
 Mathlib/Analysis/Convex/Basic.lean    | 62 ++++++++++++++++++++++++---
 Mathlib/Analysis/Convex/Topology.lean | 11 +++++
 2 files changed, 68 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Analysis/Convex/Basic.lean b/Mathlib/Analysis/Convex/Basic.lean
index 110c931738f0f1..3269c9ecb76f29 100644
--- a/Mathlib/Analysis/Convex/Basic.lean
+++ b/Mathlib/Analysis/Convex/Basic.lean
@@ -30,7 +30,7 @@ variable {𝕜 E F β : Type*}
 
 open LinearMap Set
 
-open BigOperators Classical Convex Pointwise
+open scoped BigOperators Convex Pointwise
 
 /-! ### Convexity of sets -/
 
@@ -665,6 +665,8 @@ end Submodule
 
 section Simplex
 
+section OrderedSemiring
+
 variable (𝕜) (ι : Type*) [OrderedSemiring 𝕜] [Fintype ι]
 
 /-- The standard simplex in the space of functions `ι → 𝕜` is the set of vectors with non-negative
@@ -688,11 +690,61 @@ theorem convex_stdSimplex : Convex 𝕜 (stdSimplex 𝕜 ι) := by
     exact hab
 #align convex_std_simplex convex_stdSimplex
 
-variable {ι}
+@[nontriviality] lemma stdSimplex_of_subsingleton [Subsingleton 𝕜] : stdSimplex 𝕜 ι = univ :=
+  eq_univ_of_forall fun _ ↦ ⟨fun _ ↦ (Subsingleton.elim _ _).le, Subsingleton.elim _ _⟩
+
+/-- The standard simplex in the zero-dimensional space is empty. -/
+lemma stdSimplex_of_isEmpty_index [IsEmpty ι] [Nontrivial 𝕜] : stdSimplex 𝕜 ι = ∅ :=
+  eq_empty_of_forall_not_mem <| by rintro f ⟨-, hf⟩; simp at hf
+
+lemma stdSimplex_unique [Unique ι] : stdSimplex 𝕜 ι = {fun _ ↦ 1} := by
+  refine eq_singleton_iff_unique_mem.2 ⟨⟨fun _ ↦ zero_le_one, Fintype.sum_unique _⟩, ?_⟩
+  rintro f ⟨-, hf⟩
+  rw [Fintype.sum_unique] at hf
+  exact funext (Unique.forall_iff.2 hf)
 
-theorem ite_eq_mem_stdSimplex (i : ι) : (fun j => ite (i = j) (1 : 𝕜) 0) ∈ stdSimplex 𝕜 ι :=
-  ⟨fun j => by simp only; split_ifs <;> norm_num, by
-    rw [Finset.sum_ite_eq, if_pos (Finset.mem_univ _)]⟩
+variable {ι} [DecidableEq ι]
+
+theorem single_mem_stdSimplex (i : ι) : Pi.single i 1 ∈ stdSimplex 𝕜 ι :=
+  ⟨le_update_iff.2 ⟨zero_le_one, fun _ _ ↦ le_rfl⟩, by simp⟩
+
+theorem ite_eq_mem_stdSimplex (i : ι) : (if i = · then (1 : 𝕜) else 0) ∈ stdSimplex 𝕜 ι := by
+  simpa only [@eq_comm _ i, ← Pi.single_apply] using single_mem_stdSimplex 𝕜 i
 #align ite_eq_mem_std_simplex ite_eq_mem_stdSimplex
 
+/-- The edges are contained in the simplex. -/
+lemma segment_single_subset_stdSimplex (i j : ι) :
+    [Pi.single i 1 -[𝕜] Pi.single j 1] ⊆ stdSimplex 𝕜 ι :=
+  (convex_stdSimplex 𝕜 ι).segment_subset (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)
+
+lemma stdSimplex_fin_two : stdSimplex 𝕜 (Fin 2) = [Pi.single 0 1 -[𝕜] Pi.single 1 1] := by
+  refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)
+  rintro f ⟨hf₀, hf₁⟩
+  rw [Fin.sum_univ_two] at hf₁
+  refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩
+  simp
+
+end OrderedSemiring
+
+section OrderedRing
+
+variable (𝕜) [OrderedRing 𝕜]
+
+/-- The standard one-dimensional simplex in `Fin 2 → 𝕜` is equivalent to the unit interval. -/
+@[simps (config := .asFn)]
+def stdSimplexEquivIcc : stdSimplex 𝕜 (Fin 2) ≃ Icc (0 : 𝕜) 1 where
+  toFun f := ⟨f.1 0, f.2.1 _, f.2.2 ▸
+    Finset.single_le_sum (fun i _ ↦ f.2.1 i) (Finset.mem_univ _)⟩
+  invFun x := ⟨![x, 1 - x], Fin.forall_fin_two.2 ⟨x.2.1, sub_nonneg.2 x.2.2⟩,
+    calc
+      ∑ i : Fin 2, ![(x : 𝕜), 1 - x] i = x + (1 - x) := Fin.sum_univ_two _
+      _ = 1 := add_sub_cancel'_right _ _⟩
+  left_inv f := Subtype.eq <| funext <| Fin.forall_fin_two.2 <| .intro rfl <|
+      calc
+        (1 : 𝕜) - f.1 0 = f.1 0 + f.1 1 - f.1 0 := by rw [← Fin.sum_univ_two f.1, f.2.2]
+        _ = f.1 1 := add_sub_cancel' _ _
+  right_inv x := Subtype.eq rfl
+
+end OrderedRing
+
 end Simplex
diff --git a/Mathlib/Analysis/Convex/Topology.lean b/Mathlib/Analysis/Convex/Topology.lean
index d91cf594e89606..2bfd6a5aede468 100644
--- a/Mathlib/Analysis/Convex/Topology.lean
+++ b/Mathlib/Analysis/Convex/Topology.lean
@@ -72,6 +72,17 @@ theorem isCompact_stdSimplex : IsCompact (stdSimplex ℝ ι) :=
 instance stdSimplex.instCompactSpace_coe : CompactSpace ↥(stdSimplex ℝ ι) :=
   isCompact_iff_compactSpace.mp <| isCompact_stdSimplex _
 
+/-- The standard one-dimensional simplex in `ℝ² = Fin 2 → ℝ`
+is homeomorphic to the unit interval. -/
+@[simps! (config := .asFn)]
+def stdSimplexHomeomorphUnitInterval : stdSimplex ℝ (Fin 2) ≃ₜ unitInterval where
+  toEquiv := stdSimplexEquivIcc ℝ
+  continuous_toFun := .subtype_mk ((continuous_apply 0).comp continuous_subtype_val) _
+  continuous_invFun := by
+    apply Continuous.subtype_mk
+    exact (continuous_pi <| Fin.forall_fin_two.2
+      ⟨continuous_subtype_val, continuous_const.sub continuous_subtype_val⟩)
+
 end stdSimplex
 
 /-! ### Topological vector space -/