feat(measure_theory): typeclass for measures positive on nonempty ope…

…ns (#11652)

Add a typeclass for measures positive on nonempty opens, migrate `is(_add?)_haar_measure` to this API.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

src/measure_theory/constructions/borel_space.lean

@@ -8,6 +8,7 @@ import analysis.complex.basic
 import analysis.normed_space.finite_dimension
 import measure_theory.group.arithmetic
 import measure_theory.lattice
+import measure_theory.measure.open_pos
 import topology.algebra.ordered.liminf_limsup
 import topology.continuous_function.basic
 import topology.instances.ereal
@@ -694,6 +695,15 @@ lemma closed_embedding.measurable {f : α → γ} (hf : closed_embedding f) :
   measurable f :=
 hf.continuous.measurable
 
+lemma continuous.is_open_pos_measure_map {f : β → γ} (hf : continuous f)
+  (hf_surj : function.surjective f) {μ : measure β} [μ.is_open_pos_measure] :
+  (measure.map f μ).is_open_pos_measure :=
+begin
+  refine ⟨λ U hUo hUne, _⟩,
+  rw [measure.map_apply hf.measurable hUo.measurable_set],
+  exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)
+end
+
 @[priority 100, to_additive]
 instance has_continuous_mul.has_measurable_mul [has_mul γ] [has_continuous_mul γ] :
   has_measurable_mul γ :=

src/measure_theory/covering/besicovitch_vector_space.lean

@@ -171,7 +171,7 @@ begin
     by simp only [μ.add_haar_ball_of_pos _ ρpos],
   have J : (s.card : ℝ≥0∞) * ennreal.of_real (δ ^ (finrank ℝ E))
     ≤ ennreal.of_real (ρ ^ (finrank ℝ E)) :=
