refactor(Order/Disjointed): allow arbitrary partial orders as domain (#20545)

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: 3 people

Mathlib.lean

@@ -680,6 +680,7 @@ import Mathlib.Algebra.Order.CauSeq.BigOperators
 import Mathlib.Algebra.Order.CauSeq.Completion
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Algebra.Order.CompleteField
+import Mathlib.Algebra.Order.Disjointed
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Field.Canonical
 import Mathlib.Algebra.Order.Field.Defs

Mathlib/Algebra/Order/Disjointed.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2025 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+import Mathlib.Algebra.Order.PartialSups
+import Mathlib.Data.Nat.SuccPred
+import Mathlib.Order.Disjointed
+
+/-!
+# `Disjointed` for functions on a `SuccAddOrder`
+
+This file contains material excised from `Mathlib.Order.Disjointed` to avoid import dependencies
+from `Mathlib.Algebra.Order` into `Mathlib.Order`.
+
+## TODO
+
+Find a useful statement of `disjointedRec_succ`.
+-/
+
+open Order
+
+variable {α ι : Type*} [GeneralizedBooleanAlgebra α]
+
+section SuccAddOrder
+
+variable [LinearOrder ι] [LocallyFiniteOrderBot ι] [Add ι] [One ι] [SuccAddOrder ι]
+
+theorem disjointed_add_one [NoMaxOrder ι] (f : ι → α) (i : ι) :
+    disjointed f (i + 1) = f (i + 1) \ partialSups f i := by
+  simpa only [succ_eq_add_one] using disjointed_succ f (not_isMax i)
+
+protected lemma Monotone.disjointed_add_one_sup {f : ι → α} (hf : Monotone f) (i : ι) :
+    disjointed f (i + 1) ⊔ f i = f (i + 1) := by
+  simpa only [succ_eq_add_one i] using hf.disjointed_succ_sup i
+
+protected lemma Monotone.disjointed_add_one [NoMaxOrder ι]  {f : ι → α} (hf : Monotone f) (i : ι) :
+    disjointed f (i + 1) = f (i + 1) \ f i := by
+  rw [← succ_eq_add_one, hf.disjointed_succ]
+  exact not_isMax i
+
+end SuccAddOrder
+
+section Nat
+
+/-- A recursion principle for `disjointed`. To construct / define something for `disjointed f i`,
+it's enough to construct / define it for `f n` and to able to extend through diffs.
+
+Note that this version allows an arbitrary `Sort*`, but requires the domain to be `Nat`, while
+the root-level `disjointedRec` allows more general domains but requires `p` to be `Prop`-valued. -/
+def Nat.disjointedRec {f : ℕ → α} {p : α → Sort*} (hdiff : ∀ ⦃t i⦄, p t → p (t \ f i)) :
+    ∀ ⦃n⦄, p (f n) → p (disjointed f n)
+  | 0 => fun h₀ ↦ disjointed_zero f ▸ h₀
+  | n + 1 => fun h => by
+    suffices H : ∀ k, p (f (n + 1) \ partialSups f k) from disjointed_add_one f n ▸ H n
+    intro k
+    induction k with
+    | zero => exact hdiff h
+    | succ k ih => simpa only [partialSups_add_one, ← sdiff_sdiff_left] using hdiff ih
+
+@[simp]
+theorem disjointedRec_zero {f : ℕ → α} {p : α → Sort*}
+    (hdiff : ∀ ⦃t i⦄, p t → p (t \ f i)) (h₀ : p (f 0)) :
+    Nat.disjointedRec hdiff h₀ = (disjointed_zero f ▸ h₀) :=
+  rfl
+
+-- TODO: Find a useful statement of `disjointedRec_succ`.
+
+end Nat

Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean

@@ -72,6 +72,18 @@ theorem isCaratheodory_union (h₁ : IsCaratheodory m s₁) (h₂ : IsCaratheodo
     union_diff_left, h₂ (t ∩ s₁)]
   simp [diff_eq, add_assoc]
 
+variable {m} in
+lemma IsCaratheodory.biUnion_of_finite {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Finite)
+    (h : ∀ i ∈ t, m.IsCaratheodory (s i)) :
+    m.IsCaratheodory (⋃ i ∈ t, s i) := by
+  classical
+  lift t to Finset ι using ht
+  induction t using Finset.induction_on with
+  | empty => simp
+  | @insert i t hi IH =>
+    simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
+    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)
+
 theorem measure_inter_union (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : IsCaratheodory m s₁) {t : Set α} :
     m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂) := by
   rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]
