feat: add mul_iff right and mul_iff_left for (AE)(Strongly)Measurable (#12711)

Add the lemma that says that if `f` is measurable, then `f+g` is measurable iff `g` is measurable. Then add the same but with `g+f`, and the same lemmas about AEMeasurable, StronglyMeasurable and AEStronglyMeasurable.



Co-authored-by: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Author: LorenzoLuccioli

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -452,6 +452,17 @@ protected theorem div [Div β] [ContinuousDiv β] (hf : StronglyMeasurable f)
 #align measure_theory.strongly_measurable.div MeasureTheory.StronglyMeasurable.div
 #align measure_theory.strongly_measurable.sub MeasureTheory.StronglyMeasurable.sub
 
+@[to_additive]
+theorem mul_iff_right [CommGroup β] [TopologicalGroup β] (hf : StronglyMeasurable f) :
+    StronglyMeasurable (f * g) ↔ StronglyMeasurable g :=
+  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
+    fun h ↦ hf.mul h⟩
+
+@[to_additive]
+theorem mul_iff_left [CommGroup β] [TopologicalGroup β] (hf : StronglyMeasurable f) :
+    StronglyMeasurable (g * f) ↔ StronglyMeasurable g :=
+  mul_comm g f ▸ mul_iff_right hf
+
 @[to_additive (attr := aesop safe 20 apply (rule_sets := [Measurable]))]
 protected theorem smul {𝕜} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜}
     {g : α → β} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
@@ -1355,6 +1366,17 @@ protected theorem div [Group β] [TopologicalGroup β] (hf : AEStronglyMeasurabl
 #align measure_theory.ae_strongly_measurable.div MeasureTheory.AEStronglyMeasurable.div
 #align measure_theory.ae_strongly_measurable.sub MeasureTheory.AEStronglyMeasurable.sub
 
+@[to_additive]
+theorem mul_iff_right [CommGroup β] [TopologicalGroup β] (hf : AEStronglyMeasurable f μ) :
+    AEStronglyMeasurable (f * g) μ ↔ AEStronglyMeasurable g μ :=
+  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
+    fun h ↦ hf.mul h⟩
+
+@[to_additive]
+theorem mul_iff_left [CommGroup β] [TopologicalGroup β] (hf : AEStronglyMeasurable f μ) :
+    AEStronglyMeasurable (g * f) μ ↔ AEStronglyMeasurable g μ :=
+  mul_comm g f ▸ AEStronglyMeasurable.mul_iff_right hf
+
 @[to_additive (attr := aesop safe 20 apply (rule_sets := [Measurable]))]
 protected theorem smul {𝕜} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜}
     {g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :

Mathlib/MeasureTheory/Group/Arithmetic.lean

@@ -520,6 +520,32 @@ theorem measurableEmbedding_inv [InvolutiveInv α] [MeasurableInv α] :
 
 end Inv
 
+@[to_additive]
+theorem Measurable.mul_iff_right {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G]
+    [MeasurableMul₂ G] [MeasurableInv G] {f g : α → G} (hf : Measurable f) :
+    Measurable (f * g) ↔ Measurable g :=
+  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
+    fun h ↦ hf.mul h⟩
+
+@[to_additive]
+theorem AEMeasurable.mul_iff_right {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G]
+    [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure α} {f g : α → G} (hf : AEMeasurable f μ) :
+    AEMeasurable (f * g) μ ↔ AEMeasurable g μ :=
+  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
+    fun h ↦ hf.mul h⟩
+
+@[to_additive]
+theorem Measurable.mul_iff_left {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G]
+    [MeasurableMul₂ G] [MeasurableInv G] {f g : α → G} (hf : Measurable f) :
+    Measurable (g * f) ↔ Measurable g :=
+  mul_comm g f ▸ Measurable.mul_iff_right hf
+
+@[to_additive]
+theorem AEMeasurable.mul_iff_left {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G]
+    [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure α} {f g : α → G} (hf : AEMeasurable f μ) :
+    AEMeasurable (g * f) μ ↔ AEMeasurable g μ :=
+  mul_comm g f ▸ AEMeasurable.mul_iff_right hf
+
 /-- `DivInvMonoid.Pow` is measurable. -/
 instance DivInvMonoid.measurableZPow (G : Type u) [DivInvMonoid G] [MeasurableSpace G]
     [MeasurableMul₂ G] [MeasurableInv G] : MeasurablePow G ℤ :=