English
If R is a partially ordered ring with star, topological structure, and a continuous square root, then the function space C(α, R) is a StarOrderedRing with the pointwise operations and the induced order.
Русский
Если R — частично упорядченное кольцо со звездой и есть непрерывная квадратный корень, то функция C(α,R) становится StarOrderedRing с точечными операциями и индуцированным порядком.
LaTeX
$$$\mathrm{StarOrderedRing}\bigl(C(\alpha, R)\bigr)$$$
Lean4
instance {R : Type*} [PartialOrder R] [NonUnitalSemiring R] [StarRing R] [StarOrderedRing R] [TopologicalSpace R]
[ContinuousStar R] [IsTopologicalSemiring R] [ContinuousSqrt R] : StarOrderedRing C(α, R) :=
by
refine StarOrderedRing.of_le_iff ?_
intro f g
constructor
· rw [ContinuousMap.le_def]
intro h
use
(mk _ ContinuousSqrt.continuousOn_sqrt.restrict).comp
⟨_, map_continuous (f.prodMk g) |>.codRestrict (s := {x | x.1 ≤ x.2}) (by exact h)⟩
ext x
simpa [IsSelfAdjoint.star_eq <| .of_nonneg (ContinuousSqrt.sqrt_nonneg (f x, g x) (h x))] using
ContinuousSqrt.sqrt_mul_sqrt (f x, g x) (h x)
· rintro ⟨p, rfl⟩
exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (p x))
