English
For Real-linear positive Λ, the Real RMK framework gives a representation by a measure that matches the integral on simple functions and extends to f ∈ C_c(X,ℝ).
Русский
Для реал- линейного положительного Λ система RMK задаёт меру, которая согласуется с интегралом на простых функциях и распространяется на f ∈ C_c(X,ℝ).
LaTeX
$$$\\int f\, d(\\text{rieszMeasure }Λ)= Λ f$ for f ∈ C_c(X,ℝ).$$
Lean4
/-- If `f` assumes values between `0` and `1` and the support is contained in `V`, then
`Λ f ≤ rieszMeasure V`. -/
theorem 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 Λ V :=
by
apply le_trans _ (measure_mono hV)
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 (Λ.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 Λ) ⟨tsupport f, f.hasCompactSupport⟩ (Real.toNNReal_pos.mpr hε)
simp_rw [NNReal.val_eq_coe, Real.toNNReal_coe] at hg
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]
