English
If m is σ-additive on a set ring, then m is σ-subadditive.
Русский
Если m является σ-аддитивным на кольце множеств, значит оно σ-субаддитивно.
LaTeX
$$m.IsSigmaSubadditive$$
Lean4
/-- If an additive content is σ-additive on a set ring, then it is σ-subadditive. -/
theorem isSigmaSubadditive_of_addContent_iUnion_eq_tsum (hC : IsSetRing C)
(m_iUnion :
∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : (⋃ i, f i) ∈ C) (_hf_disj : Pairwise (Disjoint on f)),
m (⋃ i, f i) = ∑' i, m (f i)) :
m.IsSigmaSubadditive := by
intro f hf hf_Union
have h_tendsto : Tendsto (fun n ↦ m (partialSups f n)) atTop (𝓝 (m (⋃ i, f i))) :=
by
rw [← iSup_eq_iUnion, ← iSup_partialSups_eq]
refine
tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion (partialSups_monotone f)
(hC.partialSups_mem hf) ?_
rwa [← iSup_eq_iUnion, iSup_partialSups_eq]
have h_tendsto' : Tendsto (fun n ↦ ∑ i ∈ range (n + 1), m (f i)) atTop (𝓝 (∑' i, m (f i))) :=
by
rw [tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (f i))) 1]
exact ENNReal.tendsto_nat_tsum _
refine le_of_tendsto_of_tendsto' h_tendsto h_tendsto' fun _ ↦ ?_
rw [partialSups_eq_biUnion_range]
exact addContent_biUnion_le hC (fun _ _ ↦ hf _)