@@ -93,17 +105,16 @@ theorem isCaratheodory_inter (h₁ : IsCaratheodory m s₁) (h₂ : IsCaratheodo
 lemma isCaratheodory_diff (h₁ : IsCaratheodory m s₁) (h₂ : IsCaratheodory m s₂) :
     IsCaratheodory m (s₁ \ s₂) := m.isCaratheodory_inter h₁ (m.isCaratheodory_compl h₂)
 
-lemma isCaratheodory_partialSups {s : ℕ → Set α} (h : ∀ i, m.IsCaratheodory (s i)) (i : ℕ) :
+lemma isCaratheodory_partialSups {ι : Type*} [PartialOrder ι] [LocallyFiniteOrderBot ι]
+    {s : ι → Set α} (h : ∀ i, m.IsCaratheodory (s i)) (i : ι) :
     m.IsCaratheodory (partialSups s i) := by
-  induction i with
-  | zero => exact h 0
-  | succ i hi => exact partialSups_add_one s i ▸ m.isCaratheodory_union hi (h (i + 1))
-
-lemma isCaratheodory_disjointed {s : ℕ → Set α} (h : ∀ i, m.IsCaratheodory (s i)) (i : ℕ) :
-    m.IsCaratheodory (disjointed s i) := by
-  induction i with
-  | zero => exact h 0
-  | succ i _ => exact m.isCaratheodory_diff (h (i + 1)) (m.isCaratheodory_partialSups h i)
+  simpa only [partialSups_apply, Finset.sup'_eq_sup, Finset.sup_set_eq_biUnion, ← Finset.mem_coe,
+    Finset.coe_Iic] using .biUnion_of_finite (finite_Iic _) (fun j _ ↦ h j)
+
+lemma isCaratheodory_disjointed {ι : Type*} [PartialOrder ι] [LocallyFiniteOrderBot ι]
+    {s : ι → Set α} (h : ∀ i, m.IsCaratheodory (s i)) (i : ι) :
+    m.IsCaratheodory (disjointed s i) :=
+  disjointedRec (fun _ j ht ↦ m.isCaratheodory_diff ht <| h j) (h i)
 
 theorem isCaratheodory_sum {s : ℕ → Set α} (h : ∀ i, IsCaratheodory m (s i))
     (hd : Pairwise (Disjoint on s)) {t : Set α} :

Mathlib/MeasureTheory/SetSemiring.lean

@@ -321,16 +321,25 @@ lemma biInter_mem {ι : Type*} (hC : IsSetRing C) {s : ι → Set α}
     refine hC.inter_mem hs.1 ?_
     exact h (fun n hnS ↦ hs.2 n hnS)
 
-lemma partialSups_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n ∈ C) (n : ℕ) :
+lemma finsetSup_mem (hC : IsSetRing C) {ι : Type*} {s : ι → Set α} {t : Finset ι}
+    (hs : ∀ i ∈ t, s i ∈ C) :
+    t.sup s ∈ C := by
+  classical
+  induction t using Finset.induction_on with
+  | empty => exact hC.empty_mem
+  | @insert m t hm ih =>
+    simpa only [sup_insert] using
+      hC.union_mem (hs m <| mem_insert_self m t) (ih <| fun i hi ↦ hs _ <| mem_insert_of_mem hi)
+
+lemma partialSups_mem {ι : Type*} [Preorder ι] [LocallyFiniteOrderBot ι]
+    (hC : IsSetRing C) {s : ι → Set α} (hs : ∀ n, s n ∈ C) (n : ι) :
     partialSups s n ∈ C := by
-  rw [partialSups_eq_biUnion_range]
-  exact hC.biUnion_mem _ (fun n _ ↦ hs n)
-
-lemma disjointed_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n ∈ C) (n : ℕ) :
-    disjointed s n ∈ C := by
-  cases n with
-  | zero => exact hs 0
-  | succ n => exact hC.diff_mem (hs n.succ) (hC.partialSups_mem hs n)
+  simpa only [partialSups_apply, sup'_eq_sup] using hC.finsetSup_mem (fun i hi ↦ hs i)
+
+lemma disjointed_mem {ι : Type*} [Preorder ι] [LocallyFiniteOrderBot ι]
+    (hC : IsSetRing C) {s : ι → Set α} (hs : ∀ j, s j ∈ C) (i : ι) :
+    disjointed s i ∈ C :=
+  disjointedRec (fun _ j ht ↦ hC.diff_mem ht <| hs j) (hs i)
 
 end IsSetRing