English
If Λ is determined by equality of Integrals, the associated rieszMeasure is well-defined and unique.
Русский
Если Λ задаётся через равенство интегралов, то соответствующая rieszMeasure существует и уникальна.
LaTeX
$$$\\text{rieszMeasure }Λ$ is uniquely determined by $\\int f\, d(\\text{rieszMeasure }Λ) = Λ f$.$$
Lean4
/-- If `f` assumes the value `1` on a compact set `K` then `rieszMeasure K ≤ Λ f`. -/
theorem 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 Λ K ≤ ENNReal.ofReal (Λ f) :=
by
rw [← Compacts.coe_mk K hK, rieszMeasure,
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 (Λ.map_nonneg hf) NNReal.zero_le_coe] at hp
apply csInf_le'
rw [Set.mem_image]
use f.nnrealPart
simp_rw [Set.mem_setOf_eq, nnrealPart_apply, Real.one_le_toNNReal]
refine ⟨(fun x hx ↦ Eq.ge (hfK x hx)), ?_⟩
apply NNReal.eq
rw [toNNRealLinear_apply, show f.nnrealPart.toReal = f by ext z; simp [hf z], hp]
