English
For a suitable f with 0 ≤ f ≤ 1, the finite content bound implies a bound by rieszMeasure Λ on K.
Русский
Для подходящей f с 0 ≤ f ≤ 1 ограничение контента приводит к ограничению rieszMeasure Λ на K.
LaTeX
$$$\\text{If }0\\le f\\le 1\\text{ and } tsupport(f)\\subseteq K,\\ λΛ(K) \\le \\text{rieszMeasure}(K).$$$
Lean4
theorem contentRegular_rieszContent : (rieszContent Λ).ContentRegular :=
by
intro K
simp only [rieszContent, le_antisymm_iff, le_iInf_iff, ENNReal.coe_le_coe, Content.mk_apply]
refine ⟨fun K' hK' ↦ rieszContentAux_mono Λ (hK'.trans interior_subset), ?_⟩
rw [iInf_le_iff]
intro b hb
rw [rieszContentAux, ENNReal.le_coe_iff]
have : b < ⊤ := by
obtain ⟨F, hF⟩ := exists_compact_superset K.2
exact (le_iInf_iff.mp (hb ⟨F, hF.1⟩) hF.2).trans_lt ENNReal.coe_lt_top
refine ⟨b.toNNReal, (ENNReal.coe_toNNReal this.ne).symm, NNReal.coe_le_coe.mp ?_⟩
apply le_iff_forall_pos_le_add.mpr
intro ε hε
lift ε to ℝ≥0 using hε.le
obtain ⟨f, hfleoneonK, hfle⟩ := exists_lt_rieszContentAux_add_pos Λ K (Real.toNNReal_pos.mpr hε)
rw [rieszContentAux, Real.toNNReal_of_nonneg hε.le, ← NNReal.coe_lt_coe] at hfle
refine ((le_iff_forall_one_lt_le_mul₀ (zero_le (Λ f))).mpr fun α hα ↦ ?_).trans hfle.le
rw [mul_comm, ← smul_eq_mul, ← map_smul]
set K' := f ⁻¹' Ici α⁻¹
have hKK' : ↑K ⊆ interior K' :=
subset_interior_iff.2
⟨f ⁻¹' Ioi α⁻¹, isOpen_Ioi.preimage f.1.2, fun x hx ↦ (inv_lt_one_of_one_lt₀ hα).trans_le (hfleoneonK x hx),
preimage_mono Ioi_subset_Ici_self⟩
have hK'cp : IsCompact K' :=
.of_isClosed_subset f.2 (isClosed_Ici.preimage f.1.2) fun x hx ↦
subset_closure ((inv_pos_of_pos <| zero_lt_one.trans hα).trans_le hx).ne'
set hb' := hb ⟨K', hK'cp⟩
simp only [Compacts.coe_mk, le_iInf_iff] at hb'
exact
(ENNReal.toNNReal_mono (by simp) <| hb' hKK').trans <|
csInf_le' ⟨α • f, fun x ↦ (inv_le_iff_one_le_mul₀' (zero_lt_one.trans hα)).mp, by simp⟩
