From 55406feb85ce92d7da24702636dc1dcc359fed33 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 17:37:14 +0530 Subject: [PATCH 1/2] Fill finite additivity of counting measure. --- Analysis/MeasureTheory/Section_1_4_3.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean index c95f4f67..7a3be98a 100644 --- a/Analysis/MeasureTheory/Section_1_4_3.lean +++ b/Analysis/MeasureTheory/Section_1_4_3.lean @@ -177,7 +177,8 @@ noncomputable def FinitelyAdditiveMeasure.counting (X:Type*) : FinitelyAdditiveM measure := fun E => ENat.card E measure_pos := fun _ _ => by positivity measure_empty := by simp - measure_finite_additive := by sorry + measure_finite_additive := fun E F _ _ hdisj => + (ENat.card_union_eq_add_card_of_disjoint hdisj).symm } /-- Boolean algebras are closed under intersection. -/ From ac8ce12a07a5fef20e802e69de3f4ac328c8de5d Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 30 Sep 2026 16:13:59 +0530 Subject: [PATCH 2/2] Use the set cardinality union theorem for counting measure --- Analysis/MeasureTheory/Section_1_4_3.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean index 7a3be98a..999deff6 100644 --- a/Analysis/MeasureTheory/Section_1_4_3.lean +++ b/Analysis/MeasureTheory/Section_1_4_3.lean @@ -177,8 +177,9 @@ noncomputable def FinitelyAdditiveMeasure.counting (X:Type*) : FinitelyAdditiveM measure := fun E => ENat.card E measure_pos := fun _ _ => by positivity measure_empty := by simp - measure_finite_additive := fun E F _ _ hdisj => - (ENat.card_union_eq_add_card_of_disjoint hdisj).symm + measure_finite_additive := fun E F _ _ hdisj => by + simp only [ENat.card_coe_set_eq, Set.encard_union_eq hdisj] + norm_cast } /-- Boolean algebras are closed under intersection. -/