English
For a finite measure μ, the data f ↦ μ.testAgainstNN f endows μ with a continuous linear functional on bounded nonnegative test functions, i.e., a weak dual element.
Русский
Для конечной меры μ функция f ↦ μ.testAgainstNN f определяет непрерывный линейный функционал на ограниченных неотрицательных тест-функциях, т. е. элемент слабого двойственного пространства.
LaTeX
$$$ \forall \mu : \text{FiniteMeasure } \Omega, \; \text{toWeakDualBCNN}(\mu) \text{ is the functional } f \mapsto \mu.testAgainstNN f. $$$
Lean4
/-- Finite measures yield elements of the `WeakDual` of bounded continuous nonnegative
functions via `MeasureTheory.FiniteMeasure.testAgainstNN`, i.e., integration. -/
def toWeakDualBCNN (μ : FiniteMeasure Ω) : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)
where
toFun f := μ.testAgainstNN f
map_add' := testAgainstNN_add μ
map_smul' := testAgainstNN_smul μ
cont := μ.testAgainstNN_lipschitz.continuous
