From 463e9dca2e63629bb3dd65b196615df29e58df66 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Sat, 27 Jun 2020 00:21:31 -0400
Subject: [PATCH] define scalar multiplication of ennreal with measure

---
 src/measure_theory/measure_space.lean | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/measure_theory/measure_space.lean b/src/measure_theory/measure_space.lean
index 779850d4642ed..9b463b10ae580 100644
--- a/src/measure_theory/measure_space.lean
+++ b/src/measure_theory/measure_space.lean
@@ -25,7 +25,7 @@ extension of the restricted measure.
 In the first part of the file we define operations on arbitrary functions defined on measurable
 sets.
 
-Measures on `α` form a complete lattice.
+Measures on `α` form a complete lattice, and are closed under scalar multiplication with `ennreal`.
 
 Given a measure, the null sets are the sets where `μ s = 0`, where `μ` denotes the corresponding
 outer measure (so `s` might not be measurable). We can then define the completion of `μ` as the
@@ -709,6 +709,25 @@ instance : complete_lattice (measure α) :=
   le_inf       := assume a b c hac hbc, le_Inf $ by simp [*, or_imp_distrib] {contextual := tt},
   .. measure.partial_order, .. measure.order_top, .. measure.order_bot }
 
+instance : has_scalar ennreal (measure α) :=
+⟨λ x m, {
+  m_Union := λ s hs h2s, by { simp only [measure_of_eq_coe, to_outer_measure_apply, smul_apply,
+    ennreal.tsum_mul_left, measure_Union h2s hs] },
+  trimmed := by { convert trim_smul m.to_outer_measure x, ext1 s,
+    simp only [m.trimmed, smul_apply, measure_of_eq_coe] },
+  ..x • m.to_outer_measure }⟩
+
+@[simp] theorem smul_apply (a : ennreal) (m : measure α) (s : set α) : (a • m) s = a * m s := rfl
+
+instance : semimodule ennreal (measure α) :=
+{ smul_add := λ a m₁ m₂, ext $ λ s hs, mul_add _ _ _,
+  add_smul := λ a b m, ext $ λ s hs, add_mul _ _ _,
+  mul_smul := λ a b m, ext $ λ s hs, mul_assoc _ _ _,
+  one_smul := λ m, ext $ λ s hs, one_mul _,
+  zero_smul := λ m, ext $ λ s hs, zero_mul _,
+  smul_zero := λ a, ext $ λ s hs, mul_zero _,
+  ..measure.has_scalar }
+
 end
 
 /-- The pushforward of a measure. It is defined to be `0` if `f` is not a measurable function. -/