From 9a750ff308d5b4de96542d406f5c8ad4500e7af0 Mon Sep 17 00:00:00 2001 From: arienmalec Date: Wed, 25 Jan 2023 09:27:09 +0000 Subject: [PATCH] feat: port Order.PartialSups (#1757) port of order.partial.sups Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Johan Commelin --- Mathlib.lean | 1 + Mathlib/Algebra/Tropical/BigOperators.lean | 4 +- Mathlib/Data/Set/Finite.lean | 8 +- .../ConditionallyCompleteLattice/Finset.lean | 22 +- Mathlib/Order/PartialSups.lean | 196 ++++++++++++++++++ 5 files changed, 214 insertions(+), 17 deletions(-) create mode 100644 Mathlib/Order/PartialSups.lean diff --git a/Mathlib.lean b/Mathlib.lean index 246f482a861cd..37535a4723e0d 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -700,6 +700,7 @@ import Mathlib.Order.Monotone.Union import Mathlib.Order.OmegaCompletePartialOrder import Mathlib.Order.OrdContinuous import Mathlib.Order.OrderIsoNat +import Mathlib.Order.PartialSups import Mathlib.Order.PropInstances import Mathlib.Order.RelClasses import Mathlib.Order.RelIso.Basic diff --git a/Mathlib/Algebra/Tropical/BigOperators.lean b/Mathlib/Algebra/Tropical/BigOperators.lean index 6fc9fb981aac0..9b4dc1663c980 100644 --- a/Mathlib/Algebra/Tropical/BigOperators.lean +++ b/Mathlib/Algebra/Tropical/BigOperators.lean @@ -106,7 +106,7 @@ theorem trop_infₛ_image [ConditionallyCompleteLinearOrder R] (s : Finset S) (f trop (infₛ (f '' s)) = ∑ i in s, trop (f i) := by rcases s.eq_empty_or_nonempty with (rfl | h) · simp only [Set.image_empty, coe_empty, sum_empty, WithTop.infₛ_empty, trop_top] - rw [← inf'_eq_cInf_image _ h, inf'_eq_inf, s.trop_inf] + rw [← inf'_eq_cinfₛ_image _ h, inf'_eq_inf, s.trop_inf] #align trop_Inf_image trop_infₛ_image theorem trop_infᵢ [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → WithTop R) : @@ -133,7 +133,7 @@ theorem untrop_sum_eq_infₛ_image [ConditionallyCompleteLinearOrder R] (s : Fin (f : S → Tropical (WithTop R)) : untrop (∑ i in s, f i) = infₛ (untrop ∘ f '' s) := by rcases s.eq_empty_or_nonempty with (rfl | h) · simp only [Set.image_empty, coe_empty, sum_empty, WithTop.infₛ_empty, untrop_zero] - · rw [← inf'_eq_cInf_image _ h, inf'_eq_inf, Finset.untrop_sum'] + · rw [← inf'_eq_cinfₛ_image _ h, inf'_eq_inf, Finset.untrop_sum'] #align untrop_sum_eq_Inf_image untrop_sum_eq_infₛ_image theorem untrop_sum [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → Tropical (WithTop R)) : diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean index 4659b00638615..a8b060598a74e 100644 --- a/Mathlib/Data/Set/Finite.lean +++ b/Mathlib/Data/Set/Finite.lean @@ -1385,17 +1385,17 @@ theorem Finite.supᵢ_binfi_of_antitone {ι ι' α : Type _} [Preorder ι'] [Non @Finite.supᵢ_binfi_of_monotone ι ι'ᵒᵈ α _ _ _ _ _ hs _ fun i hi => (hf i hi).dual_left #align set.finite.supr_binfi_of_antitone Set.Finite.supᵢ_binfi_of_antitone -theorem Finite.infᵢ_bsupr_of_monotone {ι ι' α : Type _} [Preorder ι'] [Nonempty ι'] +theorem Finite.infᵢ_bsupᵢ_of_monotone {ι ι' α : Type _} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) : (⨅ j, ⨆ i ∈ s, f i j) = ⨆ i ∈ s, ⨅ j, f i j := hs.supᵢ_binfi_of_antitone (α := αᵒᵈ) fun i hi => (hf i hi).dual_right -#align set.finite.infi_bsupr_of_monotone Set.Finite.infᵢ_bsupr_of_monotone +#align set.finite.infi_bsupr_of_monotone Set.Finite.infᵢ_bsupᵢ_of_monotone -theorem Finite.infᵢ_bsupr_of_antitone {ι ι' α : Type _} [Preorder ι'] [Nonempty ι'] +theorem Finite.infᵢ_bsupᵢ_of_antitone {ι ι' α : Type _} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) : (⨅ j, ⨆ i ∈ s, f i j) = ⨆ i ∈ s, ⨅ j, f i j := hs.supᵢ_binfi_of_monotone (α := αᵒᵈ) fun i hi => (hf i hi).dual_right -#align set.finite.infi_bsupr_of_antitone Set.Finite.infᵢ_bsupr_of_antitone +#align set.finite.infi_bsupr_of_antitone Set.Finite.infᵢ_bsupᵢ_of_antitone theorem supᵢ_infᵢ_of_monotone {ι ι' α : Type _} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Frame α] {f : ι → ι' → α} (hf : ∀ i, Monotone (f i)) : diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean index 56494558dad86..6c28299e74aa1 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean @@ -87,7 +87,7 @@ non-empty. As a result, we can translate between the two. namespace Finset -theorem sup'_eq_cSup_image [ConditionallyCompleteLattice β] (s : Finset α) (H) (f : α → β) : +theorem sup'_eq_csupₛ_image [ConditionallyCompleteLattice β] (s : Finset α) (H) (f : α → β) : s.sup' H f = supₛ (f '' s) := by apply le_antisymm · refine' Finset.sup'_le _ _ fun a ha => _ @@ -97,20 +97,20 @@ theorem sup'_eq_cSup_image [ConditionallyCompleteLattice β] (s : Finset α) (H) · apply csupₛ_le ((coe_nonempty.mpr H).image _) rintro _ ⟨a, ha, rfl⟩ exact Finset.le_sup' _ ha -#align finset.sup'_eq_cSup_image Finset.sup'_eq_cSup_image +#align finset.sup'_eq_cSup_image Finset.sup'_eq_csupₛ_image -theorem inf'_eq_cInf_image [ConditionallyCompleteLattice β] (s : Finset α) (H) (f : α → β) : +theorem inf'_eq_cinfₛ_image [ConditionallyCompleteLattice β] (s : Finset α) (H) (f : α → β) : s.inf' H f = infₛ (f '' s) := - @sup'_eq_cSup_image _ βᵒᵈ _ _ H _ -#align finset.inf'_eq_cInf_image Finset.inf'_eq_cInf_image + @sup'_eq_csupₛ_image _ βᵒᵈ _ _ H _ +#align finset.inf'_eq_cInf_image Finset.inf'_eq_cinfₛ_image -theorem sup'_id_eq_cSup [ConditionallyCompleteLattice α] (s : Finset α) (H) : - s.sup' H id = supₛ s := by rw [sup'_eq_cSup_image s H, Set.image_id] -#align finset.sup'_id_eq_cSup Finset.sup'_id_eq_cSup +theorem sup'_id_eq_csupₛ [ConditionallyCompleteLattice α] (s : Finset α) (H) : + s.sup' H id = supₛ s := by rw [sup'_eq_csupₛ_image s H, Set.image_id] +#align finset.sup'_id_eq_cSup Finset.sup'_id_eq_csupₛ -theorem inf'_id_eq_cInf [ConditionallyCompleteLattice α] (s : Finset α) (H) : +theorem inf'_id_eq_cinfₛ [ConditionallyCompleteLattice α] (s : Finset α) (H) : s.inf' H id = infₛ s := - @sup'_id_eq_cSup αᵒᵈ _ _ H -#align finset.inf'_id_eq_cInf Finset.inf'_id_eq_cInf + @sup'_id_eq_csupₛ αᵒᵈ _ _ H +#align finset.inf'_id_eq_cInf Finset.inf'_id_eq_cinfₛ end Finset diff --git a/Mathlib/Order/PartialSups.lean b/Mathlib/Order/PartialSups.lean new file mode 100644 index 0000000000000..ac3d2bc5cf206 --- /dev/null +++ b/Mathlib/Order/PartialSups.lean @@ -0,0 +1,196 @@ +/- +Copyright (c) 2021 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison + +! This file was ported from Lean 3 source module order.partial_sups +! leanprover-community/mathlib commit d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Data.Finset.Lattice +import Mathlib.Order.Hom.Basic +import Mathlib.Order.ConditionallyCompleteLattice.Finset + +/-! +# The monotone sequence of partial supremums of a sequence + +We define `partialSups : (ℕ → α) → ℕ →o α` inductively. For `f : ℕ → α`, `partialSups f` is +the sequence `f 0 `, `f 0 ⊔ f 1`, `f 0 ⊔ f 1 ⊔ f 2`, ... The point of this definition is that +* it doesn't need a `⨆`, as opposed to `⨆ (i ≤ n), f i` (which also means the wrong thing on + `ConditionallyCompleteLattice`s). +* it doesn't need a `⊥`, as opposed to `(Finset.range (n + 1)).sup f`. +* it avoids needing to prove that `Finset.range (n + 1)` is nonempty to use `Finset.sup'`. + +Equivalence with those definitions is shown by `partialSups_eq_bsupᵢ`, `partialSups_eq_sup_range`, +and `partialSups_eq_sup'_range` respectively. + +## Notes + +One might dispute whether this sequence should start at `f 0` or `⊥`. We choose the former because : +* Starting at `⊥` requires... having a bottom element. +* `fun f n ↦ (Finset.range n).sup f` is already effectively the sequence starting at `⊥`. +* If we started at `⊥` we wouldn't have the Galois insertion. See `partialSups.gi`. + +## TODO + +One could generalize `partialSups` to any locally finite bot preorder domain, in place of `ℕ`. +Necessary for the TODO in the module docstring of `Order.disjointed`. +-/ + + +variable {α : Type _} + +section SemilatticeSup + +variable [SemilatticeSup α] + +/-- The monotone sequence whose value at `n` is the supremum of the `f m` where `m ≤ n`. -/ +def partialSups (f : ℕ → α) : ℕ →o α := + ⟨@Nat.rec (fun _ => α) (f 0) fun (n : ℕ) (a : α) => a ⊔ f (n + 1), + monotone_nat_of_le_succ fun _ => le_sup_left⟩ +#align partial_sups partialSups + +@[simp] +theorem partialSups_zero (f : ℕ → α) : partialSups f 0 = f 0 := + rfl +#align partial_sups_zero partialSups_zero + +@[simp] +theorem partialSups_succ (f : ℕ → α) (n : ℕ) : + partialSups f (n + 1) = partialSups f n ⊔ f (n + 1) := + rfl +#align partial_sups_succ partialSups_succ + +theorem le_partialSups_of_le (f : ℕ → α) {m n : ℕ} (h : m ≤ n) : f m ≤ partialSups f n := by + induction' n with n ih + · rw [nonpos_iff_eq_zero.mp h, partialSups_zero] + · cases' h with h h + · exact le_sup_right + · exact (ih h).trans le_sup_left +#align le_partial_sups_of_le le_partialSups_of_le + +theorem le_partialSups (f : ℕ → α) : f ≤ partialSups f := fun _n => le_partialSups_of_le f le_rfl +#align le_partial_sups le_partialSups + +theorem partialSups_le (f : ℕ → α) (n : ℕ) (a : α) (w : ∀ m, m ≤ n → f m ≤ a) : + partialSups f n ≤ a := by + induction' n with n ih + · apply w 0 le_rfl + · exact sup_le (ih fun m p => w m (Nat.le_succ_of_le p)) (w (n + 1) le_rfl) +#align partial_sups_le partialSups_le + +@[simp] +theorem bddAbove_range_partialSups {f : ℕ → α} : + BddAbove (Set.range (partialSups f)) ↔ BddAbove (Set.range f) := by + apply exists_congr fun a => _ + intro a + constructor + · rintro h b ⟨i, rfl⟩ + exact (le_partialSups _ _).trans (h (Set.mem_range_self i)) + · rintro h b ⟨i, rfl⟩ + exact partialSups_le _ _ _ fun _ _ => h (Set.mem_range_self _) +#align bdd_above_range_partial_sups bddAbove_range_partialSups + +theorem Monotone.partialSups_eq {f : ℕ → α} (hf : Monotone f) : (partialSups f : ℕ → α) = f := by + ext n + induction' n with n ih + · rfl + · rw [partialSups_succ, ih, sup_eq_right.2 (hf (Nat.le_succ _))] +#align monotone.partial_sups_eq Monotone.partialSups_eq + +theorem partialSups_mono : Monotone (partialSups : (ℕ → α) → ℕ →o α) := by + rintro f g h n + induction' n with n ih + · exact h 0 + · exact sup_le_sup ih (h _) +#align partial_sups_mono partialSups_mono + +/-- `partialSups` forms a Galois insertion with the coercion from monotone functions to functions. +-/ +def partialSups.gi : GaloisInsertion (partialSups : (ℕ → α) → ℕ →o α) (↑) where + choice f h := + ⟨f, by convert (partialSups f).monotone; exact (le_partialSups f).antisymm h⟩ + gc f g := by + refine' ⟨(le_partialSups f).trans, fun h => _⟩ + convert partialSups_mono h + exact OrderHom.ext _ _ g.monotone.partialSups_eq.symm + le_l_u f := le_partialSups f + choice_eq f h := OrderHom.ext _ _ ((le_partialSups f).antisymm h) +#align partial_sups.gi partialSups.gi + +theorem partialSups_eq_sup'_range (f : ℕ → α) (n : ℕ) : + partialSups f n = (Finset.range (n + 1)).sup' ⟨n, Finset.self_mem_range_succ n⟩ f := by + induction' n with n ih + · simp + · dsimp [partialSups] at ih⊢ + simp_rw [@Finset.range_succ n.succ] + rw [ih, Finset.sup'_insert, sup_comm] +#align partial_sups_eq_sup'_range partialSups_eq_sup'_range + +end SemilatticeSup + +theorem partialSups_eq_sup_range [SemilatticeSup α] [OrderBot α] (f : ℕ → α) (n : ℕ) : + partialSups f n = (Finset.range (n + 1)).sup f := by + induction' n with n ih + · simp + · dsimp [partialSups] at ih⊢ + rw [Finset.range_succ, Finset.sup_insert, sup_comm, ih] +#align partial_sups_eq_sup_range partialSups_eq_sup_range + +/- Note this lemma requires a distributive lattice, so is not useful (or true) in situations such as +submodules. -/ +theorem partialSups_disjoint_of_disjoint [DistribLattice α] [OrderBot α] (f : ℕ → α) + (h : Pairwise (Disjoint on f)) {m n : ℕ} (hmn : m < n) : Disjoint (partialSups f m) (f n) := by + induction' m with m ih + · exact h hmn.ne + · rw [partialSups_succ, disjoint_sup_left] + exact ⟨ih (Nat.lt_of_succ_lt hmn), h hmn.ne⟩ +#align partial_sups_disjoint_of_disjoint partialSups_disjoint_of_disjoint + +section ConditionallyCompleteLattice + +variable [ConditionallyCompleteLattice α] + +theorem partialSups_eq_csupᵢ_Iic (f : ℕ → α) (n : ℕ) : partialSups f n = ⨆ i : Set.Iic n, f i := by + have : Set.Iio (n + 1) = Set.Iic n := Set.ext fun _ => Nat.lt_succ_iff + rw [partialSups_eq_sup'_range, Finset.sup'_eq_csupₛ_image, Finset.coe_range, supᵢ, this] + simp only [Set.range, Subtype.exists, Set.mem_Iic, exists_prop, (· '' ·)] +#align partial_sups_eq_csupr_Iic partialSups_eq_csupᵢ_Iic + +@[simp] +theorem csupᵢ_partialSups_eq {f : ℕ → α} (h : BddAbove (Set.range f)) : + (⨆ n, partialSups f n) = ⨆ n, f n := by + refine' (csupᵢ_le fun n => _).antisymm (csupᵢ_mono _ <| le_partialSups f) + · rw [partialSups_eq_csupᵢ_Iic] + exact csupᵢ_le fun i => le_csupᵢ h _ + · rwa [bddAbove_range_partialSups] +#align csupr_partial_sups_eq csupᵢ_partialSups_eq + +end ConditionallyCompleteLattice + +section CompleteLattice + +variable [CompleteLattice α] + +theorem partialSups_eq_bsupᵢ (f : ℕ → α) (n : ℕ) : partialSups f n = ⨆ i ≤ n, f i := by + simpa only [supᵢ_subtype] using partialSups_eq_csupᵢ_Iic f n +#align partial_sups_eq_bsupr partialSups_eq_bsupᵢ + +-- Porting note: simp can prove this @[simp] +theorem supᵢ_partialSups_eq (f : ℕ → α) : (⨆ n, partialSups f n) = ⨆ n, f n := + csupᵢ_partialSups_eq <| OrderTop.bddAbove _ +#align supr_partial_sups_eq supᵢ_partialSups_eq + +theorem supᵢ_le_supᵢ_of_partialSups_le_partialSups {f g : ℕ → α} + (h : partialSups f ≤ partialSups g) : (⨆ n, f n) ≤ ⨆ n, g n := by + rw [← supᵢ_partialSups_eq f, ← supᵢ_partialSups_eq g] + exact supᵢ_mono h +#align supr_le_supr_of_partial_sups_le_partial_sups supᵢ_le_supᵢ_of_partialSups_le_partialSups + +theorem supᵢ_eq_supᵢ_of_partialSups_eq_partialSups {f g : ℕ → α} + (h : partialSups f = partialSups g) : (⨆ n, f n) = ⨆ n, g n := by + simp_rw [← supᵢ_partialSups_eq f, ← supᵢ_partialSups_eq g, h] +#align supr_eq_supr_of_partial_sups_eq_partial_sups supᵢ_eq_supᵢ_of_partialSups_eq_partialSups + +end CompleteLattice