refactor(MeasureTheory/RieszMarkovKakutani): Use PositiveLinearMap (#28059)

This PR refactors the unbundled `{Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ} (hΛ : ∀ f, 0 ≤ f → 0 ≤ Λ f)` in the statement of RMK to the bundled `(Λ : C_c(X, ℝ) →ₚ[ℝ] ℝ)`.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Uniqueness.20in.20Riesz.E2.80.93Markov.E2.80.93Kakutani.20representation.20theorem



Co-authored-by: Thomas Zhu <29544653+hanwenzhu@users.noreply.github.com>

Author: CoolRmal

Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

@@ -81,6 +81,10 @@ instance : FunLike (E₁ →ₚ[R] E₂) E₁ E₂ where
     apply DFunLike.coe_injective'
     exact h
 
+@[ext]
+lemma ext {f g : E₁ →ₚ[R] E₂} (h : ∀ x, f x = g x) : f = g :=
+  DFunLike.ext f g h
+
 instance : LinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂ where
   map_add f := map_add f.toLinearMap
   map_smulₛₗ f := f.toLinearMap.map_smul'

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean

@@ -48,17 +48,10 @@ lemma CompactlySupportedContinuousMap.monotone_of_nnreal : Monotone Λ := by
   simp
 
 /-- The positivity of a linear functional `Λ` implies that `Λ` is monotone. -/
+@[deprecated PositiveLinearMap.mk₀ (since := "2025-08-08")]
 lemma CompactlySupportedContinuousMap.monotone_of_nonneg {Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ}
-    (hΛ : ∀ f, 0 ≤ f → 0 ≤ Λ f) : Monotone Λ := by
-  intro f₁ f₂ h
-  have : 0 ≤ Λ (f₂ - f₁) := by
-    apply hΛ
-    intro x
-    simp only [coe_zero, Pi.zero_apply, coe_sub, Pi.sub_apply, sub_nonneg]
-    exact h x
-  calc Λ f₁ ≤ Λ f₁ + Λ (f₂ - f₁) := by exact (le_add_iff_nonneg_right (Λ f₁)).mpr this
-  _ = Λ (f₁ + (f₂ - f₁)) := by exact Eq.symm (LinearMap.map_add Λ f₁ (f₂ - f₁))
-  _ = Λ f₂ := by congr; exact add_sub_cancel f₁ f₂
+    (hΛ : ∀ f, 0 ≤ f → 0 ≤ Λ f) : Monotone Λ :=
+  (PositiveLinearMap.mk₀ Λ hΛ).monotone
 
 end Monotone
 

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean

@@ -39,8 +39,8 @@ namespace NNRealRMK
 the (Bochner) integral of `f` (as a `ℝ`-valued function) with respect to the `rieszMeasure`
 associated to `Λ` is equal to `Λ f`. -/
 theorem integral_rieszMeasure (f : C_c(X, ℝ≥0)) : ∫ (x : X), (f x : ℝ) ∂(rieszMeasure Λ) = Λ f := by
-  rw [← eq_toRealLinear_toReal Λ f,
-      ← RealRMK.integral_rieszMeasure (toRealLinear_nonneg Λ) f.toReal]
+  rw [← eq_toRealPositiveLinear_toReal Λ f,
+      ← RealRMK.integral_rieszMeasure (toRealPositiveLinear Λ) f.toReal]
   simp [RealRMK.rieszMeasure, NNRealRMK.rieszMeasure]
 
 /-- The **Riesz-Markov-Kakutani representation theorem**: given a positive linear functional `Λ`,

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Yoh Tanimoto. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yoh Tanimoto, Oliver Butterley
 -/
-import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
 import Mathlib.MeasureTheory.Integral.Bochner.Set
+import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
 import Mathlib.Order.Interval.Set.Union
 
 /-!
@@ -45,41 +45,43 @@ namespace RealRMK
 
 variable {X : Type*} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X]
   [BorelSpace X]
-variable {Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ} (hΛ : ∀ f, 0 ≤ f → 0 ≤ Λ f)
+variable (Λ : C_c(X, ℝ) →ₚ[ℝ] ℝ)
 
 /-- The measure induced for `Real`-linear positive functional `Λ`, defined through `toNNRealLinear`
 and the `NNReal`-version of `rieszContent`. This is under the namespace `RealRMK`, while
 `rieszMeasure` without namespace is for `NNReal`-linear `Λ`. -/
