feat(measure_theory/measure/measure_space): In sigma finite measure s…

…paces, disjoint unions can have at most countably many positive measure parts. (#15492)

Main addition of this PR: In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts.

Also in this PR: A disjoint union whose measure is finite has at most finitely many parts of measure greater than any positive constant.



Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>

src/data/set/intervals/disjoint.lean

@@ -170,4 +170,26 @@ lemma is_lub.bUnion_Iic_eq_Iic (a_lub : is_lub s a) (a_mem : a ∈ s) :
   (⋃ x ∈ s, Iic x) = Iic a :=
 a_lub.dual.bUnion_Ici_eq_Ici a_mem
 
+lemma Union_Ici_eq_Ioi_infi {R : Type*} [complete_linear_order R]
+  {f : ι → R} (no_least_elem : (⨅ i, f i) ∉ range f) :
+  (⋃ (i : ι), Ici (f i)) = Ioi (⨅ i, f i) :=
+by simp only [← is_glb.bUnion_Ici_eq_Ioi (@is_glb_infi _ _ _ f) no_least_elem,
+              mem_range, Union_exists, Union_Union_eq']
+
+lemma Union_Iic_eq_Iio_supr {R : Type*} [complete_linear_order R]
+  {f : ι → R} (no_greatest_elem : (⨆ i, f i) ∉ range f) :
+  (⋃ (i : ι), Iic (f i)) = Iio (⨆ i, f i) :=
+@Union_Ici_eq_Ioi_infi ι (order_dual R) _ f no_greatest_elem
+
+lemma Union_Ici_eq_Ici_infi {R : Type*} [complete_linear_order R]
+  {f : ι → R} (has_least_elem : (⨅ i, f i) ∈ range f) :
+  (⋃ (i : ι), Ici (f i)) = Ici (⨅ i, f i) :=
+by simp only [← is_glb.bUnion_Ici_eq_Ici (@is_glb_infi _ _ _ f) has_least_elem,
+              mem_range, Union_exists, Union_Union_eq']
+
+lemma Union_Iic_eq_Iic_supr {R : Type*} [complete_linear_order R]
+  {f : ι → R} (has_greatest_elem : (⨆ i, f i) ∈ range f) :
+  (⋃ (i : ι), Iic (f i)) = Iic (⨆ i, f i) :=
+@Union_Ici_eq_Ici_infi ι (order_dual R) _ f has_greatest_elem
+
 end Union_Ixx

src/measure_theory/measure/measure_space.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 import measure_theory.measure.null_measurable
 import measure_theory.measurable_space
+import topology.algebra.order.liminf_limsup
 
 /-!
 # Measure spaces
@@ -174,6 +175,21 @@ lemma measure_bUnion_finset {s : finset ι} {f : ι → set α} (hd : pairwise_d
   μ (⋃ b ∈ s, f b) = ∑ p in s, μ (f p) :=
 measure_bUnion_finset₀ hd.ae_disjoint (λ b hb, (hm b hb).null_measurable_set)
 
+/-- The measure of a disjoint union (even uncountable) of measurable sets is at least the sum of
+the measures of the sets. -/
+lemma tsum_meas_le_meas_Union_of_disjoint {ι : Type*} [measurable_space α] (μ : measure α)
+  {As : ι → set α} (As_mble : ∀ (i : ι), measurable_set (As i))
+  (As_disj : pairwise (disjoint on As)) :
+  ∑' i, μ (As i) ≤ μ (⋃ i, As i) :=
+begin
+  rcases (show summable (λ i, μ (As i)), from ennreal.summable) with ⟨S, hS⟩,
+  rw [hS.tsum_eq],
+  refine tendsto_le_of_eventually_le hS tendsto_const_nhds (eventually_of_forall _),
+  intros s,
+  rw ← measure_bUnion_finset (λ i hi j hj hij, As_disj hij) (λ i _, As_mble i),
+  exact measure_mono (Union₂_subset_Union (λ (i : ι), i ∈ s) (λ (i : ι), As i)),
+end
+
 /-- If `s` is a countable set, then the measure of its preimage can be found as the sum of measures
 of the fibers `f ⁻¹' {y}`. -/
 lemma tsum_measure_preimage_singleton {s : set β} (hs : s.countable) {f : α → β}
@@ -2990,6 +3006,83 @@ begin
   exact (measure_mono (inter_subset_right _ _)).trans_lt (measure_spanning_sets_lt_top _ _),
 end
 
+/-- A set in a σ-finite space has zero measure if and only if its intersection with
+all members of the countable family of finite measure spanning sets has zero measure. -/
+lemma forall_measure_inter_spanning_sets_eq_zero
+  [measurable_space α] {μ : measure α} [sigma_finite μ] (s : set α) :
+  (∀ n, μ (s ∩ (spanning_sets μ n)) = 0) ↔ μ s = 0 :=
+begin
+  nth_rewrite 0 (show s = ⋃ n, (s ∩ (spanning_sets μ n)),
+                 by rw [← inter_Union, Union_spanning_sets, inter_univ]),
+  rw [measure_Union_null_iff],
+end
+
+/-- A set in a σ-finite space has positive measure if and only if its intersection with
+some member of the countable family of finite measure spanning sets has positive measure. -/
+lemma exists_measure_inter_spanning_sets_pos
+  [measurable_space α] {μ : measure α} [sigma_finite μ] (s : set α) :
+  (∃ n, 0 < μ (s ∩ (spanning_sets μ n))) ↔ 0 < μ s :=
+begin
+  rw ← not_iff_not,
+  simp only [not_exists, not_lt, nonpos_iff_eq_zero],
+  exact forall_measure_inter_spanning_sets_eq_zero s,
+end
+
+/-- If the union of disjoint measurable sets has finite measure, then there are only
+finitely many members of the union whose measure exceeds any given positive number. -/
+lemma finite_const_le_meas_of_disjoint_Union {ι : Type*} [measurable_space α] (μ : measure α)
+  {ε : ℝ≥0∞} (ε_pos : 0 < ε) {As : ι → set α} (As_mble : ∀ (i : ι), measurable_set (As i))
+  (As_disj : pairwise (disjoint on As)) (Union_As_finite : μ (⋃ i, As i) ≠ ∞) :
+  set.finite {i : ι | ε ≤ μ (As i)} :=
+begin
+  by_contradiction con,
+  have aux := lt_of_le_of_lt (tsum_meas_le_meas_Union_of_disjoint μ As_mble As_disj)
+                              (lt_top_iff_ne_top.mpr Union_As_finite),
+  exact con (ennreal.finite_const_le_of_tsum_ne_top aux.ne ε_pos.ne.symm),
+end
+
+/-- If the union of disjoint measurable sets has finite measure, then there are only
+countably many members of the union whose measure is positive. -/
+lemma countable_meas_pos_of_disjoint_of_meas_Union_ne_top {ι : Type*} [measurable_space α]
+  (μ : measure α) {As : ι → set α} (As_mble : ∀ (i : ι), measurable_set (As i))
+  (As_disj : pairwise (disjoint on As)) (Union_As_finite : μ (⋃ i, As i) ≠ ∞) :
+  set.countable {i : ι | 0 < μ (As i)} :=
+begin
+  set posmeas := {i : ι | 0 < μ (As i)} with posmeas_def,
+  rcases exists_seq_strict_anti_tendsto' ennreal.zero_lt_one with ⟨as, ⟨as_decr, ⟨as_mem, as_lim⟩⟩⟩,
+  set fairmeas := λ (n : ℕ) , {i : ι | as n ≤ μ (As i)} with fairmeas_def,
+  have countable_union : posmeas = (⋃ n, fairmeas n) ,
+  { have fairmeas_eq : ∀ n, fairmeas n = (λ i, μ (As i)) ⁻¹' Ici (as n),
+      from λ n, by simpa only [fairmeas_def],
+    simpa only [fairmeas_eq, posmeas_def, ← preimage_Union,
+                Union_Ici_eq_Ioi_of_lt_of_tendsto (0 : ℝ≥0∞) (λ n, (as_mem n).1) as_lim], },
+  rw countable_union,
+  refine countable_Union (λ n, finite.countable _),
+  refine finite_const_le_meas_of_disjoint_Union μ (as_mem n).1 As_mble As_disj Union_As_finite,
+end
+
+/-- In a σ-finite space, among disjoint measurable sets, only countably many can have positive
+measure. -/
+lemma countable_meas_pos_of_disjoint_Union
+  {ι : Type*} [measurable_space α] {μ : measure α} [sigma_finite μ]
+  {As : ι → set α} (As_mble : ∀ (i : ι), measurable_set (As i))
+  (As_disj : pairwise (disjoint on As)) :
+  set.countable {i : ι | 0 < μ (As i)} :=
+begin
+  have obs : {i : ι | 0 < μ (As i)} ⊆ (⋃ n, {i : ι | 0 < μ ((As i) ∩ (spanning_sets μ n))}),
+  { intros i i_in_nonzeroes,
+    by_contra con,
+    simp only [mem_Union, mem_set_of_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *,
+    simpa [(forall_measure_inter_spanning_sets_eq_zero _).mp con] using i_in_nonzeroes, },
+  apply countable.mono obs,
+  refine countable_Union (λ n, countable_meas_pos_of_disjoint_of_meas_Union_ne_top μ _ _ _),
+  { exact λ i, measurable_set.inter (As_mble i) (measurable_spanning_sets μ n), },
+  { exact λ i j i_ne_j b hbi hbj, As_disj i_ne_j
+            (hbi.trans (inter_subset_left _ _)) (hbj.trans (inter_subset_left _ _)), },
+  { refine (lt_of_le_of_lt (measure_mono _) (measure_spanning_sets_lt_top μ n)).ne,
+    exact Union_subset (λ i, inter_subset_right _ _), },
+end
+
 /-- The measurable superset `to_measurable μ t` of `t` (which has the same measure as `t`)
 satisfies, for any measurable set `s`, the equality `μ (to_measurable μ t ∩ s) = μ (t ∩ s)`.
 This only holds when `μ` is σ-finite. For a version without this assumption (but requiring

src/topology/algebra/order/liminf_limsup.lean

@@ -320,6 +320,46 @@ f_incr.map_Liminf_of_continuous_at f_cont
 
 end monotone
 
+section infi_and_supr
+
+open_locale topological_space
+
+open filter set
+
+variables {ι : Type*} {R : Type*} [complete_linear_order R] [topological_space R] [order_topology R]
+
+lemma infi_eq_of_forall_le_of_tendsto {x : R} {as : ι → R}
+  (x_le : ∀ i, x ≤ as i) {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
+  (⨅ i, as i) = x :=
+begin
+  refine infi_eq_of_forall_ge_of_forall_gt_exists_lt (λ i, x_le i) _,
+  apply λ w x_lt_w, ‹filter.ne_bot F›.nonempty_of_mem (eventually_lt_of_tendsto_lt x_lt_w as_lim),
+end
+
+lemma supr_eq_of_forall_le_of_tendsto {x : R} {as : ι → R}
+  (le_x : ∀ i, as i ≤ x) {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
+  (⨆ i, as i) = x :=
+@infi_eq_of_forall_le_of_tendsto ι (order_dual R) _ _ _ x as le_x F _ as_lim
+
+lemma Union_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
+  {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
+  (⋃ (i : ι), Ici (as i)) = Ioi x :=
+begin
+  have obs : x ∉ range as,
+  { intro maybe_x_is,
+    rcases mem_range.mp maybe_x_is with ⟨i, hi⟩,
+    simpa only [hi, lt_self_iff_false] using x_lt i, } ,
+  rw ← infi_eq_of_forall_le_of_tendsto (λ i, (x_lt i).le) as_lim at *,
+  exact Union_Ici_eq_Ioi_infi obs,
+end
+
+lemma Union_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
+  {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
+  (⋃ (i : ι), Iic (as i)) = Iio x :=
+@Union_Ici_eq_Ioi_of_lt_of_tendsto (order_dual R) _ _ _ ι x as lt_x F _ as_lim
+
+end infi_and_supr
+
 section indicator
 
 open_locale big_operators