feat: more facts on measures in topological groups (#8286)

Prerequisites for #8198

Mathlib/MeasureTheory/Group/LIntegral.lean

@@ -68,9 +68,8 @@ variable [TopologicalSpace G] [Group G] [TopologicalGroup G] [BorelSpace G] [IsM
 @[to_additive
       "For nonzero regular left invariant measures, the integral of a continuous nonnegative
       function `f` is 0 iff `f` is 0."]
-theorem lintegral_eq_zero_of_isMulLeftInvariant [Regular μ] (hμ : μ ≠ 0) {f : G → ℝ≥0∞}
+theorem lintegral_eq_zero_of_isMulLeftInvariant [Regular μ] [NeZero μ] {f : G → ℝ≥0∞}
     (hf : Continuous f) : ∫⁻ x, f x ∂μ = 0 ↔ f = 0 := by
-  haveI := isOpenPosMeasure_of_mulLeftInvariant_of_regular hμ
   rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]
 #align measure_theory.lintegral_eq_zero_of_is_mul_left_invariant MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant
 #align measure_theory.lintegral_eq_zero_of_is_add_left_invariant MeasureTheory.lintegral_eq_zero_of_isAddLeftInvariant

Mathlib/MeasureTheory/Group/Measure.lean

@@ -412,6 +412,9 @@ section Inv
 
 variable [Inv G]
 
+@[to_additive]
+theorem inv_def (μ : Measure G) : μ.inv = Measure.map inv μ := rfl
+
 @[to_additive (attr := simp)]
 theorem inv_eq_self (μ : Measure G) [IsInvInvariant μ] : μ.inv = μ :=
   IsInvInvariant.inv_eq_self
@@ -546,21 +549,37 @@ section TopologicalGroup
 variable [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G]
 
 @[to_additive]
-instance Measure.Regular.inv [ContinuousInv G] [T2Space G] [Regular μ] : Regular μ.inv :=
+instance Measure.IsFiniteMeasureOnCompacts.inv [ContinuousInv G] [IsFiniteMeasureOnCompacts μ] :
+    IsFiniteMeasureOnCompacts μ.inv :=
+  IsFiniteMeasureOnCompacts.map μ (Homeomorph.inv G)
+
+@[to_additive]
+instance Measure.IsOpenPosMeasure.inv [ContinuousInv G] [IsOpenPosMeasure μ] :
+    IsOpenPosMeasure μ.inv :=
+  (Homeomorph.inv G).continuous.isOpenPosMeasure_map (Homeomorph.inv G).surjective
+
+@[to_additive]
+instance Measure.Regular.inv [ContinuousInv G] [Regular μ] : Regular μ.inv :=
   Regular.map (Homeomorph.inv G)
 #align measure_theory.measure.regular.inv MeasureTheory.Measure.Regular.inv
 #align measure_theory.measure.regular.neg MeasureTheory.Measure.Regular.neg
 
+@[to_additive]
+instance Measure.InnerRegular.inv [ContinuousInv G] [InnerRegular μ] : InnerRegular μ.inv :=
+  InnerRegular.map (Homeomorph.inv G)
+
 variable [TopologicalGroup G]
 
 @[to_additive]
-theorem regular_inv_iff [T2Space G] : μ.inv.Regular ↔ μ.Regular := by
-  constructor
-  · intro h; rw [← μ.inv_inv]; exact Measure.Regular.inv
-  · intro h; exact Measure.Regular.inv
+theorem regular_inv_iff : μ.inv.Regular ↔ μ.Regular :=
+  Regular.map_iff (Homeomorph.inv G)
 #align measure_theory.regular_inv_iff MeasureTheory.regular_inv_iff
 #align measure_theory.regular_neg_iff MeasureTheory.regular_neg_iff
 
+@[to_additive]
+theorem innerRegular_inv_iff : μ.inv.InnerRegular ↔ μ.InnerRegular :=
+  InnerRegular.map_iff (Homeomorph.inv G)
+
 variable [IsMulLeftInvariant μ]
 
 /-- If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to
@@ -585,19 +604,27 @@ theorem isOpenPosMeasure_of_mulLeftInvariant_of_compact (K : Set G) (hK : IsComp
 
 /-- A nonzero left-invariant regular measure gives positive mass to any open set. -/
 @[to_additive "A nonzero left-invariant regular measure gives positive mass to any open set."]
-theorem isOpenPosMeasure_of_mulLeftInvariant_of_regular [Regular μ] (h₀ : μ ≠ 0) :
+instance (priority := 80) isOpenPosMeasure_of_mulLeftInvariant_of_regular [Regular μ] [NeZero μ] :
     IsOpenPosMeasure μ :=
-  let ⟨K, hK, h2K⟩ := Regular.exists_compact_not_null.mpr h₀
+  let ⟨K, hK, h2K⟩ := Regular.exists_compact_not_null.mpr (NeZero.ne μ)
   isOpenPosMeasure_of_mulLeftInvariant_of_compact K hK h2K
 #align measure_theory.is_open_pos_measure_of_mul_left_invariant_of_regular MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular
 #align measure_theory.is_open_pos_measure_of_add_left_invariant_of_regular MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular
 
+/-- A nonzero left-invariant inner regular measure gives positive mass to any open set. -/
+@[to_additive "A nonzero left-invariant inner regular measure gives positive mass to any open set."]
+instance (priority := 80) isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular
+    [InnerRegular μ] [NeZero μ] :
+    IsOpenPosMeasure μ :=
+  let ⟨K, hK, h2K⟩ := InnerRegular.exists_compact_not_null.mpr (NeZero.ne μ)
+  isOpenPosMeasure_of_mulLeftInvariant_of_compact K hK h2K
+
 @[to_additive]
 theorem null_iff_of_isMulLeftInvariant [Regular μ] {s : Set G} (hs : IsOpen s) :
     μ s = 0 ↔ s = ∅ ∨ μ = 0 := by
-  by_cases h3μ : μ = 0; · simp [h3μ]
-  · haveI := isOpenPosMeasure_of_mulLeftInvariant_of_regular h3μ
-    simp only [h3μ, or_false_iff, hs.measure_eq_zero_iff μ]
+  rcases eq_zero_or_neZero μ with rfl|hμ
+  · simp
+  · simp only [or_false_iff, hs.measure_eq_zero_iff μ, NeZero.ne μ]
 #align measure_theory.null_iff_of_is_mul_left_invariant MeasureTheory.null_iff_of_isMulLeftInvariant
 #align measure_theory.null_iff_of_is_add_left_invariant MeasureTheory.null_iff_of_isAddLeftInvariant
 
@@ -695,6 +722,40 @@ theorem measure_univ_of_isMulLeftInvariant [WeaklyLocallyCompactSpace G] [Noncom
 #align measure_theory.measure_univ_of_is_mul_left_invariant MeasureTheory.measure_univ_of_isMulLeftInvariant
 #align measure_theory.measure_univ_of_is_add_left_invariant MeasureTheory.measure_univ_of_isAddLeftInvariant
 
+@[to_additive]
+lemma _root_.MeasurableSet.mul_closure_one_eq {s : Set G} (hs : MeasurableSet s) :
+    s * (closure {1} : Set G) = s := by
+  apply MeasurableSet.induction_on_open (C := fun t ↦ t • (closure {1} : Set G) = t) ?_ ?_ ?_ hs
+  · intro U hU
+    exact hU.mul_closure_one_eq
+  · rintro t - ht
+    exact compl_mul_closure_one_eq_iff.2 ht
+  · rintro f - - h''f
+    simp only [iUnion_smul, h''f]
+
+/-- If a compact set is included in a measurable set, then so is its closure. -/
+@[to_additive]
+lemma _root_.IsCompact.closure_subset_of_measurableSet_of_group {k s : Set G}
+    (hk : IsCompact k) (hs : MeasurableSet s) (h : k ⊆ s) : closure k ⊆ s := by
+  rw [← hk.mul_closure_one_eq_closure, ← hs.mul_closure_one_eq]
+  exact mul_subset_mul_right h
+
+@[to_additive (attr := simp)]
+lemma measure_mul_closure_one (s : Set G) (μ : Measure G) :
+    μ (s * (closure {1} : Set G)) = μ s := by
+  apply le_antisymm ?_ (measure_mono (subset_mul_closure_one s))
+  conv_rhs => rw [measure_eq_iInf]
+  simp only [le_iInf_iff]
+  intro t kt t_meas
+  apply measure_mono
+  rw [← t_meas.mul_closure_one_eq]
+  exact smul_subset_smul_right kt
+
+@[to_additive]
+lemma _root_.IsCompact.measure_closure_eq_of_group {k : Set G} (hk : IsCompact k) (μ : Measure G) :
+    μ (closure k) = μ k := by
+  rw [← hk.mul_closure_one_eq_closure, measure_mul_closure_one]
+
 end TopologicalGroup
 
 section CommSemigroup
@@ -720,42 +781,46 @@ section Haar
 
 namespace Measure
 
-/-- A measure on an additive group is an additive Haar measure if it is left-invariant, and gives
-finite mass to compact sets and positive mass to open sets. -/
+/-- A measure on an additive group is an additive Haar measure if it is left-invariant, and
+gives finite mass to compact sets and positive mass to open sets.
+
+Textbooks generally require an additional regularity assumption to ensure nice behavior on
+arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
+`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
+sense is automatically regular and inner regular on second countable locally compact groups, as
+checked just below this definition. -/
 class IsAddHaarMeasure {G : Type*} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
   (μ : Measure G) extends IsFiniteMeasureOnCompacts μ, IsAddLeftInvariant μ, IsOpenPosMeasure μ :
   Prop
 #align measure_theory.measure.is_add_haar_measure MeasureTheory.Measure.IsAddHaarMeasure
 
-/-- A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact
-sets and positive mass to open sets. -/
+/-- A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to
+compact sets and positive mass to open sets.
+
+Textbooks generally require an additional regularity assumption to ensure nice behavior on
+arbitrary locally compact groups. Use `[IsHaarMeasure μ] [Regular μ]` or
+`[IsHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
+sense is automatically regular and inner regular on second countable locally compact groups, as
+checked just below this definition.-/
 @[to_additive existing]
 class IsHaarMeasure {G : Type*} [Group G] [TopologicalSpace G] [MeasurableSpace G]
   (μ : Measure G) extends IsFiniteMeasureOnCompacts μ, IsMulLeftInvariant μ, IsOpenPosMeasure μ :
   Prop
 #align measure_theory.measure.is_haar_measure MeasureTheory.Measure.IsHaarMeasure
 
-/-- Record that a Haar measure on a locally compact space is locally finite. This is needed as the
-fact that a measure which is finite on compacts is locally finite is not registered as an instance,
-to avoid an instance loop.
+#noalign measure_theory.measure.is_locally_finite_measure_of_is_haar_measure
+#noalign measure_theory.measure.is_locally_finite_measure_of_is_add_haar_measure
 
-See Note [lower instance priority]. -/
-@[to_additive
-"Record that an additive Haar measure on a locally compact space is locally finite. This is needed
-as the fact that a measure which is finite on compacts is locally finite is not registered as an
-instance, to avoid an instance loop.
+variable [Group G] [TopologicalSpace G] (μ : Measure G) [IsHaarMeasure μ]
 
-See Note [lower instance priority]"]
-instance (priority := 100) isLocallyFiniteMeasure_of_isHaarMeasure {G : Type*} [Group G]
-    [MeasurableSpace G] [TopologicalSpace G] [WeaklyLocallyCompactSpace G] (μ : Measure G)
-    [IsHaarMeasure μ] : IsLocallyFiniteMeasure μ :=
-  isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts
-#align measure_theory.measure.is_locally_finite_measure_of_is_haar_measure MeasureTheory.Measure.isLocallyFiniteMeasure_of_isHaarMeasure
-#align measure_theory.measure.is_locally_finite_measure_of_is_add_haar_measure MeasureTheory.Measure.isLocallyFiniteMeasure_of_isAddHaarMeasure
+/-! Check that typeclass inference knows that a Haar measure on a locally compact second countable
+topological group is automatically regular and inner regular. -/
 
-section
+example [TopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [BorelSpace G] :
+    Regular μ := by infer_instance
 
-variable [Group G] [TopologicalSpace G] (μ : Measure G) [IsHaarMeasure μ]
+example [TopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [BorelSpace G] :
+    InnerRegular μ := by infer_instance
 
 @[to_additive (attr := simp)]
 theorem haar_singleton [TopologicalGroup G] [BorelSpace G] (g : G) : μ {g} = μ {(1 : G)} := by
@@ -803,42 +868,67 @@ theorem isHaarMeasure_map [BorelSpace G] [TopologicalGroup G] {H : Type*} [Group
 #align measure_theory.measure.is_haar_measure_map MeasureTheory.Measure.isHaarMeasure_map
 #align measure_theory.measure.is_add_haar_measure_map MeasureTheory.Measure.isAddHaarMeasure_map
 
+/-- The image of a finite Haar measure under a continuous surjective group homomorphism is again
+a Haar measure. See also `isHaarMeasure_map`.-/
+@[to_additive
+"The image of a finite additive Haar measure under a continuous surjective additive group
+homomorphism is again an additive Haar measure. See also `isAddHaarMeasure_map`."]
+theorem isHaarMeasure_map_of_isFiniteMeasure
+    [BorelSpace G] [TopologicalGroup G] {H : Type*} [Group H]
+    [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [TopologicalGroup H] [IsFiniteMeasure μ]
+    (f : G →* H) (hf : Continuous f) (h_surj : Surjective f) :
+    IsHaarMeasure (Measure.map f μ) :=
+  { toIsMulLeftInvariant := isMulLeftInvariant_map f.toMulHom hf.measurable h_surj
+    lt_top_of_isCompact := fun _K hK ↦ hK.measure_lt_top
+    toIsOpenPosMeasure := hf.isOpenPosMeasure_map h_surj }
+
 /-- The image of a Haar measure under map of a left action is again a Haar measure. -/
 @[to_additive
    "The image of a Haar measure under map of a left additive action is again a Haar measure"]
-instance isHaarMeasure_map_smul {α} [BorelSpace G] [TopologicalGroup G] [T2Space G]
+instance isHaarMeasure_map_smul {α} [BorelSpace G] [TopologicalGroup G]
     [Group α] [MulAction α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G]
     [ContinuousConstSMul α G] (a : α) : IsHaarMeasure (Measure.map (a • · : G → G) μ) where
   toIsMulLeftInvariant := isMulLeftInvariant_map_smul _
   lt_top_of_isCompact K hK := by
-    rw [map_apply (measurable_const_smul _) hK.measurableSet]
+    let F := (Homeomorph.smul a (α := G)).toMeasurableEquiv
+    change map F μ K < ∞
+    rw [F.map_apply K]
     exact IsCompact.measure_lt_top <| (Homeomorph.isCompact_preimage (Homeomorph.smul a)).2 hK
   toIsOpenPosMeasure :=
     (continuous_const_smul a).isOpenPosMeasure_map (MulAction.surjective a)
 
 /-- The image of a Haar measure under right multiplication is again a Haar measure. -/
 @[to_additive isHaarMeasure_map_add_right
   "The image of a Haar measure under right addition is again a Haar measure."]
-instance isHaarMeasure_map_mul_right [BorelSpace G] [TopologicalGroup G] [T2Space G] (g : G) :
+instance isHaarMeasure_map_mul_right [BorelSpace G] [TopologicalGroup G] (g : G) :
     IsHaarMeasure (Measure.map (· * g) μ) :=
   isHaarMeasure_map_smul μ (MulOpposite.op g)
 
 /-- A convenience wrapper for `MeasureTheory.Measure.isHaarMeasure_map`. -/
 @[to_additive "A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`."]
 nonrec theorem _root_.MulEquiv.isHaarMeasure_map [BorelSpace G] [TopologicalGroup G] {H : Type*}
-    [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [T2Space H]
+    [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H]
     [TopologicalGroup H] (e : G ≃* H) (he : Continuous e) (hesymm : Continuous e.symm) :
     IsHaarMeasure (Measure.map e μ) :=
-  isHaarMeasure_map μ (e : G →* H) he e.surjective
-    ({ e with } : G ≃ₜ H).toCocompactMap.cocompact_tendsto'
+  { toIsMulLeftInvariant := isMulLeftInvariant_map e.toMulHom he.measurable e.surjective
+    lt_top_of_isCompact := by
+      intro K hK
+      let F : G ≃ₜ H := {
+        e.toEquiv with
+        continuous_toFun := he
+        continuous_invFun := hesymm }
+      change map F.toMeasurableEquiv μ K < ∞
+      rw [F.toMeasurableEquiv.map_apply K]
+      exact (F.isCompact_preimage.mpr hK).measure_lt_top
+    toIsOpenPosMeasure := he.isOpenPosMeasure_map e.surjective }
 #align mul_equiv.is_haar_measure_map MulEquiv.isHaarMeasure_map
 #align add_equiv.is_add_haar_measure_map AddEquiv.isAddHaarMeasure_map
 
 /-- A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map`. -/
 theorem _root_.ContinuousLinearEquiv.isAddHaarMeasure_map
     {E F R S : Type*} [Semiring R] [Semiring S]
     [AddCommGroup E] [Module R E] [AddCommGroup F] [Module S F]
-    [TopologicalSpace E] [TopologicalAddGroup E] [TopologicalSpace F] [T2Space F]
+    [TopologicalSpace E] [TopologicalAddGroup E] [TopologicalSpace F]
     [TopologicalAddGroup F]
     {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
     [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F]
@@ -872,14 +962,14 @@ instance prod.instIsHaarMeasure {G : Type*} [Group G] [TopologicalSpace G] {_ :
 /-- If the neutral element of a group is not isolated, then a Haar measure on this group has
 no atoms.
 
-The additive version of this instance applies in particular to show that an additive Haar measure on
-a nontrivial finite-dimensional real vector space has no atom. -/
+The additive version of this instance applies in particular to show that an additive Haar
+measure on a nontrivial finite-dimensional real vector space has no atom. -/
 @[to_additive
 "If the zero element of an additive group is not isolated, then an additive Haar measure on this
 group has no atoms.
 
-This applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional
-real vector space has no atom."]
+This applies in particular to show that an additive Haar measure on a nontrivial
+finite-dimensional real vector space has no atom."]
 instance (priority := 100) IsHaarMeasure.noAtoms [TopologicalGroup G] [BorelSpace G] [T1Space G]
     [WeaklyLocallyCompactSpace G] [(𝓝[≠] (1 : G)).NeBot] (μ : Measure G) [μ.IsHaarMeasure] :
     NoAtoms μ := by
@@ -893,8 +983,6 @@ instance (priority := 100) IsHaarMeasure.noAtoms [TopologicalGroup G] [BorelSpac
 #align measure_theory.measure.is_haar_measure.has_no_atoms MeasureTheory.Measure.IsHaarMeasure.noAtoms
 #align measure_theory.measure.is_add_haar_measure.has_no_atoms MeasureTheory.Measure.IsAddHaarMeasure.noAtoms
 
-end
-
 end Measure
 
 end Haar