-noncomputable def rieszMeasure := (rieszContent (toNNRealLinear Λ hΛ)).measure
+noncomputable def rieszMeasure := (rieszContent (toNNRealLinear Λ)).measure
 
 /-- If `f` assumes values between `0` and `1` and the support is contained in `V`, then
 `Λ f ≤ rieszMeasure V`. -/
 lemma le_rieszMeasure_tsupport_subset {f : C_c(X, ℝ)} (hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1)
-    {V : Set X} (hV : tsupport f ⊆ V) : ENNReal.ofReal (Λ f) ≤ rieszMeasure hΛ V := by
+    {V : Set X} (hV : tsupport f ⊆ V) : ENNReal.ofReal (Λ f) ≤ rieszMeasure Λ V := by
   apply le_trans _ (measure_mono hV)
-  have := Content.measure_eq_content_of_regular (rieszContent (toNNRealLinear Λ hΛ))
-    (contentRegular_rieszContent (toNNRealLinear Λ hΛ)) (⟨tsupport f, f.hasCompactSupport⟩)
+  have := Content.measure_eq_content_of_regular (rieszContent (toNNRealLinear Λ))
+    (contentRegular_rieszContent (toNNRealLinear Λ)) (⟨tsupport f, f.hasCompactSupport⟩)
   rw [← Compacts.coe_mk (tsupport f) f.hasCompactSupport, rieszMeasure, this, rieszContent,
-    ENNReal.ofReal_eq_coe_nnreal (hΛ f fun x ↦ (hf x).1), Content.mk_apply, ENNReal.coe_le_coe]
+    ENNReal.ofReal_eq_coe_nnreal (Λ.map_nonneg fun x ↦ (hf x).1), Content.mk_apply,
+    ENNReal.coe_le_coe]
   apply le_iff_forall_pos_le_add.mpr
   intro _ hε
-  obtain ⟨g, hg⟩ := exists_lt_rieszContentAux_add_pos (toNNRealLinear Λ hΛ)
+  obtain ⟨g, hg⟩ := exists_lt_rieszContentAux_add_pos (toNNRealLinear Λ)
     ⟨tsupport f, f.hasCompactSupport⟩ (Real.toNNReal_pos.mpr hε)
   simp_rw [NNReal.val_eq_coe, Real.toNNReal_coe] at hg
-  refine (monotone_of_nonneg hΛ ?_).trans hg.2.le
+  refine (Λ.mono ?_).trans hg.2.le
   intro x
   by_cases hx : x ∈ tsupport f
   · simpa using le_trans (hf x).2 (hg.1 x hx)
   · simp [image_eq_zero_of_notMem_tsupport hx]
 
 /-- If `f` assumes the value `1` on a compact set `K` then `rieszMeasure K ≤ Λ f`. -/
 lemma rieszMeasure_le_of_eq_one {f : C_c(X, ℝ)} (hf : ∀ x, 0 ≤ f x) {K : Set X}
-    (hK : IsCompact K) (hfK : ∀ x ∈ K, f x = 1) : rieszMeasure hΛ K ≤ ENNReal.ofReal (Λ f) := by
+    (hK : IsCompact K) (hfK : ∀ x ∈ K, f x = 1) : rieszMeasure Λ K ≤ ENNReal.ofReal (Λ f) := by
   rw [← Compacts.coe_mk K hK, rieszMeasure,
-    Content.measure_eq_content_of_regular _ (contentRegular_rieszContent (toNNRealLinear Λ hΛ))]
+    Content.measure_eq_content_of_regular _ (contentRegular_rieszContent (toNNRealLinear Λ))]
   apply ENNReal.coe_le_iff.mpr
   intro p hp
-  rw [← ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_eq_ofReal_iff (hΛ f hf) NNReal.zero_le_coe] at hp
+  rw [← ENNReal.ofReal_coe_nnreal,
+    ENNReal.ofReal_eq_ofReal_iff (Λ.map_nonneg hf) NNReal.zero_le_coe] at hp
   apply csInf_le'
   rw [Set.mem_image]
   use f.nnrealPart
