feat(measure_theory/group/arithmetic): add more to_additive attribute…

…s for actions (#9032)

Introduce additivised versions of some more smul classes and corresponding instances and lemmas for different types of (measurable) additive actions.

src/algebra/add_torsor.lean

@@ -335,11 +335,6 @@ instance [T : ∀ i, add_torsor (fg i) (fp i)] : add_torsor (Π i, fg i) (Π i,
   vsub_vadd' := λ p₁ p₂, funext $ λ i, vsub_vadd (p₁ i) (p₂ i),
   vadd_vsub' := λ g p, funext $ λ i, vadd_vsub (g i) (p i) }
 
-/-- Addition in a product of `add_torsor`s. -/
-@[simp] lemma vadd_apply [T : ∀ i, add_torsor (fg i) (fp i)] (x : Π i, fg i) (y : Π i, fp i)
-  {i : I} : (x +ᵥ y) i = x i +ᵥ y i
-:= rfl
-
 end pi
 
 namespace equiv

src/algebra/module/pi.lean

@@ -19,18 +19,22 @@ variable {I : Type u}     -- The indexing type
 variable {f : I → Type v} -- The family of types already equipped with instances
 variables (x y : Π i, f i) (i : I)
 
+@[to_additive pi.has_vadd]
 instance has_scalar {α : Type*} [Π i, has_scalar α $ f i] :
   has_scalar α (Π i : I, f i) :=
 ⟨λ s x, λ i, s • (x i)⟩
 
+@[to_additive]
 lemma smul_def {α : Type*} [Π i, has_scalar α $ f i] (s : α) : s • x = λ i, s • x i := rfl
-@[simp] lemma smul_apply {α : Type*} [Π i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl
+@[simp, to_additive]
+lemma smul_apply {α : Type*} [Π i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl
 
+@[to_additive pi.has_vadd']
 instance has_scalar' {g : I → Type*} [Π i, has_scalar (f i) (g i)] :
   has_scalar (Π i, f i) (Π i : I, g i) :=
 ⟨λ s x, λ i, (s i) • (x i)⟩
 
-@[simp]
+@[simp, to_additive]
 lemma smul_apply' {g : I → Type*} [∀ i, has_scalar (f i) (g i)] (s : Π i, f i) (x : Π i, g i) :
   (s • x) i = s i • x i :=
 rfl
@@ -54,23 +58,27 @@ instance is_scalar_tower'' {g : I → Type*} {h : I → Type*}
   [Π i, is_scalar_tower (f i) (g i) (h i)] : is_scalar_tower (Π i, f i) (Π i, g i) (Π i, h i) :=
 ⟨λ x y z, funext $ λ i, smul_assoc (x i) (y i) (z i)⟩
 
+@[to_additive]
 instance smul_comm_class {α β : Type*}
   [Π i, has_scalar α $ f i] [Π i, has_scalar β $ f i] [∀ i, smul_comm_class α β (f i)] :
   smul_comm_class α β (Π i : I, f i) :=
 ⟨λ x y z, funext $ λ i, smul_comm x y (z i)⟩
 
+@[to_additive]
 instance smul_comm_class' {g : I → Type*} {α : Type*}
   [Π i, has_scalar α $ g i] [Π i, has_scalar (f i) (g i)] [∀ i, smul_comm_class α (f i) (g i)] :
   smul_comm_class α (Π i : I, f i) (Π i : I, g i) :=
 ⟨λ x y z, funext $ λ i, smul_comm x (y i) (z i)⟩
 
+@[to_additive]
 instance smul_comm_class'' {g : I → Type*} {h : I → Type*}
   [Π i, has_scalar (g i) (h i)] [Π i, has_scalar (f i) (h i)]
   [∀ i, smul_comm_class (f i) (g i) (h i)] : smul_comm_class (Π i, f i) (Π i, g i) (Π i, h i) :=
 ⟨λ x y z, funext $ λ i, smul_comm (x i) (y i) (z i)⟩
 
 /-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is
 not an instance as `i` cannot be inferred. -/
+@[to_additive pi.has_faithful_vadd_at]
 lemma has_faithful_scalar_at {α : Type*}
   [Π i, has_scalar α $ f i] [Π i, nonempty (f i)] (i : I) [has_faithful_scalar α (f i)] :
   has_faithful_scalar α (Π i, f i) :=
@@ -80,6 +88,7 @@ lemma has_faithful_scalar_at {α : Type*}
   simpa using this,
 end⟩
 
+@[to_additive pi.has_faithful_vadd]
 instance has_faithful_scalar {α : Type*}
   [nonempty I] [Π i, has_scalar α $ f i] [Π i, nonempty (f i)] [Π i, has_faithful_scalar α (f i)] :
   has_faithful_scalar α (Π i, f i) :=
@@ -99,12 +108,14 @@ instance smul_with_zero' {g : I → Type*} [Π i, has_zero (g i)]
   zero_smul := λ _, funext $ λ _, zero_smul _ _,
   ..pi.has_scalar' }
 
+@[to_additive]
 instance mul_action (α) {m : monoid α} [Π i, mul_action α $ f i] :
   @mul_action α (Π i : I, f i) m :=
 { smul := (•),
   mul_smul := λ r s f, funext $ λ i, mul_smul _ _ _,
   one_smul := λ f, funext $ λ i, one_smul α _ }
 
+@[to_additive]
 instance mul_action' {g : I → Type*} {m : Π i, monoid (f i)} [Π i, mul_action (f i) (g i)] :
   @mul_action (Π i, f i) (Π i : I, g i) (@pi.monoid I f m) :=
 { smul := (•),

src/measure_theory/group/arithmetic.lean

@@ -388,27 +388,46 @@ instance has_measurable_div₂_of_mul_inv (G : Type*) [measurable_space G]
   has_measurable_div₂ G :=
 ⟨by { simp only [div_eq_mul_inv], exact measurable_fst.mul measurable_snd.inv }⟩
 
+/-- We say that the action of `M` on `α` `has_measurable_vadd` if for each `c` the map `x ↦ c +ᵥ x`
+is a measurable function and for each `x` the map `c ↦ c +ᵥ x` is a measurable function. -/
+class has_measurable_vadd (M α : Type*) [has_vadd M α] [measurable_space M] [measurable_space α] :
+  Prop :=
+(measurable_const_vadd : ∀ c : M, measurable ((+ᵥ) c : α → α))
+(measurable_vadd_const : ∀ x : α, measurable (λ c : M, c +ᵥ x))
+
 /-- We say that the action of `M` on `α` `has_measurable_smul` if for each `c` the map `x ↦ c • x`
 is a measurable function and for each `x` the map `c ↦ c • x` is a measurable function. -/
+@[to_additive]
 class has_measurable_smul (M α : Type*) [has_scalar M α] [measurable_space M] [measurable_space α] :
   Prop :=
 (measurable_const_smul : ∀ c : M, measurable ((•) c : α → α))
 (measurable_smul_const : ∀ x : α, measurable (λ c : M, c • x))
 
-/-- We say that the action of `M` on `α` `has_measurable_smul` if the map
+/-- We say that the action of `M` on `α` `has_measurable_vadd₂` if the map
+`(c, x) ↦ c +ᵥ x` is a measurable function. -/
+class has_measurable_vadd₂ (M α : Type*) [has_vadd M α] [measurable_space M]
+  [measurable_space α] : Prop :=
+(measurable_vadd : measurable (function.uncurry (+ᵥ) : M × α → α))
+
+/-- We say that the action of `M` on `α` `has_measurable_smul₂` if the map
 `(c, x) ↦ c • x` is a measurable function. -/
+@[to_additive has_measurable_vadd₂]
 class has_measurable_smul₂ (M α : Type*) [has_scalar M α] [measurable_space M]
   [measurable_space α] : Prop :=
 (measurable_smul : measurable (function.uncurry (•) : M × α → α))
 
 export has_measurable_smul (measurable_const_smul measurable_smul_const)
   has_measurable_smul₂ (measurable_smul)
+export has_measurable_vadd (measurable_const_vadd measurable_vadd_const)
+  has_measurable_vadd₂ (measurable_vadd)
 
+@[to_additive]
 instance has_measurable_smul_of_mul (M : Type*) [monoid M] [measurable_space M]
   [has_measurable_mul M] :
   has_measurable_smul M M :=
 ⟨measurable_id.const_mul, measurable_id.mul_const⟩
 
+@[to_additive]
 instance has_measurable_smul₂_of_mul (M : Type*) [monoid M] [measurable_space M]
   [has_measurable_mul₂ M] :
   has_measurable_smul₂ M M :=
@@ -419,50 +438,50 @@ section smul
 variables {M β α : Type*} [measurable_space M] [measurable_space β] [has_scalar M β]
   [measurable_space α]
 
-@[measurability]
+@[measurability, to_additive]
 lemma measurable.smul [has_measurable_smul₂ M β]
   {f : α → M} {g : α → β} (hf : measurable f) (hg : measurable g) :
   measurable (λ x, f x • g x) :=
 measurable_smul.comp (hf.prod_mk hg)
 
-@[measurability]
+@[measurability, to_additive]
 lemma ae_measurable.smul [has_measurable_smul₂ M β]
   {f : α → M} {g : α → β} {μ : measure α} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
   ae_measurable (λ x, f x • g x) μ :=
 has_measurable_smul₂.measurable_smul.comp_ae_measurable (hf.prod_mk hg)
 
-@[priority 100]
+@[priority 100, to_additive]
 instance has_measurable_smul₂.to_has_measurable_smul [has_measurable_smul₂ M β] :
   has_measurable_smul M β :=
 ⟨λ c, measurable_const.smul measurable_id, λ y, measurable_id.smul measurable_const⟩
 
 variables [has_measurable_smul M β] {μ : measure α}
 
-@[measurability]
+@[measurability, to_additive]
 lemma measurable.smul_const {f : α → M} (hf : measurable f) (y : β) : measurable (λ x, f x • y) :=
 (has_measurable_smul.measurable_smul_const y).comp hf
 
-@[measurability]
+@[measurability, to_additive]
 lemma ae_measurable.smul_const {f : α → M} (hf : ae_measurable f μ) (y : β) :
   ae_measurable (λ x, f x • y) μ :=
 (has_measurable_smul.measurable_smul_const y).comp_ae_measurable hf
 
-@[measurability]
+@[measurability, to_additive]
 lemma measurable.const_smul' {f : α → β} (hf : measurable f) (c : M) :
   measurable (λ x, c • f x) :=
 (has_measurable_smul.measurable_const_smul c).comp hf
 
-@[measurability]
+@[measurability, to_additive]
 lemma measurable.const_smul {f : α → β} (hf : measurable f) (c : M) :
   measurable (c • f) :=
 hf.const_smul' c
 
-@[measurability]
+@[measurability, to_additive]
 lemma ae_measurable.const_smul' {f : α → β} (hf : ae_measurable f μ) (c : M) :
   ae_measurable (λ x, c • f x) μ :=
 (has_measurable_smul.measurable_const_smul c).comp_ae_measurable hf
 
-@[measurability]
+@[measurability, to_additive]
 lemma ae_measurable.const_smul {f : α → β} (hf : ae_measurable f μ) (c : M) :
   ae_measurable (c • f) μ :=
 hf.const_smul' c
@@ -477,25 +496,31 @@ variables {M β α : Type*} [measurable_space M] [measurable_space β] [monoid M
 variables {G : Type*} [group G] [measurable_space G] [mul_action G β]
   [has_measurable_smul G β]
 
+@[to_additive]
 lemma measurable_const_smul_iff (c : G) :
   measurable (λ x, c • f x) ↔ measurable f :=
 ⟨λ h, by simpa only [inv_smul_smul] using h.const_smul' c⁻¹, λ h, h.const_smul c⟩
 
+@[to_additive]
 lemma ae_measurable_const_smul_iff (c : G) :
   ae_measurable (λ x, c • f x) μ ↔ ae_measurable f μ :=
 ⟨λ h, by simpa only [inv_smul_smul] using h.const_smul' c⁻¹, λ h, h.const_smul c⟩
 
+@[to_additive]
 instance : measurable_space (units M) := measurable_space.comap (coe : units M → M) ‹_›
 
+@[to_additive]
 instance units.has_measurable_smul : has_measurable_smul (units M) β :=
 { measurable_const_smul := λ c, (measurable_const_smul (c : M) : _),
   measurable_smul_const := λ x,
     (measurable_smul_const x : measurable (λ c : M, c • x)).comp measurable_space.le_map_comap, }
 
+@[to_additive]
 lemma is_unit.measurable_const_smul_iff {c : M} (hc : is_unit c) :
   measurable (λ x, c • f x) ↔ measurable f :=
 let ⟨u, hu⟩ := hc in hu ▸ measurable_const_smul_iff u
 
+@[to_additive]
 lemma is_unit.ae_measurable_const_smul_iff {c : M} (hc : is_unit c) :
   ae_measurable (λ x, c • f x) μ ↔ ae_measurable f μ :=
 let ⟨u, hu⟩ := hc in hu ▸ ae_measurable_const_smul_iff u

src/measure_theory/measure/haar.lean

@@ -506,11 +506,25 @@ scaled so that `add_haar_measure K₀ K₀ = 1`."]
 def haar_measure (K₀ : positive_compacts G) : measure G :=
 ((haar_content K₀).outer_measure K₀.1)⁻¹ • (haar_content K₀).measure
 
+-- Unfortunately we have to manually give the additive version here
+lemma add_haar_measure_apply {G : Type*} [add_group G] [topological_space G] [t2_space G]
+  [topological_add_group G] [measurable_space G] [borel_space G] {K₀ : positive_compacts G}
+  {s : set G} (hs : measurable_set s) : add_haar_measure K₀ s =
+  (add_haar_content K₀).outer_measure s / (add_haar_content K₀).outer_measure K₀.1 :=
+begin
+  delta add_haar_measure,
+  simp only [hs, div_eq_mul_inv, mul_comm, content.measure_apply, algebra.id.smul_eq_mul,
+    coe_smul, pi.smul_apply],
+end
+
 @[to_additive]
 lemma haar_measure_apply {K₀ : positive_compacts G} {s : set G} (hs : measurable_set s) :
   haar_measure K₀ s = (haar_content K₀).outer_measure s / (haar_content K₀).outer_measure K₀.1 :=
-by simp only [haar_measure, hs, div_eq_mul_inv, mul_comm, content.measure_apply,
-      algebra.id.smul_eq_mul, pi.smul_apply, measure.coe_smul]
+begin
+  delta haar_measure,
+  simp only [hs, div_eq_mul_inv, mul_comm, content.measure_apply, algebra.id.smul_eq_mul,
+    coe_smul, pi.smul_apply],
+end
 
 @[to_additive]
 lemma is_mul_left_invariant_haar_measure (K₀ : positive_compacts G) :