-      (ennreal.mul_le_mul_right (μ.add_haar_ball_pos _ zero_lt_one).ne'
+      (ennreal.mul_le_mul_right (measure_ball_pos _ _ zero_lt_one).ne'
         measure_ball_lt_top.ne).1 I,
   have K : (s.card : ℝ) ≤ (5 : ℝ) ^ finrank ℝ E,
     by simpa [ennreal.to_real_mul, div_eq_mul_inv] using

src/measure_theory/group/basic.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn
 import measure_theory.integral.lebesgue
 import measure_theory.measure.regular
 import measure_theory.group.measurable_equiv
+import measure_theory.measure.open_pos
 
 /-!
 # Measures on Groups
@@ -189,48 +190,43 @@ variables [is_mul_left_invariant μ]
 /-- If a left-invariant measure gives positive mass to a compact set, then
 it gives positive mass to any open set. -/
 @[to_additive]
-lemma measure_pos_of_is_open_of_is_mul_left_invariant
-  {K : set G} (hK : is_compact K) (h : μ K ≠ 0) {U : set G} (hU : is_open U) (h'U : U.nonempty) :
-  0 < μ U :=
+lemma is_open_pos_measure_of_mul_left_invariant_of_compact
+  (K : set G) (hK : is_compact K) (h : μ K ≠ 0) :
+  is_open_pos_measure μ :=
 begin
+  refine ⟨λ U hU hne, _⟩,
   contrapose! h,
   rw ← nonpos_iff_eq_zero,
-  rw nonpos_iff_eq_zero at h,
-  rw ← hU.interior_eq at h'U,
+  rw ← hU.interior_eq at hne,
   obtain ⟨t, hKt⟩ : ∃ (t : finset G), K ⊆ ⋃ (g : G) (H : g ∈ t), (λ (h : G), g * h) ⁻¹' U :=
-    compact_covered_by_mul_left_translates hK h'U,
+    compact_covered_by_mul_left_translates hK hne,
   calc μ K ≤ μ (⋃ (g : G) (H : g ∈ t), (λ (h : G), g * h) ⁻¹' U) : measure_mono hKt
   ... ≤ ∑ g in t, μ ((λ (h : G), g * h) ⁻¹' U) : measure_bUnion_finset_le _ _
   ... = 0 : by simp [measure_preimage_mul, h]
 end
 
-/-! A nonzero left-invariant regular measure gives positive mass to any open set. -/
+/-- A nonzero left-invariant regular measure gives positive mass to any open set. -/
 @[to_additive]
-lemma null_iff_empty_of_is_mul_left_invariant [regular μ]
-  (hμ : μ ≠ 0) {s : set G} (hs : is_open s) :
-  μ s = 0 ↔ s = ∅ :=
-begin
-  obtain ⟨K, hK, h2K⟩ := regular.exists_compact_not_null.mpr hμ,
-  refine ⟨λ h, _, λ h, by simp only [h, measure_empty]⟩,
-  contrapose h,
-  exact (measure_pos_of_is_open_of_is_mul_left_invariant hK h2K hs (ne_empty_iff_nonempty.mp h)).ne'
-end
+lemma is_open_pos_measure_of_mul_left_invariant_of_regular [regular μ] (h₀ : μ ≠ 0) :
+  is_open_pos_measure μ :=
+let ⟨K, hK, h2K⟩ := regular.exists_compact_not_null.mpr h₀
+in is_open_pos_measure_of_mul_left_invariant_of_compact K hK h2K
 
 @[to_additive]
 lemma null_iff_of_is_mul_left_invariant [regular μ]
   {s : set G} (hs : is_open s) :
   μ s = 0 ↔ s = ∅ ∨ μ = 0 :=
 begin
-  by_cases hμ : μ = 0, { simp [hμ] },
-  simp only [hμ, or_false],
-  exact null_iff_empty_of_is_mul_left_invariant hμ hs,
+  by_cases h3μ : μ = 0, { simp [h3μ] },
+  { haveI := is_open_pos_measure_of_mul_left_invariant_of_regular h3μ,
+    simp only [h3μ, or_false, hs.measure_eq_zero_iff μ] },
 end
 
 @[to_additive]
 lemma measure_ne_zero_iff_nonempty_of_is_mul_left_invariant [regular μ]
   (hμ : μ ≠ 0) {s : set G} (hs : is_open s) :
   μ s ≠ 0 ↔ s.nonempty :=
-by simp_rw [← ne_empty_iff_nonempty, ne.def, null_iff_empty_of_is_mul_left_invariant hμ hs]
+by simpa [null_iff_of_is_mul_left_invariant hs, hμ] using ne_empty_iff_nonempty
 
 @[to_additive]
 lemma measure_pos_iff_nonempty_of_is_mul_left_invariant [regular μ]
@@ -270,21 +266,8 @@ lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (hμ : μ ≠ 0)
   {f : G → ℝ≥0∞} (hf : continuous f) :
   ∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=
 begin
-  split, swap, { rintro rfl, simp_rw [pi.zero_apply, lintegral_zero] },
-  intro h, contrapose h,
-  simp_rw [funext_iff, not_forall, pi.zero_apply] at h, cases h with x hx,
-  obtain ⟨r, h1r, h2r⟩ : ∃ r : ℝ≥0∞, 0 < r ∧ r < f x :=
-  exists_between (pos_iff_ne_zero.mpr hx),
-  have h3r := hf.is_open_preimage (Ioi r) is_open_Ioi,
-  let s := Ioi r,
-  rw [← ne.def, ← pos_iff_ne_zero],
-  have : 0 < r * μ (f ⁻¹' Ioi r),
-  { have : (f ⁻¹' Ioi r).nonempty, from ⟨x, h2r⟩,
-    simpa [h1r.ne', measure_pos_iff_nonempty_of_is_mul_left_invariant hμ h3r, h1r] },
-  refine this.trans_le _,
-  rw [← set_lintegral_const, ← lintegral_indicator _ h3r.measurable_set],
-  apply lintegral_mono,
-  refine indicator_le (λ y, le_of_lt),
+  haveI := is_open_pos_measure_of_mul_left_invariant_of_regular hμ,
+  rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]
 end
 
 end group
@@ -337,29 +320,20 @@ 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. -/
 class is_add_haar_measure {G : Type*} [add_group G] [topological_space G] [measurable_space G]
-  (μ : measure G) extends is_finite_measure_on_compacts μ, is_add_left_invariant μ : Prop :=
-(open_pos : ∀ (U : set G), is_open U → U.nonempty → 0 < μ U)
+  (μ : measure G)
+  extends is_finite_measure_on_compacts μ, is_add_left_invariant μ, is_open_pos_measure μ : Prop
 
 /-- 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. -/
 @[to_additive]
 class is_haar_measure {G : Type*} [group G] [topological_space G] [measurable_space G]
-  (μ : measure G) extends is_finite_measure_on_compacts μ, is_mul_left_invariant μ : Prop :=
-(open_pos : ∀ (U : set G), is_open U → U.nonempty → 0 < μ U)
+  (μ : measure G)
+  extends is_finite_measure_on_compacts μ, is_mul_left_invariant μ, is_open_pos_measure μ : Prop
 
 section
 
 variables [group G] [topological_space G] (μ : measure G) [is_haar_measure μ]
 
-@[to_additive]
-lemma _root_.is_open.haar_pos {U : set G} (hU : is_open U) (h'U : U.nonempty) :
-  0 < μ U :=
-is_haar_measure.open_pos U hU h'U
-
-@[to_additive]
-lemma haar_pos_of_nonempty_interior {U : set G} (hU : (interior U).nonempty) : 0 < μ U :=
-(is_open_interior.haar_pos μ hU).trans_le $ measure_mono interior_subset
-
 @[simp, to_additive]
 lemma haar_singleton [topological_group G] [borel_space G] (g : G) :
   μ {g} = μ {(1 : G)} :=
@@ -371,14 +345,8 @@ end
 @[to_additive measure_theory.measure.is_add_haar_measure.smul]
 lemma is_haar_measure.smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) :
   is_haar_measure (c • μ) :=
-{ lt_top_of_is_compact := λ K hK, begin
-    change c * μ K < ∞,
-    simp [lt_top_iff_ne_top, hK.measure_lt_top.ne, cpos, ctop],
-  end,
-  open_pos := λ U U_open U_ne, bot_lt_iff_ne_bot.2 $ begin
-    change c * μ U ≠ 0,
-    simp [cpos, (_root_.is_open.haar_pos μ U_open U_ne).ne'],
-  end }
+{ lt_top_of_is_compact := λ K hK, ennreal.mul_lt_top ctop hK.measure_lt_top.ne,
+  to_is_open_pos_measure := is_open_pos_measure_smul μ cpos }
 
 /-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then
 it is a Haar measure -/
@@ -389,7 +357,7 @@ lemma is_haar_measure_of_is_compact_nonempty_interior [topological_group G] [bor
   is_haar_measure μ :=
 { lt_top_of_is_compact :=
     λ L hL, measure_lt_top_of_is_compact_of_is_mul_left_invariant' h'K h' hL,
-  open_pos := λ U hU, measure_pos_of_is_open_of_is_mul_left_invariant hK h hU }
+  to_is_open_pos_measure := is_open_pos_measure_of_mul_left_invariant_of_compact K hK h }
 
 /-- The image of a Haar measure under a group homomorphism which is also a homeomorphism is again
 a Haar measure. -/
@@ -415,14 +383,7 @@ lemma is_haar_measure_map [borel_space G] [topological_group G] {H : Type*} [gro
     rw ← this,
     exact is_compact.measure_lt_top (hK.image hfsymm)
   end,
-  open_pos := begin
-    assume U hU h'U,
-    rw map_apply hf.measurable hU.measurable_set,
-    refine (hU.preimage hf).haar_pos _ _,
-    have : f.symm '' U = f ⁻¹' U := equiv.image_eq_preimage _ _,
-    rw ← this,
-    simp [h'U],
-  end }
+  to_is_open_pos_measure := hf.is_open_pos_measure_map f.surjective }
 
 /-- A Haar measure on a sigma-compact space is sigma-finite. -/
 @[priority 100, to_additive] -- see Note [lower instance priority]
@@ -467,7 +428,7 @@ begin
     rw B at A,
     rwa [ennreal.le_div_iff_mul_le _ (or.inr μKlt), mul_comm],
     right,
-    apply ne_of_gt (haar_pos_of_nonempty_interior μ ⟨_, K_int⟩) },
+    apply (measure_pos_of_nonempty_interior μ ⟨_, K_int⟩).ne' },
   have J : tendsto (λ (n : ℕ),  μ K / n) at_top (𝓝 (μ K / ∞)) :=
     ennreal.tendsto.const_div ennreal.tendsto_nat_nhds_top (or.inr μKlt),
   simp only [ennreal.div_top] at J,

src/measure_theory/integral/interval_integral.lean

@@ -5,7 +5,7 @@ Authors: Yury G. Kudryashov, Patrick Massot, Sébastien Gouëzel
 -/
 import analysis.normed_space.dual
 import data.set.intervals.disjoint
-import measure_theory.measure.lebesgue
+import measure_theory.measure.haar_lebesgue
 import analysis.calculus.extend_deriv
 import measure_theory.integral.set_integral
 import measure_theory.integral.vitali_caratheodory
@@ -1191,26 +1191,19 @@ end
 `f c < g c` at some point `c ∈ [a, b]`, then `∫ x in a..b, f x < ∫ x in a..b, g x`. -/
 lemma integral_lt_integral_of_continuous_on_of_le_of_exists_lt {f g : ℝ → ℝ} {a b : ℝ}
   (hab : a < b) (hfc : continuous_on f (Icc a b)) (hgc : continuous_on g (Icc a b))
-  (hle : ∀ x ∈ Icc a b, f x ≤ g x) (hlt : ∃ c ∈ Icc a b, f c < g c) :
+  (hle : ∀ x ∈ Ioc a b, f x ≤ g x) (hlt : ∃ c ∈ Icc a b, f c < g c) :
   ∫ x in a..b, f x < ∫ x in a..b, g x :=
 begin
   refine integral_lt_integral_of_ae_le_of_measure_set_of_lt_ne_zero hab.le
     (hfc.interval_integrable_of_Icc hab.le) (hgc.interval_integrable_of_Icc hab.le)
-    ((ae_restrict_mem measurable_set_Ioc).mono $ λ x hx, hle x (Ioc_subset_Icc_self hx)) _,
-  simp only [measure.restrict_apply' measurable_set_Ioc],
-  rcases hlt with ⟨c, ⟨hac, hcb⟩, hlt⟩,
-  have : ∀ᶠ x in 𝓝[Icc a b] c, f x < g x,
-    from ((hfc c ⟨hac, hcb⟩).prod (hgc c ⟨hac, hcb⟩)).eventually (is_open_lt_prod.mem_nhds hlt),
-  rcases (eventually_nhds_within_iff.1 this).exists_Ioo_subset with ⟨l, u, ⟨hlc, hcu⟩, hsub⟩,
-  have A : Ioo (max a l) (min b u) ⊆ Ioc a b,
-    from Ioo_subset_Ioc_self.trans (Ioc_subset_Ioc (le_max_left _ _) (min_le_left _ _)),
-  have B : Ioo (max a l) (min b u) ⊆ Ioo l u,
-    from Ioo_subset_Ioo (le_max_right _ _) (min_le_right _ _),
-  refine ne_of_gt _,
-  calc (0 : ℝ≥0∞) < volume (Ioo (max a l) (min b u)) :
-    by simp [hab, hlc.trans_le hcb, hac.trans_lt hcu, hlc.trans hcu]
-  ... ≤ volume ({x | f x < g x} ∩ Ioc a b) :
-    measure_mono (λ x hx, ⟨hsub (B hx) (Ioc_subset_Icc_self $ A hx), A hx⟩)
+    ((ae_restrict_mem measurable_set_Ioc).mono hle) _,
+  contrapose! hlt,
+  have h_eq : f =ᵐ[volume.restrict (Ioc a b)] g,
+  { simp only [← not_le, ← ae_iff] at hlt,
+    exact eventually_le.antisymm ((ae_restrict_iff' measurable_set_Ioc).2 $
+      eventually_of_forall hle) hlt },
+  simp only [measure.restrict_congr_set Ioc_ae_eq_Icc] at h_eq,
+  exact λ c hc, (measure.eq_on_Icc_of_ae_eq volume hab.ne h_eq hfc hgc hc).ge
 end
 
 lemma integral_nonneg_of_ae_restrict (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Icc a b)] f) :

src/measure_theory/measure/haar.lean

@@ -605,10 +605,10 @@ theorem is_haar_measure_eq_smul_is_haar_measure
   ∃ (c : ℝ≥0∞), (c ≠ 0) ∧ (c ≠ ∞) ∧ (μ = c • ν) :=
 begin
   have K : positive_compacts G := classical.choice (topological_space.nonempty_positive_compacts G),
-  have νpos : 0 < ν K.1 := haar_pos_of_nonempty_interior _ K.2.2,
+  have νpos : 0 < ν K.1 := measure_pos_of_nonempty_interior _ K.2.2,
   have νlt : ν K.1 < ∞ := is_compact.measure_lt_top K.2.1,
   refine ⟨μ K.1 / ν K.1, _, _, _⟩,
-  { simp only [νlt.ne, (μ.haar_pos_of_nonempty_interior K.property.right).ne', ne.def,
+  { simp only [νlt.ne, (μ.measure_pos_of_nonempty_interior K.property.right).ne', ne.def,
       ennreal.div_zero_iff, not_false_iff, or_self] },
   { simp only [div_eq_mul_inv, νpos.ne', (is_compact.measure_lt_top K.property.left).ne, or_self,
       ennreal.inv_eq_top, with_top.mul_eq_top_iff, ne.def, not_false_iff, and_false, false_and] },
@@ -657,7 +657,7 @@ begin
     by { conv_rhs { rw μeq },
          simp, },
   have : c^2 = 1^2 :=
-    (ennreal.mul_eq_mul_right (haar_pos_of_nonempty_interior _ K.2.2).ne'
+    (ennreal.mul_eq_mul_right (measure_pos_of_nonempty_interior _ K.2.2).ne'
       (is_compact.measure_lt_top K.2.1).ne).1 this,
   have : c = 1 := (ennreal.pow_strict_mono two_ne_zero).injective this,
   rw [hc, this, one_smul]

src/measure_theory/measure/haar_lebesgue.lean

@@ -373,16 +373,6 @@ begin
   rw [this, measure_preimage_add]
 end
 
-lemma add_haar_ball_pos {E : Type*} [normed_group E] [measurable_space E]
-  (μ : measure E) [is_add_haar_measure μ] (x : E) {r : ℝ} (hr : 0 < r) :
-  0 < μ (ball x r) :=
-is_open_ball.add_haar_pos μ (nonempty_ball.2 hr)
-
-lemma add_haar_closed_ball_pos {E : Type*} [normed_group E] [measurable_space E]
-  (μ : measure E) [is_add_haar_measure μ] (x : E) {r : ℝ} (hr : 0 < r) :
-  0 < μ (closed_ball x r) :=
-lt_of_lt_of_le (add_haar_ball_pos μ x hr) (measure_mono ball_subset_closed_ball)
-
 lemma add_haar_ball_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
   μ (ball x (r * s)) = ennreal.of_real (r ^ (finrank ℝ E)) * μ (ball 0 s) :=
 begin
@@ -560,7 +550,7 @@ begin
     = (μ (closed_ball x r) * (μ (closed_ball x r))⁻¹) * (μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) :
       by { simp only [div_eq_mul_inv], ring }
     ... = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u) :
-      by rw [ennreal.mul_inv_cancel (add_haar_closed_ball_pos μ x rpos).ne'
+      by rw [ennreal.mul_inv_cancel (measure_closed_ball_pos μ x rpos).ne'
           measure_closed_ball_lt_top.ne, one_mul],
 end
 
@@ -673,7 +663,7 @@ begin
     { simp only [uzero, ennreal.inv_eq_top, implies_true_iff, ne.def, not_false_iff] },
     congr' 1,
     apply ennreal.sub_eq_of_add_eq
-      (lt_of_le_of_lt (measure_mono (inter_subset_right _ _)) utop.lt_top).ne,
+      (ne_top_of_le_ne_top utop (measure_mono (inter_subset_right _ _))),
     rw [inter_comm _ u, inter_comm _ u],
     exact measure_inter_add_diff u vmeas },
   have L : tendsto (λ r, μ (sᶜ ∩ closed_ball x r) / μ (closed_ball x r)) (𝓝[>] 0) (𝓝 0),
@@ -682,14 +672,14 @@ begin
       filter_upwards [self_mem_nhds_within],
       assume r hr,
       rw [div_eq_mul_inv, ennreal.mul_inv_cancel],
-      { apply (add_haar_closed_ball_pos μ _ hr).ne' },
+      { exact (measure_closed_ball_pos μ _ hr).ne' },
       { exact measure_closed_ball_lt_top.ne } },
     have B := ennreal.tendsto.sub A h (or.inl ennreal.one_ne_top),
     simp only [tsub_self] at B,
     apply B.congr' _,
     filter_upwards [self_mem_nhds_within],
     rintros r (rpos : 0 < r),
-    convert I (closed_ball x r) sᶜ (add_haar_closed_ball_pos μ _ rpos).ne'
+    convert I (closed_ball x r) sᶜ (measure_closed_ball_pos μ _ rpos).ne'
       (measure_closed_ball_lt_top).ne hs.compl,
     rw compl_compl },
   have L' : tendsto (λ (r : ℝ), μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0) :=