From 50ddf86a1ce8262f34b46312e3d81547cca69ff8 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 17:36:27 +0530 Subject: [PATCH] Fill the ENNReal action on countably additive measures. --- Analysis/MeasureTheory/Section_1_4_3.lean | 27 +++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean index 60d13f856..e73a142a3 100644 --- a/Analysis/MeasureTheory/Section_1_4_3.lean +++ b/Analysis/MeasureTheory/Section_1_4_3.lean @@ -231,10 +231,29 @@ noncomputable instance CountablyAdditiveMeasure.instSmul {X:Type*} {B: ConcreteS noncomputable instance CountablyAdditiveMeasure.instDistribMulAction {X:Type*} {B: ConcreteSigmaAlgebra X} : DistribMulAction ENNReal (CountablyAdditiveMeasure B) := { - smul_zero := by sorry, - smul_add := by sorry, - one_smul := by sorry, - mul_smul := by sorry + smul_zero := by + intro c + congr 1 + ext A + simp + smul_add := by + intro c μ ν + cases μ; cases ν + congr 1 + ext A + exact left_distrib (c : EReal) _ _ + one_smul := by + intro μ + cases μ + congr 1 + ext A + exact one_smul EReal _ + mul_smul := by + intro a b μ + cases μ + congr 1 + ext A + exact mul_assoc (a : EReal) _ _ } /-- Exercise 1.4.22(ii) -/