toNNRealLinear — Mathlib

English

There is a nonnegative-linear map toNNRealLinear Λ : C_c(α, ℝ≥0) →ℝ≥0 defined by f ↦ ⟨Λ (toRealLinearMap f), Λ.map_nonneg (by simp)⟩, with linearity properties.

Русский

Существуют линейные над множеством ℝ≥0 отображения toNNRealLinear Λ : C_c(α, ℝ≥0) →ℝ≥0, заданные как f ↦ ⟨Λ (toRealLinearMap f), Λ.map_nonneg (по доказательству)⟩, удовлетворяющие линейности.

LaTeX

$$$ toNNRealLinear(\Lambda)(f) = \langle \Lambda(\mathrm{toRealLinearMap} f), \Lambda(\mathrm{map\_nonneg}(\text{proof})) \rangle $$$

Lean4

/-- For a positive linear functional `Λ : C_c(α, ℝ) → ℝ`, define a `ℝ≥0`-linear map. -/
noncomputable def toNNRealLinear (Λ : C_c(α, ℝ) →ₚ[ℝ] ℝ) : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
    where
  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]

Похожие утверждения