feat(measure_theory): drop some measurable_set assumptions (#11536)

* make `exists_subordinate_pairwise_disjoint` work for `null_measurable_set`s;
* use `ae_disjoint` in `measure_Union₀`, drop `measure_Union_of_null_inter`;
* prove `measure_inter_add_diff` for `null_measurable_set`s;
* drop some `measurable_set` assumptions in `measure_union`, `measure_diff`, etc;
* golf.

src/measure_theory/constructions/borel_space.lean

@@ -623,8 +623,8 @@ begin
   { rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, -, hst⟩,
     have : directed_on (≤) s, from directed_on_iff_directed.2 (directed_of_sup $ λ _ _, id),
     simp only [← bsupr_measure_Iic hsc (hsd.exists_ge' hst) this, h] },
-  rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic measurable_set_Iic,
-      measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic measurable_set_Iic, h a, h b],
+  rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic,
+      measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic, h a, h b],
   { rw ← h a, exact (measure_lt_top μ _).ne },
   { exact (measure_lt_top μ _).ne }
 end
@@ -1239,7 +1239,6 @@ begin
     { apply disjoint_left.2 (λ x hx h'x, _),
       have : 0 < f x := h'x.2,
       exact lt_irrefl 0 (this.trans_le hx.2.le) },
-    { exact hs.inter (hf (measurable_set_singleton _)) },
     { exact hs.inter (hf measurable_set_Ioi) } },
   have B : μ (s ∩ f⁻¹' (Ioi 0)) = μ (s ∩ f⁻¹' {∞}) + μ (s ∩ f⁻¹' (Ioo 0 ∞)),
   { rw ← measure_union,
@@ -1254,7 +1253,6 @@ begin
     { apply disjoint_left.2 (λ x hx h'x, _),
       have : f x < ∞ := h'x.2.2,
       exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm)) },
-    { exact hs.inter (hf (measurable_set_singleton _)) },
     { exact hs.inter (hf measurable_set_Ioo) } },
   have C : μ (s ∩ f⁻¹' (Ioo 0 ∞)) = ∑' (n : ℤ), μ (s ∩ f⁻¹' (Ico (t^n) (t^(n+1)))),
   { rw [← measure_Union, ennreal.Ioo_zero_top_eq_Union_Ico_zpow (ennreal.one_lt_coe_iff.2 ht)

src/measure_theory/covering/besicovitch.lean

@@ -585,7 +585,7 @@ begin
       { rw [finset.set_bUnion_finset_image],
         exact le_trans (measure_mono (diff_subset_diff so (subset.refl _))) H },
     rw [← diff_inter_self_eq_diff,
-      measure_diff_le_iff_le_add _ omeas (inter_subset_right _ _) ((measure_lt_top μ _).ne)], swap,
+      measure_diff_le_iff_le_add _ (inter_subset_right _ _) ((measure_lt_top μ _).ne)], swap,
     { apply measurable_set.inter _ omeas,
       haveI : encodable (u i) := (u_count i).to_encodable,
       exact measurable_set.Union

src/measure_theory/decomposition/jordan.lean

@@ -369,7 +369,6 @@ begin
           (hS₄ ▸ measure_mono (set.inter_subset_right _ _)), zero_add],
     { refine set.disjoint_of_subset_left (set.inter_subset_right _ _)
         (set.disjoint_of_subset_right (set.inter_subset_right _ _) disjoint_compl_right) },
-    { exact hi.inter hS₁ },
     { exact hi.inter hS₁.compl } },
   have hμ₂ : (j₂.pos_part i).to_real = j₂.to_signed_measure (i ∩ Tᶜ),
   { rw [to_signed_measure, to_signed_measure_sub_apply (hi.inter hT₁.compl),
@@ -381,7 +380,6 @@ begin
           (hT₄ ▸ measure_mono (set.inter_subset_right _ _)), zero_add],
     { exact set.disjoint_of_subset_left (set.inter_subset_right _ _)
         (set.disjoint_of_subset_right (set.inter_subset_right _ _) disjoint_compl_right) },
-    { exact hi.inter hT₁ },
     { exact hi.inter hT₁.compl } },
   -- since the two signed measures associated with the Jordan decompositions are the same,
   -- and the symmetric difference of the Hahn decompositions have measure zero, the result follows

src/measure_theory/decomposition/radon_nikodym.lean

@@ -51,8 +51,7 @@ begin
     suffices : singular_part μ ν set.univ = 0,
     { rw [measure.coe_zero, pi.zero_apply, ← this],
       exact measure_mono (set.subset_univ _) },
-    rw [← set.union_compl_self E, measure_union (@disjoint_compl_right _ E _) hE₁ hE₁.compl,
-        hE₂, zero_add],
+    rw [← measure_add_measure_compl hE₁, hE₂, zero_add],
     have : (singular_part μ ν + ν.with_density (rn_deriv μ ν)) Eᶜ = μ Eᶜ,
     { rw ← hadd },
     rw [measure.coe_add, pi.add_apply, h hE₃] at this,

src/measure_theory/function/continuous_map_dense.lean

@@ -110,9 +110,7 @@ begin
       from μu.trans (ennreal.add_lt_add_right ennreal.coe_ne_top μF),
     convert this.le using 1,
     { rw [add_comm, ← measure_union, set.diff_union_of_subset (Fs.trans su)],
-      { exact disjoint_sdiff_self_left },
-      { exact (u_open.sdiff F_closed).measurable_set },
-      { exact F_closed.measurable_set } },
+      exacts [disjoint_sdiff_self_left, F_closed.measurable_set] },
     have : (2:ℝ≥0∞) * η = η + η := by simpa using add_mul (1:ℝ≥0∞) 1 η,
     rw this,
     abel },

src/measure_theory/group/fundamental_domain.lean

@@ -209,7 +209,7 @@ begin
     calc ∫ x in s, f x ∂μ = ∫ x in ⋃ g : G, g • t, f x ∂(μ.restrict s) :
       by rw [restrict_congr_set (hac ht.Union_smul_ae_eq), restrict_univ]
     ... = ∑' g : G, ∫ x in g • t, f x ∂(μ.restrict s) :
-      integral_Union_of_null_inter ht.measurable_set_smul
+      integral_Union_of_null_inter (λ g, (ht.measurable_set_smul g).null_measurable_set)
         (ht.pairwise_ae_disjoint.mono $ λ i j h, hac h) hfs.integrable.integrable_on
     ... = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ :
       by simp only [restrict_restrict (ht.measurable_set_smul _), inter_comm]
@@ -222,7 +222,7 @@ begin
     ... = ∑' g : G, ∫ x in g • s, f x ∂(μ.restrict t) :
       by simp only [hf, restrict_restrict (hs.measurable_set_smul _)]
     ... = ∫ x in ⋃ g : G, g • s, f x ∂(μ.restrict t) :
-      (integral_Union_of_null_inter hs.measurable_set_smul
+      (integral_Union_of_null_inter (λ g, (hs.measurable_set_smul g).null_measurable_set)
         (hs.pairwise_ae_disjoint.mono $ λ i j h, hac h) hft.integrable.integrable_on).symm
     ... = ∫ x in t, f x ∂μ :
       by rw [restrict_congr_set (hac hs.Union_smul_ae_eq), restrict_univ] },

src/measure_theory/integral/bochner.lean

@@ -203,16 +203,22 @@ by { ext1 x, simp_rw weighted_smul_apply, congr' 2, }
 lemma weighted_smul_null {s : set α} (h_zero : μ s = 0) : (weighted_smul μ s : F →L[ℝ] F) = 0 :=
 by { ext1 x, rw [weighted_smul_apply, h_zero], simp, }
 
-lemma weighted_smul_union (s t : set α) (hs : measurable_set s) (ht : measurable_set t)
+lemma weighted_smul_union' (s t : set α) (ht : measurable_set t)
   (hs_finite : μ s ≠ ∞) (ht_finite : μ t ≠ ∞) (h_inter : s ∩ t = ∅) :
   (weighted_smul μ (s ∪ t) : F →L[ℝ] F) = weighted_smul μ s + weighted_smul μ t :=
 begin
   ext1 x,
   simp_rw [add_apply, weighted_smul_apply,
-    measure_union (set.disjoint_iff_inter_eq_empty.mpr h_inter) hs ht,
+    measure_union (set.disjoint_iff_inter_eq_empty.mpr h_inter) ht,
     ennreal.to_real_add hs_finite ht_finite, add_smul],
 end
 
+@[nolint unused_arguments]
+lemma weighted_smul_union (s t : set α) (hs : measurable_set s) (ht : measurable_set t)
+  (hs_finite : μ s ≠ ∞) (ht_finite : μ t ≠ ∞) (h_inter : s ∩ t = ∅) :
+  (weighted_smul μ (s ∪ t) : F →L[ℝ] F) = weighted_smul μ s + weighted_smul μ t :=
+weighted_smul_union' s t ht hs_finite ht_finite h_inter
+
 lemma weighted_smul_smul [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class ℝ 𝕜 F]
   (c : 𝕜) (s : set α) (x : F) :
   weighted_smul μ s (c • x) = c • weighted_smul μ s x :=

src/measure_theory/integral/interval_integral.lean

@@ -853,9 +853,9 @@ lemma integral_Iic_sub_Iic (ha : integrable_on f (Iic a) μ) (hb : integrable_on
   ∫ x in Iic b, f x ∂μ - ∫ x in Iic a, f x ∂μ = ∫ x in a..b, f x ∂μ :=
 begin
   wlog hab : a ≤ b using [a b] tactic.skip,
-  { rw [sub_eq_iff_eq_add', integral_of_le hab, ← integral_union (Iic_disjoint_Ioc (le_refl _)),
+  { rw [sub_eq_iff_eq_add', integral_of_le hab, ← integral_union (Iic_disjoint_Ioc le_rfl),
       Iic_union_Ioc_eq_Iic hab],
-    exacts [measurable_set_Iic, measurable_set_Ioc, ha, hb.mono_set (λ _, and.right)] },
+    exacts [measurable_set_Ioc, ha, hb.mono_set (λ _, and.right)] },
   { intros ha hb,
     rw [integral_symm, ← this hb ha, neg_sub] }
 end

src/measure_theory/integral/set_integral.lean

@@ -72,27 +72,22 @@ lemma set_integral_congr_set_ae (hst : s =ᵐ[μ] t) :
   ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ :=
 by rw measure.restrict_congr_set hst
 
-lemma integral_union (hst : disjoint s t) (hs : measurable_set s) (ht : measurable_set t)
+lemma integral_union_ae (hst : ae_disjoint μ s t) (ht : null_measurable_set t μ)
   (hfs : integrable_on f s μ) (hft : integrable_on f t μ) :
   ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ :=
-by simp only [integrable_on, measure.restrict_union hst hs ht, integral_add_measure hfs hft]
+by simp only [integrable_on, measure.restrict_union₀ hst ht, integral_add_measure hfs hft]
 
-lemma integral_union_ae (hst : (s ∩ t : set α) =ᵐ[μ] (∅ : set α)) (hs : measurable_set s)
-  (ht : measurable_set t) (hfs : integrable_on f s μ) (hft : integrable_on f t μ) :
+lemma integral_union (hst : disjoint s t) (ht : measurable_set t)
+  (hfs : integrable_on f s μ) (hft : integrable_on f t μ) :
   ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ :=
-begin
-  have : s =ᵐ[μ] s \ t,
-  { refine (hst.mem_iff.mono _).set_eq, simp },
-  rw [← diff_union_self, integral_union disjoint_diff.symm, set_integral_congr_set_ae this],
-  exacts [hs.diff ht, ht, hfs.mono_set (diff_subset _ _), hft]
-end
+integral_union_ae hst.ae_disjoint ht.null_measurable_set hfs hft
 
-lemma integral_diff (hs : measurable_set s) (ht : measurable_set t) (hfs : integrable_on f s μ)
+lemma integral_diff (ht : measurable_set t) (hfs : integrable_on f s μ)
   (hft : integrable_on f t μ) (hts : t ⊆ s) :
   ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ - ∫ x in t, f x ∂μ :=
 begin
   rw [eq_sub_iff_add_eq, ← integral_union, diff_union_of_subset hts],
-  exacts [disjoint_diff.symm, hs.diff ht, ht, hfs.mono_set (diff_subset _ _), hft]
+  exacts [disjoint_diff.symm, ht, hfs.mono_set (diff_subset _ _), hft]
 end
 
 lemma integral_finset_bUnion {ι : Type*} (t : finset ι) {s : ι → set α}
@@ -104,7 +99,7 @@ begin
   { simp },
   { simp only [finset.coe_insert, finset.forall_mem_insert, set.pairwise_insert,
       finset.set_bUnion_insert] at hs hf h's ⊢,
-    rw [integral_union _ hs.1 _ hf.1 (integrable_on_finset_Union.2 hf.2)],
+    rw [integral_union _ _ hf.1 (integrable_on_finset_Union.2 hf.2)],
     { rw [finset.sum_insert hat, IH hs.2 h's.1 hf.2] },
     { simp only [disjoint_Union_right],
       exact (λ i hi, (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1) },
@@ -127,7 +122,7 @@ lemma integral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [meas
 
 lemma integral_add_compl (hs : measurable_set s) (hfi : integrable f μ) :
   ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ :=
-by rw [← integral_union (@disjoint_compl_right (set α) _ _) hs hs.compl
+by rw [← integral_union (@disjoint_compl_right (set α) _ _) hs.compl
     hfi.integrable_on hfi.integrable_on, union_compl_self, integral_univ]
 
 /-- For a function `f` and a measurable set `s`, the integral of `indicator s f`
@@ -162,10 +157,10 @@ begin
   have : ∀ᶠ i in at_top, ν (s i) ∈ Icc (ν S - ε) (ν S + ε),
     from tendsto_measure_Union hsm h_mono (ennreal.Icc_mem_nhds hfi'.ne (ennreal.coe_pos.2 ε0).ne'),
   refine this.mono (λ i hi, _),
-  rw [mem_closed_ball_iff_norm', ← integral_diff hSm (hsm i) hfi (hfi.mono_set hsub) hsub,
+  rw [mem_closed_ball_iff_norm', ← integral_diff (hsm i) hfi (hfi.mono_set hsub) hsub,
     ← coe_nnnorm, nnreal.coe_le_coe, ← ennreal.coe_le_coe],
   refine (ennnorm_integral_le_lintegral_ennnorm _).trans _,
-  rw [← with_density_apply _ (hSm.diff (hsm _)), ← hν, measure_diff hsub hSm (hsm _)],
+  rw [← with_density_apply _ (hSm.diff (hsm _)), ← hν, measure_diff hsub (hsm _)],
   exacts [tsub_le_iff_tsub_le.mp hi.1,
     (hi.2.trans_lt $ ennreal.add_lt_top.2 ⟨hfi', ennreal.coe_lt_top⟩).ne]
 end
@@ -189,7 +184,7 @@ lemma integral_Union {ι : Type*} [encodable ι] {s : ι → set α} {f : α →
 (has_sum.tsum_eq (has_sum_integral_Union hm hd hfi)).symm
 
 lemma has_sum_integral_Union_of_null_inter {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
-  (hm : ∀ i, measurable_set (s i)) (hd : pairwise (λ i j, μ (s i ∩ s j) = 0))
+  (hm : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s))
   (hfi : integrable_on f (⋃ i, s i) μ) :
   has_sum (λ n, ∫ a in s n, f a ∂ μ) (∫ a in ⋃ n, s n, f a ∂μ) :=
 begin
@@ -200,7 +195,7 @@ begin
 end
 
 lemma integral_Union_of_null_inter {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
-  (hm : ∀ i, measurable_set (s i)) (hd : pairwise (λ i j, μ (s i ∩ s j) = 0))
+  (hm : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s))
   (hfi : integrable_on f (⋃ i, s i) μ) :
   (∫ a in (⋃ n, s n), f a ∂μ) = ∑' n, ∫ a in s n, f a ∂ μ :=
 (has_sum.tsum_eq (has_sum_integral_Union_of_null_inter hm hd hfi)).symm
@@ -216,20 +211,13 @@ begin
   exact ht_eq x hx,
 end
 
-private lemma set_integral_union_eq_left_of_disjoint {f : α → E} (hf : measurable f)
-  (hfi : integrable f μ) (hs : measurable_set s) (ht : measurable_set t) (ht_eq : ∀ x ∈ t, f x = 0)
-  (hs_disj : disjoint s t) :
-  ∫ x in (s ∪ t), f x ∂μ = ∫ x in s, f x ∂μ :=
-by rw [integral_union hs_disj hs ht hfi.integrable_on hfi.integrable_on,
-  set_integral_eq_zero_of_forall_eq_zero hf ht_eq, add_zero]
-
 lemma set_integral_union_eq_left {f : α → E} (hf : measurable f) (hfi : integrable f μ)
-  (hs : measurable_set s) (ht : measurable_set t) (ht_eq : ∀ x ∈ t, f x = 0) :
+  (hs : measurable_set s) (ht_eq : ∀ x ∈ t, f x = 0) :
   ∫ x in (s ∪ t), f x ∂μ = ∫ x in s, f x ∂μ :=
 begin
-  rw [← set.union_diff_self, integral_union,
-    set_integral_eq_zero_of_forall_eq_zero _ (λ x hx, ht_eq x (diff_subset _ _ hx)), add_zero],
-  exacts [hf, disjoint_diff, hs, ht.diff hs, hfi.integrable_on, hfi.integrable_on]
+  rw [← set.union_diff_self, union_comm, integral_union,
+    set_integral_eq_zero_of_forall_eq_zero _ (λ x hx, ht_eq x (diff_subset _ _ hx)), zero_add],
+  exacts [hf, disjoint_diff.symm, hs, hfi.integrable_on, hfi.integrable_on]
 end
 
 lemma set_integral_neg_eq_set_integral_nonpos [linear_order E] [order_closed_topology E]
@@ -240,7 +228,7 @@ begin
     by { ext, simp_rw [set.mem_union_eq, set.mem_set_of_eq], exact le_iff_lt_or_eq, },
   rw h_union,
   exact (set_integral_union_eq_left hf hfi (measurable_set_lt hf measurable_const)
-    (measurable_set_eq_fun hf measurable_const) (λ x hx, hx)).symm,
+    (λ x hx, hx)).symm,
 end
 
 lemma integral_norm_eq_pos_sub_neg {f : α → ℝ} (hf : measurable f) (hfi : integrable f μ) :

src/measure_theory/measure/ae_disjoint.lean

@@ -82,6 +82,16 @@ union_left_iff.mpr ⟨hs, ht⟩
 lemma union_right (ht : ae_disjoint μ s t) (hu : ae_disjoint μ s u) : ae_disjoint μ s (t ∪ u) :=
 union_right_iff.2 ⟨ht, hu⟩
 
+lemma diff_ae_eq_left (h : ae_disjoint μ s t) : (s \ t : set α) =ᵐ[μ] s :=
+@diff_self_inter _ s t ▸ diff_null_ae_eq_self h
+
+lemma diff_ae_eq_right (h : ae_disjoint μ s t) : (t \ s : set α) =ᵐ[μ] t := h.symm.diff_ae_eq_left
+
+lemma measure_diff_left (h : ae_disjoint μ s t) : μ (s \ t) = μ s := measure_congr h.diff_ae_eq_left
+
+lemma measure_diff_right (h : ae_disjoint μ s t) : μ (t \ s) = μ t :=
+measure_congr h.diff_ae_eq_right
+
 /-- If `s` and `t` are `μ`-a.e. disjoint, then `s \ u` and `t` are disjoint for some measurable null
 set `u`. -/
 lemma exists_disjoint_diff (h : ae_disjoint μ s t) :

src/measure_theory/measure/haar_lebesgue.lean

@@ -440,12 +440,10 @@ by rw [add_haar_closed_ball' μ x hr, add_haar_closed_unit_ball_eq_add_haar_unit
 lemma add_haar_sphere_of_ne_zero (x : E) {r : ℝ} (hr : r ≠ 0) :
   μ (sphere x r) = 0 :=
 begin
-  rcases lt_trichotomy r 0 with h|rfl|h,
+  rcases hr.lt_or_lt with h|h,
   { simp only [empty_diff, measure_empty, ← closed_ball_diff_ball, closed_ball_eq_empty.2 h] },
-  { exact (hr rfl).elim },
   { rw [← closed_ball_diff_ball,
-        measure_diff ball_subset_closed_ball measurable_set_closed_ball measurable_set_ball
-          measure_ball_lt_top.ne,
+        measure_diff ball_subset_closed_ball measurable_set_ball measure_ball_lt_top.ne,
         add_haar_ball_of_pos μ _ h, add_haar_closed_ball μ _ h.le, tsub_self];
     apply_instance }
 end
@@ -454,8 +452,7 @@ lemma add_haar_sphere [nontrivial E] (x : E) (r : ℝ) :
   μ (sphere x r) = 0 :=
 begin
   rcases eq_or_ne r 0 with rfl|h,
-  { simp only [← closed_ball_diff_ball, diff_empty, closed_ball_zero,
-               ball_zero, measure_singleton] },
+  { rw [sphere_zero, measure_singleton] },
   { exact add_haar_sphere_of_ne_zero μ x h }
 end