English
The Riesz content λ associated to Λ is monotone with respect to compact subsets: if K1 ⊆ K2, then λ(K1) ≤ λ(K2).
Русский
Контент Рiesz λ, связанный с Λ, монотонен по отношению к компактным множествам: если K1 ⊆ K2, то λ(K1) ≤ λ(K2).
LaTeX
$$$\\lambda(K_{1}) \\le \\lambda(K_{2})\\quad \\text{whenever } K_{1} \\subseteq K_{2}. $$$
Lean4
/-- For any compact subset `K ⊆ X`, there exist some compactly supported continuous nonnegative
functions `f` on `X` such that `f ≥ 1` on `K`. -/
theorem rieszContentAux_image_nonempty (K : Compacts X) :
(Λ '' {f : C_c(X, ℝ≥0) | ∀ x ∈ K, (1 : ℝ≥0) ≤ f x}).Nonempty :=
by
rw [image_nonempty]
obtain ⟨V, hVcp, hKsubintV⟩ := exists_compact_superset K.2
have hIsCompact_closure_interior : IsCompact (closure (interior V)) :=
by
apply IsCompact.of_isClosed_subset hVcp isClosed_closure
nth_rw 2 [← closure_eq_iff_isClosed.mpr (IsCompact.isClosed hVcp)]
exact closure_mono interior_subset
obtain ⟨f, hsuppfsubV, hfeq1onK, hfinicc⟩ :=
exists_tsupport_one_of_isOpen_isClosed isOpen_interior hIsCompact_closure_interior (IsCompact.isClosed K.2)
hKsubintV
have hfHasCompactSupport : HasCompactSupport f :=
IsCompact.of_isClosed_subset hVcp (isClosed_tsupport f) (Set.Subset.trans hsuppfsubV interior_subset)
use nnrealPart ⟨f, hfHasCompactSupport⟩
intro x hx
apply le_of_eq
simp only [nnrealPart_apply, CompactlySupportedContinuousMap.coe_mk]
rw [← Real.toNNReal_one, Real.toNNReal_eq_toNNReal_iff (zero_le_one' ℝ) (hfinicc x).1]
exact hfeq1onK.symm hx
