English
For any nonnegative f with controlled tsupport on a compact K, the bound holds for rieszMeasure: Λ f ≤ rieszMeasure K.
Русский
Для любого неотрицательного f с ограниченной опорой на компакт K верно Λ f ≤ rieszMeasure K.
LaTeX
$$$Λ f ≤ \\text{rieszMeasure}(K)$ given appropriate support conditions.$$
Lean4
theorem le_rieszMeasure_of_isCompact_tsupport_subset {f : C_c(X, ℝ≥0)} (hf : ∀ x, f x ≤ 1) {K : Set X}
(hK : IsCompact K) (h : tsupport f ⊆ K) : .ofNNReal (Λ f) ≤ rieszMeasure Λ K :=
by
rw [← TopologicalSpace.Compacts.coe_mk K hK]
simp only [rieszMeasure, Content.measure_eq_content_of_regular (rieszContent Λ) (contentRegular_rieszContent Λ)]
simp only [rieszContent, ENNReal.coe_le_coe, Content.mk_apply]
apply le_iff_forall_pos_le_add.mpr
intro ε hε
obtain ⟨g, hg⟩ := exists_lt_rieszContentAux_add_pos Λ ⟨K, hK⟩ hε
apply le_trans _ hg.2.le
apply monotone_of_nnreal Λ
intro x
simp only
by_cases hx : x ∈ tsupport f
· exact le_trans (hf x) (hg.1 x (Set.mem_of_subset_of_mem h hx))
· rw [image_eq_zero_of_notMem_tsupport hx]
exact zero_le (g x)
