English
Given a positive linear functional Λ on C_c(α,ℝ≥0), there is a corresponding real-valued positive linear map on C_c(α,ℝ) defined by T(f) = Λ(nnrealPart(f)) − Λ(nnrealPart(−f)). This constructs a real-positive linear functional from a nonnegative one.
Русский
Пусть Λ — положительная линейная функциональная карта на C_c(α,ℝ≥0). Тогда существует соответствующая линейная карта на C_c(α,ℝ), заданная T(f) = Λ(nnrealPart(f)) − Λ(nnrealPart(−f)), которая является положительной линейной функциональной картой в вещественных числах.
LaTeX
$$$T(f) = \Lambda\big((f)_{\mathbb{R}_{\ge 0}}^{\,nnreal}\big) - \Lambda\big(((−f)_{\mathbb{R}_{\ge 0}})^{nnreal}\big).$$$
Lean4
/-- 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])
