feat: When the symmetric difference has finite measure (#12370)

Add the following lemma: is `s` and `t` are two measurable sets such that `s` and `s ∆ t` have finite measures, then so does `t`.



Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -86,7 +86,7 @@ open Set
 open Filter hiding map
 
 open Function MeasurableSpace
-open scoped Classical
+open scoped Classical symmDiff
 open Topology BigOperators Filter ENNReal NNReal Interval MeasureTheory
 
 variable {α β γ δ ι R R' : Type*}
@@ -137,12 +137,10 @@ theorem measure_union_add_inter' (hs : MeasurableSet s) (t : Set α) :
   rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]
 #align measure_theory.measure_union_add_inter' MeasureTheory.measure_union_add_inter'
 
-open scoped symmDiff in
 lemma measure_symmDiff_eq (hs : MeasurableSet s) (ht : MeasurableSet t) :
     μ (s ∆ t) = μ (s \ t) + μ (t \ s) := by
   simpa only [symmDiff_def, sup_eq_union] using measure_union disjoint_sdiff_sdiff (ht.diff hs)
 
-open scoped symmDiff in
 lemma measure_symmDiff_le (s t u : Set α) :
     μ (s ∆ u) ≤ μ (s ∆ t) + μ (t ∆ u) :=
   le_trans (μ.mono <| symmDiff_triangle s t u) (measure_union_le (s ∆ t) (t ∆ u))
@@ -256,6 +254,25 @@ theorem le_measure_diff : μ s₁ - μ s₂ ≤ μ (s₁ \ s₂) :=
 
 #align measure_theory.le_measure_diff MeasureTheory.le_measure_diff
 
+/-- If the measure of the symmetric difference of two sets is finite,
+then one has infinite measure if and only if the other one does. -/
+theorem measure_eq_top_iff_of_symmDiff (hμst : μ (s ∆ t) ≠ ∞) : μ s = ∞ ↔ μ t = ∞ := by
+  suffices h : ∀ u v, μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞
+    from ⟨h s t hμst, h t s (symmDiff_comm s t ▸ hμst)⟩
+  intro u v hμuv hμu
+  by_contra! hμv
+  apply hμuv
+  rw [Set.symmDiff_def, eq_top_iff]
+  calc
+    ∞ = μ u - μ v := (WithTop.sub_eq_top_iff.2 ⟨hμu, hμv⟩).symm
+    _ ≤ μ (u \ v) := le_measure_diff
+    _ ≤ μ (u \ v ∪ v \ u) := measure_mono <| subset_union_left ..
+
+/-- If the measure of the symmetric difference of two sets is finite,
+then one has finite measure if and only if the other one does. -/
+theorem measure_ne_top_iff_of_symmDiff (hμst : μ (s ∆ t) ≠ ∞) : μ s ≠ ∞ ↔ μ t ≠ ∞ :=
+    (measure_eq_top_iff_of_symmDiff hμst).ne
+
 theorem measure_diff_lt_of_lt_add (hs : MeasurableSet s) (hst : s ⊆ t) (hs' : μ s ≠ ∞) {ε : ℝ≥0∞}
     (h : μ t < μ s + ε) : μ (t \ s) < ε := by
   rw [measure_diff hst hs hs']; rw [add_comm] at h