feat(measure_theory/group/measure): a product of Haar measures is a Haar measure (#15120)

Author: sgouezel

src/measure_theory/constructions/prod.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn
 import measure_theory.measure.giry_monad
 import dynamics.ergodic.measure_preserving
 import measure_theory.integral.set_integral
+import measure_theory.measure.open_pos
 
 /-!
 # The product measure
@@ -366,6 +367,53 @@ begin
     ... = μ.prod ν (s ×ˢ t)     : measure_to_measurable _ }
 end
 
+instance {X Y : Type*} [topological_space X] [topological_space Y]
+  {m : measurable_space X} {μ : measure X} [is_open_pos_measure μ]
+  {m' : measurable_space Y} {ν : measure Y} [is_open_pos_measure ν] [sigma_finite ν] :
+  is_open_pos_measure (μ.prod ν) :=
+begin
+  constructor,
+  rintros U U_open ⟨⟨x, y⟩, hxy⟩,
+  rcases is_open_prod_iff.1 U_open x y hxy with ⟨u, v, u_open, v_open, xu, yv, huv⟩,
+  refine ne_of_gt (lt_of_lt_of_le _ (measure_mono huv)),
+  simp only [prod_prod, canonically_ordered_comm_semiring.mul_pos],
+  split,
+  { exact u_open.measure_pos μ ⟨x, xu⟩ },
+  { exact v_open.measure_pos ν ⟨y, yv⟩ }
+end
+
+instance {α β : Type*} {mα : measurable_space α} {mβ : measurable_space β}
+  (μ : measure α) (ν : measure β) [is_finite_measure μ] [is_finite_measure ν] :
+  is_finite_measure (μ.prod ν) :=
+begin
+  constructor,
+  rw [← univ_prod_univ, prod_prod],
+  exact mul_lt_top (measure_lt_top _ _).ne (measure_lt_top _ _).ne,
+end
+
+instance {α β : Type*} {mα : measurable_space α} {mβ : measurable_space β}
+  (μ : measure α) (ν : measure β) [is_probability_measure μ] [is_probability_measure ν] :
+  is_probability_measure (μ.prod ν) :=
+⟨by rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]⟩
+
+instance {α β : Type*} [topological_space α] [topological_space β]
+  {mα : measurable_space α} {mβ : measurable_space β} (μ : measure α) (ν : measure β)
+  [is_finite_measure_on_compacts μ] [is_finite_measure_on_compacts ν] [sigma_finite ν] :
+  is_finite_measure_on_compacts (μ.prod ν) :=
+begin
+  refine ⟨λ K hK, _⟩,
+  set L := (prod.fst '' K) ×ˢ (prod.snd '' K) with hL,
+  have : K ⊆ L,
+  { rintros ⟨x, y⟩ hxy,
+    simp only [prod_mk_mem_set_prod_eq, mem_image, prod.exists, exists_and_distrib_right,
+      exists_eq_right],
+    exact ⟨⟨y, hxy⟩, ⟨x, hxy⟩⟩ },
+  apply lt_of_le_of_lt (measure_mono this),
+  rw [hL, prod_prod],
+  exact mul_lt_top ((is_compact.measure_lt_top ((hK.image continuous_fst))).ne)
+                   ((is_compact.measure_lt_top ((hK.image continuous_snd))).ne)
+end
+
 lemma ae_measure_lt_top {s : set (α × β)} (hs : measurable_set s)
   (h2s : (μ.prod ν) s ≠ ∞) : ∀ᵐ x ∂μ, ν (prod.mk x ⁻¹' s) < ∞ :=
 by { simp_rw [prod_apply hs] at h2s, refine ae_lt_top (measurable_measure_prod_mk_left hs) h2s }
@@ -845,6 +893,17 @@ lemma integrable.integral_norm_prod_right [sigma_finite μ] ⦃f : α × β →
   (hf : integrable f (μ.prod ν)) : integrable (λ y, ∫ x, ∥f (x, y)∥ ∂μ) ν :=
 hf.swap.integral_norm_prod_left
 
+lemma integrable_prod_mul {f : α → ℝ} {g : β → ℝ} (hf : integrable f μ) (hg : integrable g ν) :
+  integrable (λ (z : α × β), f z.1 * g z.2) (μ.prod ν) :=
+begin
+  refine (integrable_prod_iff _).2 ⟨_, _⟩,
+  { apply ae_strongly_measurable.mul,
+    { exact (hf.1.mono' prod_fst_absolutely_continuous).comp_measurable measurable_fst },
+    { exact (hg.1.mono' prod_snd_absolutely_continuous).comp_measurable measurable_snd } },
+  { exact eventually_of_forall (λ x, hg.const_mul (f x)) },
+  { simpa only [norm_mul, integral_mul_left] using hf.norm.mul_const _ }
+end
+
 end
 
 variables [normed_space ℝ E] [complete_space E]
@@ -1015,4 +1074,21 @@ begin
   exact integral_prod f hf
 end
 
+lemma integral_prod_mul (f : α → ℝ) (g : β → ℝ) :
+  ∫ z, f z.1 * g z.2 ∂(μ.prod ν) = (∫ x, f x ∂μ) * (∫ y, g y ∂ν) :=
+begin
+  by_cases h : integrable (λ (z : α × β), f z.1 * g z.2) (μ.prod ν),
+  { rw integral_prod _ h,
+    simp_rw [integral_mul_left, integral_mul_right] },
+  have H : ¬(integrable f μ) ∨ ¬(integrable g ν),
+  { contrapose! h,
+    exact integrable_prod_mul h.1 h.2 },
+  cases H;
+  simp [integral_undef h, integral_undef H],
+end
+
+lemma set_integral_prod_mul (f : α → ℝ) (g : β → ℝ) (s : set α) (t : set β) :
+  ∫ z in s ×ˢ t, f z.1 * g z.2 ∂(μ.prod ν) = (∫ x in s, f x ∂μ) * (∫ y in t, g y ∂ν) :=
+by simp only [← measure.prod_restrict s t, integrable_on, integral_prod_mul]
+
 end measure_theory

src/measure_theory/function/jacobian.lean

@@ -1244,4 +1244,16 @@ begin
   refl
 end
 
+theorem integral_target_eq_integral_abs_det_fderiv_smul [complete_space F]
+  {f : local_homeomorph E E} (hf' : ∀ x ∈ f.source, has_fderiv_at f (f' x) x) (g : E → F) :
+  ∫ x in f.target, g x ∂μ = ∫ x in f.source, |(f' x).det| • g (f x) ∂μ :=
+begin
+  have : f '' f.source = f.target := local_equiv.image_source_eq_target f.to_local_equiv,
+  rw ← this,
+  apply integral_image_eq_integral_abs_det_fderiv_smul μ f.open_source.measurable_set _ f.inj_on,
+  assume x hx,
+  exact (hf' x hx).has_fderiv_within_at
+end
+
+
 end measure_theory

src/measure_theory/group/measure.lean

@@ -7,6 +7,7 @@ import dynamics.ergodic.measure_preserving
 import measure_theory.measure.regular
 import measure_theory.group.measurable_equiv
 import measure_theory.measure.open_pos
+import measure_theory.constructions.prod
 
 /-!
 # Measures on Groups
@@ -115,6 +116,36 @@ begin
   exact ⟨λ h, ⟨h⟩, λ h, h.1⟩
 end
 
+@[to_additive]
+instance [is_mul_left_invariant μ] [sigma_finite μ] {H : Type*} [has_mul H]
+  {mH : measurable_space H} {ν : measure H} [has_measurable_mul H]
+  [is_mul_left_invariant ν] [sigma_finite ν] :
+  is_mul_left_invariant (μ.prod ν) :=
+begin
+  constructor,
+  rintros ⟨g, h⟩,
+  change map (prod.map ((*) g) ((*) h)) (μ.prod ν) = μ.prod ν,
+  rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),
+    map_mul_left_eq_self μ g, map_mul_left_eq_self ν h],
+  { rw map_mul_left_eq_self μ g, apply_instance },
+  { rw map_mul_left_eq_self ν h, apply_instance },
+end
+
+@[to_additive]
+instance [is_mul_right_invariant μ] [sigma_finite μ] {H : Type*} [has_mul H]
+  {mH : measurable_space H} {ν : measure H} [has_measurable_mul H]
+  [is_mul_right_invariant ν] [sigma_finite ν] :
+  is_mul_right_invariant (μ.prod ν) :=
+begin
+  constructor,
+  rintros ⟨g, h⟩,
+  change map (prod.map (* g) (* h)) (μ.prod ν) = μ.prod ν,
+  rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h),
+    map_mul_right_eq_self μ g, map_mul_right_eq_self ν h],
+  { rw map_mul_right_eq_self μ g, apply_instance },
+  { rw map_mul_right_eq_self ν h, apply_instance },
+end
+
 end has_measurable_mul
 
 end mul
@@ -488,6 +519,14 @@ instance is_haar_measure.sigma_finite [sigma_compact_space G] : sigma_finite μ
   finite := λ n, is_compact.measure_lt_top $ is_compact_compact_covering G n,
   spanning := Union_compact_covering G }⟩⟩
 
+@[to_additive]
+instance {G : Type*} [group G] [topological_space G] {mG : measurable_space G}
+  {H : Type*} [group H] [topological_space H] {mH : measurable_space H}
+  (μ : measure G) (ν : measure H) [is_haar_measure μ] [is_haar_measure ν]
+  [sigma_finite μ] [sigma_finite ν]
+  [has_measurable_mul G] [has_measurable_mul H] :
+  is_haar_measure (μ.prod ν) := {}
+
 open_locale topological_space
 open filter
 

src/measure_theory/integral/interval_integral.lean

@@ -248,6 +248,20 @@ lemma interval_integrable_iff_integrable_Icc_of_le {E : Type*} [normed_group E]
   interval_integrable f μ a b ↔ integrable_on f (Icc a b) μ :=
 by rw [interval_integrable_iff_integrable_Ioc_of_le hab, integrable_on_Icc_iff_integrable_on_Ioc]
 
+lemma integrable_on_Ici_iff_integrable_on_Ioi'
+  {E : Type*} [normed_group E] {f : ℝ → E} (ha : μ {a} ≠ ∞) :
+  integrable_on f (Ici a) μ ↔ integrable_on f (Ioi a) μ :=
+begin
+  have : Ici a = Icc a a ∪ Ioi a := (Icc_union_Ioi_eq_Ici le_rfl).symm,
+  rw [this, integrable_on_union],
+  simp [ha.lt_top]
+end
+
+lemma integrable_on_Ici_iff_integrable_on_Ioi
+  {E : Type*} [normed_group E] [has_no_atoms μ] {f : ℝ → E} :
+  integrable_on f (Ici a) μ ↔ integrable_on f (Ioi a) μ :=
+integrable_on_Ici_iff_integrable_on_Ioi' (by simp)
+
 /-- If a function is integrable with respect to a given measure `μ` then it is interval integrable
   with respect to `μ` on `interval a b`. -/
 lemma measure_theory.integrable.interval_integrable (hf : integrable f μ) :

src/measure_theory/measure/haar.lean

@@ -728,5 +728,13 @@ calc μ (s⁻¹) = measure.map (has_inv.inv) μ s :
   ((homeomorph.inv G).to_measurable_equiv.map_apply s).symm
 ... = μ s : by rw map_haar_inv
 
+@[to_additive]
+lemma measure_preserving_inv
+  {G : Type*} [comm_group G] [topological_space G] [topological_group G] [t2_space G]
+  [measurable_space G] [borel_space G] [locally_compact_space G] [second_countable_topology G]
+  (μ : measure G) [is_haar_measure μ] :
+  measure_preserving has_inv.inv μ μ :=
+⟨measurable_inv, map_haar_inv μ⟩
+
 end measure
 end measure_theory