@@ -171,8 +173,8 @@ private lemma exists_nat_large (a' b' : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (N
 
 /-- The main estimate in the proof of the Riesz-Markov-Kakutani: `Λ f` is bounded above by the
 integral of `f` with respect to the `rieszMeasure` associated to `Λ`. -/
-private lemma integral_riesz_aux (f : C_c(X, ℝ)) : Λ f ≤ ∫ x, f x ∂(rieszMeasure hΛ) := by
-  let μ := rieszMeasure hΛ
+private lemma integral_riesz_aux (f : C_c(X, ℝ)) : Λ f ≤ ∫ x, f x ∂(rieszMeasure Λ) := by
+  let μ := rieszMeasure Λ
   let K := tsupport f
   -- Suffices to show that `Λ f ≤ ∫ x, f x ∂μ + ε` for arbitrary `ε`.
   apply le_iff_forall_pos_le_add.mpr
@@ -207,7 +209,7 @@ private lemma integral_riesz_aux (f : C_c(X, ℝ)) : Λ f ≤ ∫ x, f x ∂(rie
     have h_ε' := (div_pos hε'.1 (Nat.cast_pos'.mpr hN))
     have h n x (hx : x ∈ E n) := lt_add_of_le_of_pos ((hE.2.2.1 n x hx).right) hε'.1
     have h' n := Eq.trans_ne
-      (Content.measure_apply (rieszContent (toNNRealLinear Λ hΛ)) (hE.2.2.2 n)).symm (hE' n)
+      (Content.measure_apply (rieszContent (toNNRealLinear Λ)) (hE.2.2.2 n)).symm (hE' n)
     choose V hV using fun n ↦ exists_open_approx f h_ε' (E n) (h' n) (hE.2.2.2 n) (h n)
     exact ⟨V, hV⟩
   -- Define a partition of unity subordinated to the sets `V`
@@ -244,7 +246,6 @@ private lemma integral_riesz_aux (f : C_c(X, ℝ)) : Λ f ≤ ∫ x, f x ∂(rie
     · simp [image_eq_zero_of_notMem_tsupport hx]
   · -- Use that `f ≤ y n + ε'` on `V n`
     gcongr with n hn
-    apply monotone_of_nonneg hΛ
     intro x
     by_cases hx : x ∈ tsupport (g n)
     · rw [smul_eq_mul, mul_comm]
@@ -261,7 +262,7 @@ private lemma integral_riesz_aux (f : C_c(X, ℝ)) : Λ f ≤ ∫ x, f x ∂(rie
     · calc
         _ ≤ μ.real (V n) := by
           apply (ENNReal.ofReal_le_iff_le_toReal _).mp
-          · exact le_rieszMeasure_tsupport_subset hΛ (fun x ↦ hg.2.2.1 n x) (hg.1 n)
+          · exact le_rieszMeasure_tsupport_subset Λ (fun x ↦ hg.2.2.1 n x) (hg.1 n)
           · rw [← lt_top_iff_ne_top]
             apply lt_of_le_of_lt (hV n).2.2
             rw [WithTop.add_lt_top]
@@ -275,9 +276,9 @@ private lemma integral_riesz_aux (f : C_c(X, ℝ)) : Λ f ≤ ∫ x, f x ∂(rie
     rw [← map_sum Λ g _]
     have h x : 0 ≤ (∑ n, g n) x := by simpa using Fintype.sum_nonneg fun n ↦ (hg.2.2.1 n x).1
     apply ENNReal.toReal_le_of_le_ofReal
-    · exact hΛ (∑ n, g n) (fun x ↦ h x)
+    · exact Λ.map_nonneg (fun x ↦ h x)
     · have h' x (hx : x ∈ K) : (∑ n, g n) x = 1 := by simp [hg.2.1 hx]
-      refine rieszMeasure_le_of_eq_one hΛ h f.2 h'
+      refine rieszMeasure_le_of_eq_one Λ h f.2 h'
   · -- Rearrange the sums
     have (n : Fin N) : (|a| + y n + ε') * μ.real (E n) =
         (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n) := by linarith
@@ -324,16 +325,15 @@ private lemma integral_riesz_aux (f : C_c(X, ℝ)) : Λ f ≤ ∫ x, f x ∂(rie
 
 /-- The **Riesz-Markov-Kakutani representation theorem**: given a positive linear functional `Λ`,
 the integral of `f` with respect to the `rieszMeasure` associated to `Λ` is equal to `Λ f`. -/
-theorem integral_rieszMeasure (f : C_c(X, ℝ)) : ∫ x, f x ∂(rieszMeasure hΛ) = Λ f := by
+theorem integral_rieszMeasure (f : C_c(X, ℝ)) : ∫ x, f x ∂(rieszMeasure Λ) = Λ f := by
   -- We apply the result `Λ f ≤ ∫ x, f x ∂(rieszMeasure hΛ)` to `f` and `-f`.
   apply le_antisymm
   -- prove the inequality for `- f`
   · calc
-      _ = - ∫ x, (-f) x ∂(rieszMeasure hΛ) := by simpa using integral_neg' (-f)
-      _ ≤ - Λ (-f) := neg_le_neg (integral_riesz_aux hΛ (-f))
-      _ = Λ (- -f) := Eq.symm (LinearMap.map_neg Λ (- f))
-      _ = _ := by rw [neg_neg]
+      _ = - ∫ x, (-f) x ∂(rieszMeasure Λ) := by simpa using integral_neg' (-f)
+      _ ≤ - Λ (-f) := neg_le_neg (integral_riesz_aux Λ (-f))
+      _ = _ := by simp
   -- prove the inequality for `f`
-  · exact integral_riesz_aux hΛ f
+  · exact integral_riesz_aux Λ f
 
 end RealRMK

Mathlib/Topology/ContinuousMap/CompactlySupported.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Yoh Tanimoto. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yoh Tanimoto
 -/
+import Mathlib.Algebra.Order.Module.PositiveLinearMap
 import Mathlib.Topology.Algebra.Order.Support
 import Mathlib.Topology.ContinuousMap.ZeroAtInfty
 
@@ -488,14 +489,42 @@ end SemilatticeInf
 
 section Lattice
 
-instance [Lattice β] [TopologicalSpace β] [TopologicalLattice β] [Zero β] :
+variable [TopologicalSpace β]
+
+instance [Lattice β] [TopologicalLattice β] [Zero β] :
     Lattice C_c(α, β) :=
   DFunLike.coe_injective.lattice _ coe_sup coe_inf
 
+instance instMulLeftMono [PartialOrder β] [MulZeroClass β] [ContinuousMul β] [MulLeftMono β] :
+    MulLeftMono C_c(α, β) :=
+  ⟨fun _ _ _ hg₁₂ x => mul_le_mul_left' (hg₁₂ x) _⟩
+
+instance instMulRightMono [PartialOrder β] [MulZeroClass β] [ContinuousMul β] [MulRightMono β] :
+    MulRightMono C_c(α, β) :=
+  ⟨fun _ _ _ hg₁₂ x => mul_le_mul_right' (hg₁₂ x) _⟩
+
+instance instAddLeftMono [PartialOrder β] [AddZeroClass β] [ContinuousAdd β] [AddLeftMono β] :
+    AddLeftMono C_c(α, β) :=
+  ⟨fun _ _ _ hg₁₂ x => add_le_add_left (hg₁₂ x) _⟩
+
+instance instAddRightMono [PartialOrder β] [AddZeroClass β] [ContinuousAdd β] [AddRightMono β] :
+    AddRightMono C_c(α, β) :=
+  ⟨fun _ _ _ hg₁₂ x => add_le_add_right (hg₁₂ x) _⟩
+
 -- TODO transfer this lattice structure to `BoundedContinuousFunction`
 
 end Lattice
 
+section IsOrderedAddMonoid
+
+variable [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β]
+variable [PartialOrder β] [IsOrderedAddMonoid β]
+
+instance : IsOrderedAddMonoid C_c(α, β) where
+  add_le_add_left _ _ hfg c := add_le_add_left hfg c
+
+end IsOrderedAddMonoid
+
 /-! ### `C_c` as a functor
 
 For each `β` with sufficient structure, there is a contravariant functor `C_c(-, β)` from the
@@ -764,68 +793,83 @@ lemma nnrealPart_neg_toReal_eq (f : C_c(α, ℝ≥0)) : nnrealPart (-toReal f) =
 section toNNRealLinear
 
 /-- For a positive linear functional `Λ : C_c(α, ℝ) → ℝ`, define a `ℝ≥0`-linear map. -/
-noncomputable def toNNRealLinear (Λ : C_c(α, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ f, 0 ≤ f → 0 ≤ Λ f) :
+noncomputable def toNNRealLinear (Λ : C_c(α, ℝ) →ₚ[ℝ] ℝ) :
     C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0 where
-  toFun f := ⟨Λ (toRealLinearMap f), hΛ _ <| by simp⟩
+  toFun f := ⟨Λ (toRealLinearMap f), Λ.map_nonneg (by simp)⟩
   map_add' f g := by ext; simp
   map_smul' a f := by ext; simp [NNReal.smul_def]
 
 @[simp]
-lemma toNNRealLinear_apply (Λ : C_c(α, ℝ) →ₗ[ℝ] ℝ) (hΛ) (f : C_c(α, ℝ≥0)) :
-    toNNRealLinear Λ hΛ f = Λ (toReal f) := rfl
+lemma toNNRealLinear_apply (Λ : C_c(α, ℝ) →ₚ[ℝ] ℝ) (f : C_c(α, ℝ≥0)) :
+    toNNRealLinear Λ f = Λ (toReal f) := rfl
 
 @[simp]
-lemma toNNRealLinear_inj (Λ₁ Λ₂ : C_c(α, ℝ) →ₗ[ℝ] ℝ) (hΛ₁ hΛ₂) :
-    toNNRealLinear Λ₁ hΛ₁ = toNNRealLinear Λ₂ hΛ₂ ↔ Λ₁ = Λ₂ := by
-  simp only [LinearMap.ext_iff, NNReal.eq_iff, toNNRealLinear_apply]
-  refine ⟨fun h f ↦ ?_, fun h f ↦ by rw [LinearMap.ext h]⟩
+lemma toNNRealLinear_inj (Λ₁ Λ₂ : C_c(α, ℝ) →ₚ[ℝ] ℝ) :
+    toNNRealLinear Λ₁ = toNNRealLinear Λ₂ ↔ Λ₁ = Λ₂ := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
+  ext f
   rw [← nnrealPart_sub_nnrealPart_neg f]
+  simp only [LinearMap.ext_iff, NNReal.eq_iff, toNNRealLinear_apply] at h
   simp_rw [map_sub, h]
 
 end toNNRealLinear
 
-section toRealLinear
-
-/-- For a positive linear functional `Λ : C_c(α, ℝ≥0) → ℝ≥0`, define a `ℝ`-linear map. -/
-noncomputable def toRealLinear (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) : C_c(α, ℝ) →ₗ[ℝ] ℝ where
-  toFun := fun f => Λ (nnrealPart f) - Λ (nnrealPart (- f))
-  map_add' f g := by
-    simp only [neg_add_rev]
-    obtain ⟨h, hh⟩ := exists_add_nnrealPart_add_eq f g
-    rw [← add_zero ((Λ (f + g).nnrealPart).toReal - (Λ (-g + -f).nnrealPart).toReal),
-      ← sub_self (Λ h).toReal, sub_add_sub_comm, ← NNReal.coe_add, ← NNReal.coe_add,
-      ← LinearMap.map_add, ← LinearMap.map_add, hh.1, add_comm (-g) (-f), hh.2]
-    simp only [map_add, NNReal.coe_add]
-    ring
-  map_smul' a f := by
-    rcases le_total 0 a with ha | ha
-    · rw [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f), nnrealPart_smul_pos f ha,
-        nnrealPart_smul_pos (-f) ha]
-      simp [sup_of_le_left ha, mul_sub]
-    · simp only [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f),
-        nnrealPart_smul_neg f ha, nnrealPart_smul_neg (-f) ha, map_smul,
-        NNReal.coe_mul, Real.coe_toNNReal', neg_neg, sup_of_le_left (neg_nonneg.mpr ha)]
-      ring
-
-lemma toRealLinear_apply {Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0} (f : C_c(α, ℝ)) :
-    toRealLinear Λ f = Λ (nnrealPart f) - Λ (nnrealPart (-f)) := rfl
-
-lemma toRealLinear_nonneg (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (g : C_c(α, ℝ)) (hg : 0 ≤ g) :
-    0 ≤ toRealLinear Λ g := by
-  simp [toRealLinear_apply, nnrealPart_neg_eq_zero_of_nonneg hg]
+section toRealPositiveLinear
+
+/-- For a positive linear functional `Λ : C_c(α, ℝ≥0) → ℝ≥0`, define a positive `ℝ`-linear map. -/
+noncomputable def toRealPositiveLinear (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) : C_c(α, ℝ) →ₚ[ℝ] ℝ :=
+  PositiveLinearMap.mk₀
+    { toFun := fun f => Λ (nnrealPart f) - Λ (nnrealPart (- f))
+      map_add' f g := by
+        simp only [neg_add_rev]
+        obtain ⟨h, hh⟩ := exists_add_nnrealPart_add_eq f g
+        rw [← add_zero ((Λ (f + g).nnrealPart).toReal - (Λ (-g + -f).nnrealPart).toReal),
+          ← sub_self (Λ h).toReal, sub_add_sub_comm, ← NNReal.coe_add, ← NNReal.coe_add,
+          ← LinearMap.map_add, ← LinearMap.map_add, hh.1, add_comm (-g) (-f), hh.2]
+        simp only [map_add, NNReal.coe_add]
+        ring
+      map_smul' a f := by
+        rcases le_total 0 a with ha | ha
+        · rw [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f), nnrealPart_smul_pos f ha,
+            nnrealPart_smul_pos (-f) ha]
+          simp [sup_of_le_left ha, mul_sub]
+        · simp only [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f),
+            nnrealPart_smul_neg f ha, nnrealPart_smul_neg (-f) ha, map_smul,
+            NNReal.coe_mul, Real.coe_toNNReal', neg_neg, sup_of_le_left (neg_nonneg.mpr ha)]
+          ring }
+    (fun g hg ↦ by simp [nnrealPart_neg_eq_zero_of_nonneg hg])
+
+lemma toRealPositiveLinear_apply {Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0} (f : C_c(α, ℝ)) :
+    toRealPositiveLinear Λ f = Λ (nnrealPart f) - Λ (nnrealPart (-f)) := rfl
 
 @[simp]
-lemma eq_toRealLinear_toReal (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (f : C_c(α, ℝ≥0)) :
-    toRealLinear Λ (toReal f) = Λ f := by
-  simp [toRealLinear_apply]
+lemma eq_toRealPositiveLinear_toReal (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (f : C_c(α, ℝ≥0)) :
+    toRealPositiveLinear Λ (toReal f) = Λ f := by
+  simp [toRealPositiveLinear_apply]
 
 @[simp]
-lemma eq_toNNRealLinear_toRealLinear (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) :
-    toNNRealLinear (toRealLinear Λ) (toRealLinear_nonneg Λ) = Λ := by
+lemma eq_toNNRealLinear_toRealPositiveLinear (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) :
+    toNNRealLinear (toRealPositiveLinear Λ) = Λ := by
   ext f
   simp
 
-end toRealLinear
+@[deprecated (since := "2025-08-08")]
+alias toRealLinear := toRealPositiveLinear
+
+@[deprecated (since := "2025-08-08")]
+alias toRealLinear_apply := toRealPositiveLinear_apply
+
+@[deprecated map_nonneg (since := "2025-08-08")]
+lemma toRealLinear_nonneg (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (g : C_c(α, ℝ)) (hg : 0 ≤ g) :
+    0 ≤ toRealPositiveLinear Λ g := map_nonneg _ hg
+
+@[deprecated (since := "2025-08-08")]
+alias eq_toRealLinear_toReal := eq_toRealPositiveLinear_toReal
+
+@[deprecated (since := "2025-08-08")]
+alias eq_toNNRealLinear_toRealLinear := eq_toNNRealLinear_toRealPositiveLinear
+
+end toRealPositiveLinear
 
 end CompactlySupportedContinuousMap