feature(Analysis/Convex/Basic): Convexity and the algebra map (#29248)

Let `R` and `A` be ordered rings, `A` an `R`-algebra and `R`, `A`, `M` a scalar tower. We provide sufficient conditions for an `R`-convex subset of `M` to be `A`-convex and for an `A`-convex subset of `M` to be `R`-convex.

These are used to show that, when `K` is `RCLike` and `ℝ` `K` `E` is a scalar tower, a set is `K`-convex if and only if it is `ℝ`-convex.

Used in #29258

Author: mans0954

Mathlib/Analysis/Convex/Basic.lean

@@ -595,3 +595,25 @@ protected theorem starConvex (K : Submodule 𝕜 E) : StarConvex 𝕜 (0 : E) K
   K.convex K.zero_mem
 
 end Submodule
+
+section CommSemiring
+
+variable {R : Type*} [CommSemiring R]
+variable (A : Type*) [Semiring A] [Algebra R A]
+variable {M : Type*} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M]
+variable [PartialOrder R] [PartialOrder A]
+
+lemma convex_of_nonneg_surjective_algebraMap [FaithfulSMul R A] {s : Set M}
+    (halg : Set.Ici 0 ⊆ algebraMap R A '' Set.Ici 0) (hs : Convex R s) :
+    Convex A s := by
+  simp only [Convex, StarConvex] at hs ⊢
+  intro u hu v hv a b ha hb hab
+  obtain ⟨c, hc1, hc2⟩ := halg ha
+  obtain ⟨d, hd1, hd2⟩ := halg hb
+  convert hs hu hv hc1 hd1 _ using 2
+  · rw [← hc2, algebraMap_smul]
+  · rw [← hd2, algebraMap_smul]
+  rw [← hc2, ← hd2, ← algebraMap.coe_add] at hab
+  exact (FaithfulSMul.algebraMap_eq_one_iff R A).mp hab
+
+end CommSemiring

Mathlib/Analysis/RCLike/Lemmas.lean

@@ -13,6 +13,12 @@ open scoped Finset
 
 variable {K E : Type*} [RCLike K]
 
+open ComplexOrder RCLike in
+lemma convex_RCLike_iff_convex_real [AddCommMonoid E] [Module K E] [Module ℝ E]
+    [IsScalarTower ℝ K E] {s : Set E} : Convex K s ↔ Convex ℝ s :=
+  ⟨Convex.lift ℝ,
+  fun hs => convex_of_nonneg_surjective_algebraMap _ (fun _ => nonneg_iff_exists_ofReal.mp) hs⟩
+
 namespace Polynomial
 
 theorem ofReal_eval (p : ℝ[X]) (x : ℝ) : (↑(p.eval x) : K) = aeval (↑x) p :=