English
If a compactly supported nonnegative function f satisfies 0 ≤ f ≤ 1 on X and its tsupport is contained in K, then λ(K) ≤ Λf.
Русский
Если f лежит между 0 и 1 и tsupport f ⊆ K, то λ(K) ≤ Λ(f).
LaTeX
$$$\\lambda(K) \\le Λ f \\quad\\text{whenever } ∀x,0≤f(x)\\text{ and } tsupport(f) ⊆ K.$$$
Lean4
/-- The Riesz content can be approximated arbitrarily well by evaluating the positive linear
functional on test functions: for any `ε > 0`, there exists a compactly supported continuous
nonnegative function `f` on `X` such that `f ≥ 1` on `K` and such that `λ(K) ≤ Λ f < λ(K) + ε`. -/
theorem exists_lt_rieszContentAux_add_pos (K : Compacts X) {ε : ℝ≥0} (εpos : 0 < ε) :
∃ f : C_c(X, ℝ≥0), (∀ x ∈ K, (1 : ℝ≥0) ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε := by
--choose a test function `f` s.t. `Λf = α < λ(K) + ε`
obtain ⟨α, ⟨⟨f, f_hyp⟩, α_hyp⟩⟩ :=
exists_lt_of_csInf_lt (rieszContentAux_image_nonempty Λ K) (lt_add_of_pos_right (rieszContentAux Λ K) εpos)
refine ⟨f, f_hyp.left, ?_⟩
rw [f_hyp.right]
exact α_hyp
