Lemma about volume of union

Stream: mathlib4

[Gareth Ma]

I want to prove the if $S_x$ are measurable sets in $\mathbb{R}^n$ with volume $\geq c$ a positive constant (say a ball or a square) that are pairwise disjoint and $\bigcup_{x \in s} S_x$ is bounded then $s$ must be finite. My strategy was to prove that $\bigcup_{x \in s} S_x \subseteq \mathcal{B}(large radius)$, and since $S_x$ are pairwise disjoint the volume of LHS is $\sum_{x \in s} \mathrm{Vol}(S_x)$ which is finite etc. However, this is failing miserably, as the proof attempt below asks me to prove $s$ is countable, which I don't know how to (without going the same path). Any ideas?

import Mathlib.Order.CompletePartialOrder
import Mathlib.MeasureTheory.Measure.Haar.OfBasis

open ENNReal MeasureTheory Bornology

theorem aux {ι : Type*} {s : Set ι} {f : ι → Set (EuclideanSpace ℝ (Fin 8))} {c : ℝ≥0∞} (hc : 0 < c)
    (h_bounded : IsBounded (⋃ x ∈ s, f x))
    (h_measure : ∀ x ∈ s, c ≤ volume (f x))
    (h_disjoint : s.PairwiseDisjoint f) :
    Set.Finite s := by
  obtain ⟨L, hL⟩ := h_bounded.subset_ball 0
  -- obtain ⟨L, hL⟩ := isBounded_iff_forall_norm_le.mp h_bounded
  have := volume.mono hL
  rw [OuterMeasure.measureOf_eq_coe, Measure.coe_toOuterMeasure, Set.biUnion_eq_iUnion,
    measure_iUnion] at this
  sorry

[Edward van de Meent]

you i think you'd need lemmas relating to SeparableSpace for that

[Edward van de Meent]

perhaps you might be able to argue that each $S_x$ has to contain some open ball due to having positive volume, then apply something like theorem Pairwise.countable_of_isOpen_disjoint ?

[Gareth Ma]

I will try that path, thanks :)

[Gareth Ma]

(deleted)

[Etienne Marion]

Another way would be to assume that s is infinite, and then do the reasoning on a subset of s which is countable, which will bring you a contradiction

[Gareth Ma]

Edward van de Meent said:

perhaps you might be able to argue that each $S_x$ has to contain some open ball due to having positive volume, then apply something like theorem Pairwise.countable_of_isOpen_disjoint ?

I think positive volume doesn't have to contain open balls, see fat cantor set (I googled it up).

[Gareth Ma]

I'll try the "reasoning on countable subset of s" path, seems interesting too

[Edward van de Meent]

ah right, oops :upside_down:

[Gareth Ma]

The countable subset trick(?) works well, thanks :)

import Mathlib.Order.CompletePartialOrder
import Mathlib.MeasureTheory.Measure.Haar.OfBasis
import Mathlib.Data.Real.Cardinality
import Mathlib.Data.Set.Card
import Mathlib.Data.Real.ENatENNReal
import SpherePacking.ForMathlib.VolumeOfBalls

open ENNReal MeasureTheory Bornology TopologicalSpace Cardinal EuclideanSpace

-- proven in Carleson! (and PR'ing)
axiom ENNReal.tsum_const_eq' {α : Type*} (s : Set α) (c : ENNReal) :
    ∑' (_ : s), c = s.encard * c

theorem aux {ι : Type*} {s : Set ι} {f : ι → Set (EuclideanSpace ℝ (Fin 8))} {c : ℝ≥0∞} (hc : 0 < c)
    (h_measurable : ∀ x ∈ s, MeasurableSet (f x))
    (h_bounded : IsBounded (⋃ x ∈ s, f x))
    (h_volume : ∀ x ∈ s, c ≤ volume (f x))
    (h_disjoint : s.PairwiseDisjoint f) :
    s.Finite := by
  wlog h_countable : s.Countable with h_wlog
  · by_contra! h_finite
    rw [Set.Countable, ← mk_le_aleph0_iff, not_le] at h_countable
    -- countable subset
    obtain ⟨t, ⟨ht_subset, ht_aleph0⟩⟩ := le_mk_iff_exists_subset.mp h_countable.le
    have ht_infinite : Infinite t := aleph0_le_mk_iff.mp ht_aleph0.symm.le
    have ht_countable := mk_le_aleph0_iff.mp ht_aleph0.le
    specialize @h_wlog _ t f c hc ?_ ?_ ?_ ?_ ht_countable
    · exact fun x hx ↦ h_measurable x (ht_subset hx)
    · exact h_bounded.subset <| Set.biUnion_mono ht_subset (by intros; rfl)
    · exact fun x hx ↦ h_volume x (ht_subset hx)
    · exact Set.Pairwise.mono ht_subset h_disjoint
    · exact ht_infinite.not_finite h_wlog
  · haveI : Countable s := h_countable
    obtain ⟨L, hL⟩ := h_bounded.subset_ball 0
    have h_volume' := volume.mono hL
    rw [OuterMeasure.measureOf_eq_coe, Measure.coe_toOuterMeasure, Set.biUnion_eq_iUnion,
      measure_iUnion] at h_volume'
    · have h_le := tsum_mono (f := fun _ ↦ c) (g := fun (x : s) ↦ volume (f x)) ?_ ?_ ?_
      · have h₁ := (tsum_const_eq' _ _ ▸ h_le).trans h_volume'
        rw [← Set.encard_lt_top_iff, ← ENat.toENNReal_lt, ENat.toENNReal_top]
        refine lt_of_le_of_lt ((ENNReal.le_div_iff_mul_le ?_ ?_).mpr h₁) <| div_lt_top ?_ hc.ne.symm
        · left; positivity
        · right; exact (volume_ball_lt_top _).ne
        · exact (volume_ball_lt_top _).ne
      · exact ENNReal.summable
      · exact ENNReal.summable
      · intro x
        exact h_volume x.val x.prop
    · intro ⟨x, hx⟩ ⟨y, hy⟩ hxy
      exact h_disjoint hx hy (by simpa using hxy)
    · exact fun ⟨x, hx⟩ ↦ h_measurable x hx

[Gareth Ma]

I love ENNReal.summable

[Edward van de Meent]

oh yea, it's really convenient :grinning_face_with_smiling_eyes:

[Yury G. Kudryashov]

See exists_nonempty_inter_of_measure_univ_lt_tsum_measure for the univ version.

[Yury G. Kudryashov]

See also MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint

[Gareth Ma]

! Thanks, this should be useful for the billion other TODOs I have left >:)