feat(measure_theory/measure): generalize scalar actions (#12187)

As a result of this change, many smul lemmas now also apply to `nat` and `nnreal`, which allows some lemmas to be removed.

src/measure_theory/covering/differentiation.lean

@@ -363,7 +363,7 @@ begin
       end
     ... ≤ ρ (to_measurable (ρ + μ) (u m) ∩ w n) : begin
         rw [← coe_nnreal_smul_apply],
-        refine v.measure_le_of_frequently_le _ (absolutely_continuous.rfl.coe_nnreal_smul _) _ _,
+        refine v.measure_le_of_frequently_le _ (absolutely_continuous.rfl.smul _) _ _,
         assume x hx,
         have L : tendsto (λ (a : set α), ρ a / μ a) (v.filter_at x) (𝓝 (v.lim_ratio ρ x)) :=
           tendsto_nhds_lim hx.2.1.1,
@@ -460,7 +460,7 @@ begin
       end
     ... ≤ ρ s :
       by { rw [A, mul_zero, add_zero], exact measure_mono (inter_subset_left _ _) },
-  refine v.measure_le_of_frequently_le _ (absolutely_continuous.rfl.coe_nnreal_smul _) _ _,
+  refine v.measure_le_of_frequently_le _ (absolutely_continuous.rfl.smul _) _ _,
   assume x hx,
   have I : ∀ᶠ a in v.filter_at x, (q : ℝ≥0∞) < ρ a / μ a := (tendsto_order.1 hx.2).1 _ (h hx.1),
   apply I.frequently.mono (λ a ha, _),

src/measure_theory/decomposition/lebesgue.lean

@@ -663,7 +663,7 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
             measure.sub_apply (hA.inter hE₁) hle,
             ennreal.to_real_sub_of_le _ (ne_of_lt (measure_lt_top _ _)), sub_nonneg,
             le_sub_iff_add_le, ← ennreal.to_real_add, ennreal.to_real_le_to_real,
-            measure.coe_nnreal_smul, pi.smul_apply, with_density_apply _ (hA.inter hE₁),
+            measure.coe_smul, pi.smul_apply, with_density_apply _ (hA.inter hE₁),
             show ε • ν (A ∩ E) = (ε : ℝ≥0∞) * ν (A ∩ E), by refl,
             ← set_lintegral_const, ← lintegral_add measurable_const hξm] at this,
       { rw [ne.def, ennreal.add_eq_top, not_or_distrib],

src/measure_theory/integral/set_to_l1.lean

@@ -124,7 +124,7 @@ lemma of_smul_measure (c : ℝ≥0∞) (hc_ne_top : c ≠ ∞) (hT : fin_meas_ad
   fin_meas_additive μ T :=
 begin
   refine of_eq_top_imp_eq_top (λ s hs hμs, _) hT,
-  rw [measure.smul_apply, with_top.mul_eq_top_iff] at hμs,
+  rw [measure.smul_apply, smul_eq_mul, with_top.mul_eq_top_iff] at hμs,
   simp only [hc_ne_top, or_false, ne.def, false_and] at hμs,
   exact hμs.2,
 end
@@ -133,7 +133,7 @@ lemma smul_measure (c : ℝ≥0∞) (hc_ne_zero : c ≠ 0) (hT : fin_meas_additi
   fin_meas_additive (c • μ) T :=
 begin
   refine of_eq_top_imp_eq_top (λ s hs hμs, _) hT,
-  rw [measure.smul_apply, with_top.mul_eq_top_iff],
+  rw [measure.smul_apply, smul_eq_mul, with_top.mul_eq_top_iff],
   simp only [hc_ne_zero, true_and, ne.def, not_false_iff],
   exact or.inl hμs,
 end
@@ -270,7 +270,7 @@ begin
   refine ⟨hT.1.of_eq_top_imp_eq_top h, λ s hs hμs, _⟩,
   have hcμs : c • μ s ≠ ∞, from mt (h s hs) hμs.ne,
   rw smul_eq_mul at hcμs,
-  simp_rw [dominated_fin_meas_additive, measure.smul_apply, to_real_mul] at hT,
+  simp_rw [dominated_fin_meas_additive, measure.smul_apply, smul_eq_mul, to_real_mul] at hT,
   refine (hT.2 s hs hcμs.lt_top).trans (le_of_eq _),
   ring,
 end
@@ -1644,7 +1644,7 @@ begin
   { intros c s hs hμs,
     have hμ's : μ' s ≠ ∞,
     { refine ((hμ'_le s hs).trans_lt _).ne,
-      rw measure.smul_apply,
+      rw [measure.smul_apply, smul_eq_mul],
       exact ennreal.mul_lt_top hc' hμs.ne, },
     rw [set_to_fun_indicator_const hT hs hμs.ne, set_to_fun_indicator_const hT' hs hμ's], },
   { intros f₂ g₂ h_dish hf₂ hg₂ h_eq_f h_eq_g,
@@ -1702,8 +1702,8 @@ begin
   refine set_to_fun_measure_zero' hT (λ s hs hμs, _),
   rw lt_top_iff_ne_top at hμs,
   simp only [true_and, measure.smul_apply, with_top.mul_eq_top_iff, eq_self_iff_true, top_ne_zero,
-    ne.def, not_false_iff, not_or_distrib, not_not] at hμs,
-  simp only [hμs.right, measure.smul_apply, mul_zero],
+    ne.def, not_false_iff, not_or_distrib, not_not, smul_eq_mul] at hμs,
+  simp only [hμs.right, measure.smul_apply, mul_zero, smul_eq_mul],
 end
 
 lemma set_to_fun_congr_smul_measure (c : ℝ≥0∞) (hc_ne_top : c ≠ ∞)

src/measure_theory/measure/haar.lean

@@ -591,7 +591,7 @@ begin
   ext1 s hs,
   have := measure_mul_measure_eq μ (haar_measure K₀) K₀.compact hs,
   rw [haar_measure_self, one_mul] at this,
-  rw [← this (by norm_num), smul_apply],
+  rw [← this (by norm_num), smul_apply, smul_eq_mul],
 end
 
 @[to_additive]

src/measure_theory/measure/hausdorff.lean

@@ -349,8 +349,8 @@ begin
   refine λ s, le_of_tendsto_of_tendsto (mk_metric'.tendsto_pre _ s)
     (ennreal.tendsto.const_mul (mk_metric'.tendsto_pre _ s) (or.inr hc))
     (mem_of_superset (Ioo_mem_nhds_within_Ioi ⟨le_rfl, hr0⟩) (λ r' hr', _)),
-  simp only [mem_set_of_eq, mk_metric'.pre],
-  rw [← smul_apply, smul_bounded_by hc],
+  simp only [mem_set_of_eq, mk_metric'.pre, ring_hom.id_apply],
+  rw [←smul_eq_mul, ← smul_apply, smul_bounded_by hc],
   refine le_bounded_by.2 (λ t, (bounded_by_le _).trans _) _,
   simp only [smul_eq_mul, pi.smul_apply, extend, infi_eq_if],
   split_ifs with ht ht,
@@ -587,7 +587,7 @@ mk_metric_le_liminf_sum s r hr t ht hst _
 lemma hausdorff_measure_zero_or_top {d₁ d₂ : ℝ} (h : d₁ < d₂) (s : set X) :
   μH[d₂] s = 0 ∨ μH[d₁] s = ∞ :=
 begin
-  by_contra' H, 
+  by_contra' H,
   suffices : ∀ (c : ℝ≥0), c ≠ 0 → μH[d₂] s ≤ c * μH[d₁] s,
   { rcases ennreal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩,
     exact hc.not_le (this c (pos_iff_ne_zero.1 hc0)) },

src/measure_theory/measure/lebesgue.lean

@@ -225,11 +225,11 @@ begin
   cases lt_or_gt_of_ne h with h h,
   { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt $ neg_pos.2 h),
       measure.map_apply (measurable_const_mul a) measurable_set_Ioo, neg_sub_neg,
-      neg_mul, preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub,
+      neg_mul, preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul,
       mul_div_cancel' _ (ne_of_lt h)] },
   { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt h),
       measure.map_apply (measurable_const_mul a) measurable_set_Ioo, preimage_const_mul_Ioo _ _ h,
-      abs_of_pos h, mul_sub, mul_div_cancel' _ (ne_of_gt h)] }
+      abs_of_pos h, mul_sub, mul_div_cancel' _ (ne_of_gt h), smul_eq_mul] }
 end
 
 lemma map_volume_mul_left {a : ℝ} (h : a ≠ 0) :

src/measure_theory/measure/measure_space.lean

@@ -91,7 +91,7 @@ noncomputable theory
 open set filter (hiding map) function measurable_space topological_space (second_countable_topology)
 open_locale classical topological_space big_operators filter ennreal nnreal
 
-variables {α β γ δ ι : Type*}
+variables {α β γ δ ι R R' : Type*}
 
 namespace measure_theory
 
@@ -622,9 +622,56 @@ instance [measurable_space α] : has_add (measure α) :=
 theorem add_apply {m : measurable_space α} (μ₁ μ₂ : measure α) (s : set α) :
   (μ₁ + μ₂) s = μ₁ s + μ₂ s := rfl
 
+section has_scalar
+variables [has_scalar R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞]
+variables [has_scalar R' ℝ≥0∞] [is_scalar_tower R' ℝ≥0∞ ℝ≥0∞]
+
+instance [measurable_space α] : has_scalar R (measure α) :=
+⟨λ c μ,
+  { to_outer_measure := c • μ.to_outer_measure,
+    m_Union := λ s hs hd, begin
+      rw ←smul_one_smul ℝ≥0∞ c (_ : outer_measure α),
+      dsimp,
+      simp_rw [measure_Union hd hs, ennreal.tsum_mul_left],
+    end,
+    trimmed := by rw [outer_measure.trim_smul, μ.trimmed] }⟩
+
+@[simp] theorem smul_to_outer_measure {m : measurable_space α} (c : R) (μ : measure α) :
+  (c • μ).to_outer_measure = c • μ.to_outer_measure :=
+rfl
+
+@[simp, norm_cast] theorem coe_smul {m : measurable_space α} (c : R) (μ : measure α) :
+  ⇑(c • μ) = c • μ :=
+rfl
+
+@[simp] theorem smul_apply {m : measurable_space α} (c : R) (μ : measure α) (s : set α) :
+  (c • μ) s = c • μ s :=
+rfl
+
+instance [smul_comm_class R R' ℝ≥0∞] [measurable_space α] :
+  smul_comm_class R R' (measure α) :=
+⟨λ _ _ _, ext $ λ _ _, smul_comm _ _ _⟩
+
+instance [has_scalar R R'] [is_scalar_tower R R' ℝ≥0∞] [measurable_space α] :
+  is_scalar_tower R R' (measure α) :=
+⟨λ _ _ _, ext $ λ _ _, smul_assoc _ _ _⟩
+
+instance [has_scalar Rᵐᵒᵖ ℝ≥0∞] [is_central_scalar R ℝ≥0∞] [measurable_space α] :
+  is_central_scalar R (measure α) :=
+⟨λ _ _, ext $ λ _ _, op_smul_eq_smul _ _⟩
+
+end has_scalar
+
+instance [monoid R] [mul_action R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞] [measurable_space α] :
+  mul_action R (measure α) :=
+injective.mul_action _ to_outer_measure_injective smul_to_outer_measure
+
+-- there is no `function.injective.add_comm_monoid_smul` so we do this in two steps
 instance add_comm_monoid [measurable_space α] : add_comm_monoid (measure α) :=
-to_outer_measure_injective.add_comm_monoid to_outer_measure zero_to_outer_measure
-  add_to_outer_measure
+{ ..(to_outer_measure_injective.add_monoid_smul to_outer_measure zero_to_outer_measure
+      add_to_outer_measure (λ _ _, smul_to_outer_measure _ _) : add_monoid (measure α)),
+  ..(to_outer_measure_injective.add_comm_semigroup to_outer_measure add_to_outer_measure :
+      add_comm_semigroup (measure α)) }
 
 /-- Coercion to function as an additive monoid homomorphism. -/
 def coe_add_hom {m : measurable_space α} : measure α →+ (set α → ℝ≥0∞) :=
@@ -638,31 +685,16 @@ theorem finset_sum_apply {m : measurable_space α} (I : finset ι) (μ : ι →
   (∑ i in I, μ i) s = ∑ i in I, μ i s :=
 by rw [coe_finset_sum, finset.sum_apply]
 
-instance [measurable_space α] : has_scalar ℝ≥0∞ (measure α) :=
-⟨λ c μ,
-  { to_outer_measure := c • μ.to_outer_measure,
-    m_Union := λ s hs hd, by simp [measure_Union, *, ennreal.tsum_mul_left],
-    trimmed := by rw [outer_measure.trim_smul, μ.trimmed] }⟩
-
-@[simp] theorem smul_to_outer_measure {m : measurable_space α} (c : ℝ≥0∞) (μ : measure α) :
-  (c • μ).to_outer_measure = c • μ.to_outer_measure :=
-rfl
-
-@[simp, norm_cast] theorem coe_smul {m : measurable_space α} (c : ℝ≥0∞) (μ : measure α) :
-  ⇑(c • μ) = c • μ :=
-rfl
-
-@[simp] theorem smul_apply {m : measurable_space α} (c : ℝ≥0∞) (μ : measure α) (s : set α) :
-  (c • μ) s = c * μ s :=
-rfl
-
-instance [measurable_space α] : module ℝ≥0∞ (measure α) :=
-injective.module ℝ≥0∞ ⟨to_outer_measure, zero_to_outer_measure, add_to_outer_measure⟩
+instance [monoid R] [distrib_mul_action R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞]
+  [measurable_space α] :
+  distrib_mul_action R (measure α) :=
+injective.distrib_mul_action ⟨to_outer_measure, zero_to_outer_measure, add_to_outer_measure⟩
   to_outer_measure_injective smul_to_outer_measure
 
-@[simp, norm_cast] theorem coe_nnreal_smul {m : measurable_space α} (c : ℝ≥0) (μ : measure α) :
-  ⇑(c • μ) = c • μ :=
-rfl
+instance [semiring R] [module R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞] [measurable_space α] :
+  module R (measure α) :=
+injective.module R ⟨to_outer_measure, zero_to_outer_measure, add_to_outer_measure⟩
+  to_outer_measure_injective smul_to_outer_measure
 
 @[simp] theorem coe_nnreal_smul_apply {m : measurable_space α} (c : ℝ≥0) (μ : measure α)
   (s : set α) :
@@ -1572,11 +1604,9 @@ instance [measurable_space α] : is_refl (measure α) (≪) := ⟨λ μ, absolut
 if hf : measurable f then absolutely_continuous.mk $ λ s hs, by simpa [hf, hs] using @h _
 else by simp only [map_of_not_measurable hf]
 
-protected lemma smul (h : μ ≪ ν) (c : ℝ≥0∞) : c • μ ≪ ν :=
-mk (λ s hs hνs, by simp only [h hνs, algebra.id.smul_eq_mul, coe_smul, pi.smul_apply, mul_zero])
-
-protected lemma coe_nnreal_smul (h : μ ≪ ν) (c : ℝ≥0) : c • μ ≪ ν :=
-h.smul c
+protected lemma smul [monoid R] [distrib_mul_action R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞]
+  (h : μ ≪ ν) (c : R) : c • μ ≪ ν :=
+mk (λ s hs hνs, by simp only [h hνs, smul_eq_mul, smul_apply, smul_zero])
 
 end absolutely_continuous
 
@@ -1779,8 +1809,10 @@ lemma mem_map_restrict_ae_iff {β} {s : set α} {t : set β} {f : α → β} (hs
   t ∈ filter.map f (μ.restrict s).ae ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0 :=
 by rw [mem_map, mem_ae_iff, measure.restrict_apply' hs]
 
-lemma ae_smul_measure {p : α → Prop} (h : ∀ᵐ x ∂μ, p x) (c : ℝ≥0∞) : ∀ᵐ x ∂(c • μ), p x :=
-ae_iff.2 $ by rw [smul_apply, ae_iff.1 h, mul_zero]
+lemma ae_smul_measure {p : α → Prop} [monoid R] [distrib_mul_action R ℝ≥0∞]
+  [is_scalar_tower R ℝ≥0∞ ℝ≥0∞] (h : ∀ᵐ x ∂μ, p x) (c : R) :
+  ∀ᵐ x ∂(c • μ), p x :=
+ae_iff.2 $ by rw [smul_apply, ae_iff.1 h, smul_zero]
 
 lemma ae_smul_measure_iff {p : α → Prop} {c : ℝ≥0∞} (hc : c ≠ 0) :
   (∀ᵐ x ∂(c • μ), p x) ↔ ∀ᵐ x ∂μ, p x :=
@@ -1965,6 +1997,16 @@ instance is_finite_measure_smul_nnreal [is_finite_measure μ] {r : ℝ≥0} :
   is_finite_measure (r • μ) :=
 { measure_univ_lt_top := ennreal.mul_lt_top ennreal.coe_ne_top (measure_ne_top _ _) }
 
+instance is_finite_measure_smul_of_nnreal_tower
+  {R} [has_scalar R ℝ≥0] [has_scalar R ℝ≥0∞] [is_scalar_tower R ℝ≥0 ℝ≥0∞]
+  [is_scalar_tower R ℝ≥0∞ ℝ≥0∞]
+  [is_finite_measure μ] {r : R} :
+  is_finite_measure (r • μ) :=
+begin
+  rw ←smul_one_smul ℝ≥0 r μ,
+  apply_instance,
+end
+
 lemma is_finite_measure_of_le (μ : measure α) [is_finite_measure μ] (h : ν ≤ μ) :
   is_finite_measure ν :=
 { measure_univ_lt_top := lt_of_le_of_lt (h set.univ measurable_set.univ) (measure_lt_top _ _) }
@@ -2490,7 +2532,8 @@ begin
   rcases μ.exists_is_open_measure_lt_top x with ⟨o, xo, o_open, μo⟩,
   refine ⟨o, o_open.mem_nhds xo, _⟩,
   apply ennreal.mul_lt_top _ μo.ne,
-  simp only [ennreal.coe_ne_top, ennreal.coe_of_nnreal_hom, ne.def, not_false_iff],
+  simp only [ring_hom.to_monoid_hom_eq_coe, ring_hom.coe_monoid_hom, ennreal.coe_ne_top,
+    ennreal.coe_of_nnreal_hom, ne.def, not_false_iff],
 end
 
 /-- A measure `μ` is finite on compacts if any compact set `K` satisfies `μ K < ∞`. -/
@@ -3124,7 +3167,8 @@ protected lemma Union [encodable ι] {s : ι → set α} (h : ∀ i, ae_measurab
 ⟨λ h i, h.mono_measure $ restrict_mono (subset_Union _ _) le_rfl, ae_measurable.Union⟩
 
 @[measurability]
-lemma smul_measure (h : ae_measurable f μ) (c : ℝ≥0∞) :
+lemma smul_measure [monoid R] [distrib_mul_action R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞]
+  (h : ae_measurable f μ) (c : R) :
   ae_measurable f (c • μ) :=
 ⟨h.mk f, h.measurable_mk, ae_smul_measure h.ae_eq_mk c⟩