From 8997074a2c984031077d1939f319f00bb6a5fa39 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 16:28:49 +0530 Subject: [PATCH] Fill scalar multiplication of finitely additive measures. Nonnegativity and empty come from EReal; additivity is left-distributivity of the ENNReal coercion. --- Analysis/MeasureTheory/Section_1_4_3.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean index 60d13f856..de895913a 100644 --- a/Analysis/MeasureTheory/Section_1_4_3.lean +++ b/Analysis/MeasureTheory/Section_1_4_3.lean @@ -85,9 +85,11 @@ noncomputable instance FinitelyAdditiveMeasure.instSmul {X:Type*} {B: ConcreteBo smul := fun c μ => { measure := fun A => c * μ.measure A - measure_pos := by sorry - measure_empty := by sorry - measure_finite_additive := by sorry + measure_pos := fun A hA => mul_nonneg (zero_le _) (μ.measure_pos A hA) + measure_empty := by simp [μ.measure_empty] + measure_finite_additive := fun E F hE hF hdisj => by + simp [μ.measure_finite_additive E F hE hF hdisj] + exact mul_add (c : EReal) _ _ } }