feat: StarOrderedRing instances on ContinuousMap (#12040)

Mathlib.lean

@@ -3914,6 +3914,7 @@ import Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus
 import Mathlib.Topology.ContinuousFunction.Ordered
 import Mathlib.Topology.ContinuousFunction.Polynomial
 import Mathlib.Topology.ContinuousFunction.Sigma
+import Mathlib.Topology.ContinuousFunction.StarOrdered
 import Mathlib.Topology.ContinuousFunction.StoneWeierstrass
 import Mathlib.Topology.ContinuousFunction.T0Sierpinski
 import Mathlib.Topology.ContinuousFunction.UniqueCFC

Mathlib/Analysis/RCLike/Basic.lean

@@ -987,7 +987,7 @@ theorem reCLM_apply : ((reCLM : K →L[ℝ] ℝ) : K → ℝ) = re :=
   rfl
 #align is_R_or_C.re_clm_apply RCLike.reCLM_apply
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_re : Continuous (re : K → ℝ) :=
   reCLM.continuous
 #align is_R_or_C.continuous_re RCLike.continuous_re
@@ -1019,7 +1019,7 @@ theorem imCLM_apply : ((imCLM : K →L[ℝ] ℝ) : K → ℝ) = im :=
   rfl
 #align is_R_or_C.im_clm_apply RCLike.imCLM_apply
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_im : Continuous (im : K → ℝ) :=
   imCLM.continuous
 #align is_R_or_C.continuous_im RCLike.continuous_im

Mathlib/Data/Real/Sqrt.lean

@@ -111,6 +111,7 @@ theorem sqrt_div (x y : ℝ≥0) : sqrt (x / y) = sqrt x / sqrt y :=
   map_div₀ sqrtHom x y
 #align nnreal.sqrt_div NNReal.sqrt_div
 
+@[continuity, fun_prop]
 theorem continuous_sqrt : Continuous sqrt := sqrt.continuous
 #align nnreal.continuous_sqrt NNReal.continuous_sqrt
 

Mathlib/Topology/ContinuousFunction/StarOrdered.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Topology.ContinuousFunction.Algebra
+
+/-! # Continuous functions as a star-ordered ring -/
+
+namespace ContinuousMap
+
+variable {α : Type*} [TopologicalSpace α]
+
+lemma starOrderedRing_of_sqrt {R : Type*} [PartialOrder R] [NonUnitalRing R] [StarRing R]
+    [StarOrderedRing R] [TopologicalSpace R] [ContinuousStar R] [TopologicalRing R]
+    (sqrt : R → R) (h_continuousOn : ContinuousOn sqrt {x : R | 0 ≤ x})
+    (h_sqrt : ∀ x, 0 ≤ x → star (sqrt x) * sqrt x = x) : StarOrderedRing C(α, R) :=
+  StarOrderedRing.of_nonneg_iff' add_le_add_left fun f ↦ by
+    constructor
+    · intro hf
+      use (mk _ h_continuousOn.restrict).comp ⟨_, map_continuous f |>.codRestrict (by exact hf ·)⟩
+      ext x
+      exact h_sqrt (f x) (hf x) |>.symm
+    · rintro ⟨f, rfl⟩
+      rw [ContinuousMap.le_def]
+      exact fun x ↦ star_mul_self_nonneg (f x)
+
+open scoped ComplexOrder in
+open RCLike in
+instance (priority := 100) instStarOrderedRingRCLike {𝕜 : Type*} [RCLike 𝕜] :
+    StarOrderedRing C(α, 𝕜) :=
+  starOrderedRing_of_sqrt ((↑) ∘ Real.sqrt ∘ re) (by fun_prop) fun x hx ↦ by
+    simp only [Function.comp_apply,star_def]
+    obtain hx' := nonneg_iff.mp hx |>.right
+    rw [← conj_eq_iff_im, conj_eq_iff_re] at hx'
+    rw [conj_ofReal, ← ofReal_mul, Real.mul_self_sqrt, hx']
+    rw [nonneg_iff]
+    simpa using nonneg_iff.mp hx |>.left
+
+instance instStarOrderedRingReal : StarOrderedRing C(α, ℝ) :=
+  instStarOrderedRingRCLike (𝕜 := ℝ)
+
+open scoped ComplexOrder in
+open Complex in
+instance instStarOrderedRingComplex : StarOrderedRing C(α, ℂ) :=
+  instStarOrderedRingRCLike (𝕜 := ℂ)
+
+open NNReal in
+instance instStarOrderedRingNNReal : StarOrderedRing C(α, ℝ≥0) :=
+  StarOrderedRing.of_le_iff fun f g ↦ by
+    constructor
+    · intro hfg
+      use .comp ⟨sqrt, by fun_prop⟩ (g - f)
+      ext1 x
+      simpa using add_tsub_cancel_of_le (hfg x) |>.symm
+    · rintro ⟨s, rfl⟩
+      exact fun _ ↦ by simp
+
+end ContinuousMap