feat: basic lemmas about convexity over NNReal (#31887)

Author: ADedecker

Mathlib.lean

@@ -1707,6 +1707,7 @@ public import Mathlib.Analysis.Convex.KreinMilman
 public import Mathlib.Analysis.Convex.LinearIsometry
 public import Mathlib.Analysis.Convex.Measure
 public import Mathlib.Analysis.Convex.Mul
+public import Mathlib.Analysis.Convex.NNReal
 public import Mathlib.Analysis.Convex.PartitionOfUnity
 public import Mathlib.Analysis.Convex.PathConnected
 public import Mathlib.Analysis.Convex.Piecewise

Mathlib/Analysis/Convex/NNReal.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+module
+
+public import Mathlib.Analysis.Convex.Basic
+public import Mathlib.Data.NNReal.Basic
+
+/-!
+# Specific lemmas about convexity over `ℝ≥0`
+
+This file collects some specific results about convexity over the ring `ℝ≥0`.
+Expand as needed.
+-/
+
+@[expose] public section
+
+open Set
+open scoped NNReal
+
+namespace NNReal
+
+protected lemma Icc_subset_segment {x y : ℝ≥0} :
+    Icc x y ⊆ segment ℝ≥0 x y :=
+  Nonneg.Icc_subset_segment
+
+protected lemma segment_eq_Icc {x y : ℝ≥0} (hxy : x ≤ y) :
+    segment ℝ≥0 x y = Icc x y :=
+  Nonneg.segment_eq_Icc hxy
+
+protected lemma segment_eq_uIcc {x y : ℝ≥0} :
+    segment ℝ≥0 x y = uIcc x y :=
+  Nonneg.segment_eq_uIcc
+
+protected lemma convex_iff {M : Type*} [AddCommMonoid M] [Module ℝ M] {s : Set M} :
+    Convex ℝ≥0 s ↔ Convex ℝ s := by
+  refine ⟨fun H ↦ ?_, Convex.lift ℝ≥0⟩
+  intro _ hx _ hy a b ha hb hab
+  exact H hx hy (a := ⟨a, ha⟩) (b := ⟨b, hb⟩) (zero_le _) (zero_le _) (by ext; simpa)
+
+end NNReal

Mathlib/Analysis/Convex/Segment.lean

@@ -5,6 +5,7 @@ Authors: Alexander Bentkamp, Yury Kudryashov, Yaël Dillies
 -/
 module
 
+public import Mathlib.Algebra.Order.Nonneg.Ring
 public import Mathlib.LinearAlgebra.AffineSpace.Midpoint
 public import Mathlib.LinearAlgebra.LinearIndependent.Lemmas
 public import Mathlib.LinearAlgebra.Ray
@@ -575,6 +576,30 @@ theorem Convex.mem_Ico (h : x < y) :
 
 end LinearOrderedField
 
+namespace Nonneg
+
+variable [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜}
+
+protected lemma Icc_subset_segment {x y : {t : 𝕜 // 0 ≤ t}} :
+    Icc x y ⊆ segment {t : 𝕜 // 0 ≤ t} x y := by
+  intro a ⟨hxa, hay⟩
+  rw [← Subtype.coe_le_coe] at hxa hay
+  rcases Icc_subset_segment ⟨hxa, hay⟩ with ⟨t₁, t₂, t₁_nonneg, t₂_nonneg, t_add, hta⟩
+  refine ⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le _, zero_le _, ?_, ?_⟩ <;>
+  ext <;> simpa
+
+protected lemma segment_eq_Icc {x y : {t : 𝕜 // 0 ≤ t}} (hxy : x ≤ y) :
+    segment {t : 𝕜 // 0 ≤ t} x y = Icc x y := by
+  refine subset_antisymm (segment_subset_Icc hxy) Nonneg.Icc_subset_segment
+
+protected lemma segment_eq_uIcc {x y : {t : 𝕜 // 0 ≤ t}} :
+    segment {t : 𝕜 // 0 ≤ t} x y = uIcc x y := by
+  rcases le_total x y with h | h
+  · simp [h, Nonneg.segment_eq_Icc]
+  · simp [h, segment_symm _ x y, Nonneg.segment_eq_Icc]
+
+end Nonneg
+
 namespace Prod
 
 variable [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F]