From 2e4b80732604bf3021229d599c690994a5d97b38 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 17:34:30 +0530 Subject: [PATCH] Fill restriction of a finitely additive measure to a measurable subset. --- Analysis/MeasureTheory/Section_1_4_3.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean index 60d13f856..6024eb004 100644 --- a/Analysis/MeasureTheory/Section_1_4_3.lean +++ b/Analysis/MeasureTheory/Section_1_4_3.lean @@ -112,9 +112,14 @@ noncomputable instance FinitelyAdditiveMeasure.instDistribMulAction {X:Type*} {B def FinitelyAdditiveMeasure.restrict {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) (A:Set X) (hA:B.measurable A) : FinitelyAdditiveMeasure (B.restrict A) := { measure := fun E => μ.measure E - measure_pos := by sorry - measure_empty := by sorry - measure_finite_additive := by sorry + measure_pos := fun E hE => + μ.measure_pos (Subtype.val '' E) ((B.restrict_iff hA E).mp hE) + measure_empty := by + simpa using μ.measure_empty + measure_finite_additive := fun E F hE hF hdisj => + μ.measure_finite_additive (Subtype.val '' E) (Subtype.val '' F) + ((B.restrict_iff hA E).mp hE) ((B.restrict_iff hA F).mp hF) + (hdisj.image Subtype.val) } /-- Example 1.4.26 (Counting a measure) -/