feat(measure_theory/group, measure_theory/bochner_integration): left translate of an integral (#6936)

Translating a function on a topological group by left- (right-) multiplication by a constant does not change its integral with respect to a left- (right-) invariant measure.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

Author: 3 people

src/measure_theory/bochner_integration.lean

@@ -6,6 +6,7 @@ Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel
 import measure_theory.simple_func_dense
 import analysis.normed_space.bounded_linear_maps
 import measure_theory.l1_space
+import measure_theory.group
 import topology.sequences
 
 /-!
@@ -1573,6 +1574,74 @@ calc ∫ x, f x ∂(measure.dirac a) = ∫ x, f a ∂(measure.dirac a) :
 
 end properties
 
+section group
+
+variables {G : Type*} [measurable_space G] [topological_space G] [group G] [has_continuous_mul G]
+  [borel_space G]
+variables {μ : measure G}
+
+open measure
+
+/-- Translating a function by left-multiplication does not change its integral with respect to a
+left-invariant measure. -/
+@[to_additive]
+lemma integral_mul_left_eq_self (hμ : is_mul_left_invariant μ) {f : G → E} (g : G) :
+  ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ :=
+begin
+  have hgμ : measure.map (has_mul.mul g) μ = μ,
+  { rw ← map_mul_left_eq_self at hμ,
+    exact hμ g },
+  have h_mul : closed_embedding (λ x, g * x) := (homeomorph.mul_left g).closed_embedding,
+  rw [← integral_map_of_closed_embedding h_mul, hgμ]
+end
+
+/-- Translating a function by right-multiplication does not change its integral with respect to a
+right-invariant measure. -/
+@[to_additive]
+lemma integral_mul_right_eq_self (hμ : is_mul_right_invariant μ) {f : G → E} (g : G) :
+  ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ :=
+begin
+  have hgμ : measure.map (λ x, x * g) μ = μ,
+  { rw ← map_mul_right_eq_self at hμ,
+    exact hμ g },
+  have h_mul : closed_embedding (λ x, x * g) := (homeomorph.mul_right g).closed_embedding,
+  rw [← integral_map_of_closed_embedding h_mul, hgμ]
+end
+
+/-- If some left-translate of a function negates it, then the integral of the function with respect
+to a left-invariant measure is 0. -/
+@[to_additive]
+lemma integral_zero_of_mul_left_eq_neg (hμ : is_mul_left_invariant μ) {f : G → E} {g : G}
+  (hf' : ∀ x, f (g * x) = - f x) :
+  ∫ x, f x ∂μ = 0 :=
+begin
+  refine eq_zero_of_eq_neg ℝ (eq.symm _),
+  have : ∫ x, f (g * x) ∂μ = ∫ x, - f x ∂μ,
+  { congr,
+    ext x,
+    exact hf' x },
+  convert integral_mul_left_eq_self hμ g using 1,
+  rw [this, integral_neg]
+end
+
+/-- If some right-translate of a function negates it, then the integral of the function with respect
+to a right-invariant measure is 0. -/
+@[to_additive]
+lemma integral_zero_of_mul_right_eq_neg (hμ : is_mul_right_invariant μ) {f : G → E} {g : G}
+  (hf' : ∀ x, f (x * g) = - f x) :
+  ∫ x, f x ∂μ = 0 :=
+begin
+  refine eq_zero_of_eq_neg ℝ (eq.symm _),
+  have : ∫ x, f (x * g) ∂μ = ∫ x, - f x ∂μ,
+  { congr,
+    ext x,
+    exact hf' x },
+  convert integral_mul_right_eq_self hμ g using 1,
+  rw [this, integral_neg]
+end
+
+end group
+
 mk_simp_attribute integral_simps "Simp set for integral rules."
 
 attribute [integral_simps] integral_neg integral_smul L1.integral_add L1.integral_sub

src/measure_theory/group.lean

@@ -212,4 +212,37 @@ end
 
 end group
 
+section integration
+
+variables [group G] [has_continuous_mul G]
+open measure
+
+/-- Translating a function by left-multiplication does not change its `lintegral` with respect to
+a left-invariant measure. -/
+@[to_additive]
+lemma lintegral_mul_left_eq_self (hμ : is_mul_left_invariant μ) (f : G → ℝ≥0∞) (g : G) :
+  ∫⁻ x, f (g * x) ∂μ = ∫⁻ x, f x ∂μ :=
+begin
+  have : measure.map (has_mul.mul g) μ = μ,
+  { rw ← map_mul_left_eq_self at hμ,
+    exact hμ g },
+  convert (lintegral_map_equiv f (homeomorph.mul_left g).to_measurable_equiv).symm,
+  simp [this]
+end
+
+/-- Translating a function by right-multiplication does not change its `lintegral` with respect to
+a right-invariant measure. -/
+@[to_additive]
+lemma lintegral_mul_right_eq_self (hμ : is_mul_right_invariant μ) (f : G → ℝ≥0∞) (g : G) :
+  ∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ :=
+begin
+  have : measure.map (homeomorph.mul_right g) μ = μ,
+  { rw ← map_mul_right_eq_self at hμ,
+    exact hμ g },
+  convert (lintegral_map_equiv f (homeomorph.mul_right g).to_measurable_equiv).symm,
+  simp [this]
+end
+
+end integration
+
 end measure_theory

src/measure_theory/integration.lean

@@ -699,6 +699,27 @@ lemma lintegral_map {β} [measurable_space β] {μ' : measure β} (f : α →ₛ
 lintegral_eq_of_measure_preimage $ λ y,
 by { simp only [preimage, eq], exact (h (g ⁻¹' {y}) (g.measurable_set_preimage _)).symm }
 
+/-- The `lintegral` of simple functions transforms appropriately under a measurable equivalence.
+(Compare `lintegral_map`, which applies to a broader class of transformations of the domain, but
+requires measurability of the function being integrated.) -/
+lemma lintegral_map_equiv {β} [measurable_space β] (g : β →ₛ ℝ≥0∞) (m : α ≃ᵐ β) :
+  (g.comp m m.measurable).lintegral μ = g.lintegral (measure.map m μ) :=
+begin
+  simp [simple_func.lintegral],
+  have : (g.comp m m.measurable).range = g.range,
+  { refine le_antisymm _ _,
+    { exact g.range_comp_subset_range m.measurable },
+    convert (g.comp m m.measurable).range_comp_subset_range m.symm.measurable,
+    apply simple_func.ext,
+    intros a,
+    exact congr_arg g (congr_fun m.self_comp_symm.symm a) },
+  rw this,
+  congr' 1,
+  funext,
+  rw [m.map_apply (g ⁻¹' {x})],
+  refl,
+end
+
 end measure
 
 section fin_meas_supp
@@ -1650,6 +1671,36 @@ lemma set_lintegral_map [measurable_space β] {f : β → ℝ≥0∞} {g : α 
   ∫⁻ y in s, f y ∂(map g μ) = ∫⁻ x in g ⁻¹' s, f (g x) ∂μ :=
 by rw [restrict_map hg hs, lintegral_map hf hg]
 
+/-- The `lintegral` transforms appropriately under a measurable equivalence `g : α ≃ᵐ β`.
+(Compare `lintegral_map`, which applies to a wider class of functions `g : α → β`, but requires
+measurability of the function being integrated.) -/
+lemma lintegral_map_equiv [measurable_space β] (f : β → ℝ≥0∞) (g : α ≃ᵐ β) :
+  ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ :=
+begin
+  refine le_antisymm _ _,
+  { refine supr_le_supr2 _,
+    intros f₀,
+    use f₀.comp g g.measurable,
+    refine supr_le_supr2 _,
+    intros hf₀,
+    use λ x, hf₀ (g x),
+    exact (lintegral_map_equiv f₀ g).symm.le },
+  { refine supr_le_supr2 _,
+    intros f₀,
+    use f₀.comp g.symm g.symm.measurable,
+    refine supr_le_supr2 _,
+    intros hf₀,
+    have : (λ a, (f₀.comp (g.symm) g.symm.measurable) a) ≤ λ (a : β), f a,
+    { convert λ x, hf₀ (g.symm x),
+      funext,
+      simp [congr_arg f (congr_fun g.self_comp_symm a)] },
+    use this,
+    convert (lintegral_map_equiv (f₀.comp g.symm g.symm.measurable) g).le,
+    apply simple_func.ext,
+    intros a,
+    convert congr_arg f₀ (congr_fun g.symm_comp_self a).symm using 1 }
+end
+
 lemma lintegral_dirac' (a : α) {f : α → ℝ≥0∞} (hf : measurable f) :
   ∫⁻ a, f a ∂(dirac a) = f a :=
 by simp [lintegral_congr_ae (ae_eq_dirac' hf)]