English
The Riesz content λ is finitely subadditive: λ(K1 ∪ K2) ≤ λ(K1) + λ(K2) for compact K1,K2.
Русский
Контент Рiesz повседневно удовлетворяет конечной субаддитивности: λ(K1 ∪ K2) ≤ λ(K1) + λ(K2).
LaTeX
$$$\\lambda(K_{1} \\cup K_{2}) \\le λ(K_{1}) + λ(K_{2}).$$$
Lean4
/-- The Riesz content `λ` associated to a given positive linear functional `Λ` is
finitely subadditive: `λ(K₁ ∪ K₂) ≤ λ(K₁) + λ(K₂)` for any compact subsets `K₁, K₂ ⊆ X`. -/
theorem rieszContentAux_sup_le (K1 K2 : Compacts X) :
rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 :=
by
apply _root_.le_of_forall_pos_le_add
intro ε εpos
obtain ⟨f1, f_test_function_K1⟩ := exists_lt_rieszContentAux_add_pos Λ K1 (half_pos εpos)
obtain ⟨f2, f_test_function_K2⟩ :=
exists_lt_rieszContentAux_add_pos Λ K2
(half_pos εpos)
--let `f := f1 + f2` test function for the content of `K`
have f_test_function_union : ∀ x ∈ K1 ⊔ K2, (1 : ℝ≥0) ≤ (f1 + f2) x :=
by
rintro x (x_in_K1 | x_in_K2)
· exact le_add_right (f_test_function_K1.left x x_in_K1)
·
exact
le_add_left
(f_test_function_K2.left x x_in_K2)
--use that `Λf` is an upper bound for `λ(K1⊔K2)`
apply (rieszContentAux_le Λ f_test_function_union).trans (le_of_lt _)
rw [map_add]
--use that `Λfi` are lower bounds for `λ(Ki) + ε/2`
apply lt_of_lt_of_le (_root_.add_lt_add f_test_function_K1.right f_test_function_K2.right) (le_of_eq _)
rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]
