The monotone sequence of partial supremums of a sequence

For ι a preorder in which all bounded-above intervals are finite (such as ℕ), and α a ⊔-semilattice, we define partialSups : (ι → α) → ι →o α by the formula partialSups f i = (Finset.Iic i).sup' ⋯ f, where the ⋯ denotes a proof that Finset.Iic i is nonempty. This is a way of spelling ⊔ k ≤ i, f k which does not require a α to have a bottom element, and makes sense in conditionally-complete lattices (where indexed suprema over sets are badly-behaved).

Under stronger hypotheses on α and ι, we show that this coincides with other candidate definitions, see e.g. partialSups_eq_biSup, partialSups_eq_sup_range, and partialSups_eq_sup'_range.

We show this construction gives a Galois insertion between functions ι → α and monotone functions ι →o α, see partialSups.gi.

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 i ↦ (Finset.Iio i).sup f is already effectively the sequence starting at ⊥.
• If we started at ⊥ we wouldn't have the Galois insertion. See partialSups.gi.

def partialSups {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : ι →o α

The monotone sequence whose value at i is the supremum of the f j where j ≤ i.

Equations

• partialSups f = { toFun := fun (i : ι) => (Finset.Iic i).sup' ⋯ f, monotone' := ⋯ }

theorem partialSups_apply {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) : (partialSups f) i = (Finset.Iic i).sup' ⋯ f

theorem partialSups_iff_forall {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] {f : ι → α} (p : α → Prop) (hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b) {i : ι} : p ((partialSups f) i) ↔ ∀ j ≤ i, p (f j)

@[simp]

theorem partialSups_le_iff {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] {f : ι → α} {i : ι} {a : α} : (partialSups f) i ≤ a ↔ ∀ j ≤ i, f j ≤ a

theorem le_partialSups_of_le {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) {i j : ι} (h : i ≤ j) : f i ≤ (partialSups f) j

theorem le_partialSups {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : f ≤ ⇑(partialSups f)

theorem partialSups_le {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) (a : α) (w : ∀ j ≤ i, f j ≤ a) : (partialSups f) i ≤ a

@[simp]

theorem upperBounds_range_partialSups {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : upperBounds (Set.range ⇑(partialSups f)) = upperBounds (Set.range f)

@[simp]

theorem bddAbove_range_partialSups {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] {f : ι → α} : BddAbove (Set.range ⇑(partialSups f)) ↔ BddAbove (Set.range f)

theorem Monotone.partialSups_eq {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] {f : ι → α} (hf : Monotone f) : ⇑(partialSups f) = f

theorem partialSups_mono {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] : Monotone partialSups

theorem partialSups_monotone {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : Monotone ⇑(partialSups f)

def partialSups.gi {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] : GaloisInsertion partialSups DFunLike.coe

partialSups forms a Galois insertion with the coercion from monotone functions to functions.

Equations

• partialSups.gi = { choice := fun (f : ι → α) (h : ⇑(partialSups f) ≤ f) => { toFun := f, monotone' := ⋯ }, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

theorem Pi.partialSups_apply {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] {τ : Type u_3} {π : τ → Type u_4} [(t : τ) → SemilatticeSup (π t)] (f : ι → (t : τ) → π t) (i : ι) (t : τ) : (partialSups f) i t = (partialSups fun (x : ι) => f x t) i

@[simp]

theorem partialSups_succ {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] (f : ι → α) (i : ι) : (partialSups f) (Order.succ i) = (partialSups f) i ⊔ f (Order.succ i)

@[simp]

theorem partialSups_bot {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [PartialOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] (f : ι → α) : (partialSups f) ⊥ = f ⊥

Functions out of ℕ

@[simp]

theorem partialSups_zero {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) : (partialSups f) 0 = f 0

theorem partialSups_eq_sup'_range {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = (Finset.range (n + 1)).sup' ⋯ f

theorem partialSups_eq_sup_range {α : Type u_1} [SemilatticeSup α] [OrderBot α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = (Finset.range (n + 1)).sup f

Functions valued in a distributive lattice

These lemmas require the target to be a distributive lattice, so they are not useful (or true) in situations such as submodules.

@[simp]

theorem disjoint_partialSups_left {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [DistribLattice α] [OrderBot α] {f : ι → α} {i : ι} {x : α} : Disjoint ((partialSups f) i) x ↔ ∀ j ≤ i, Disjoint (f j) x

@[simp]

theorem disjoint_partialSups_right {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [DistribLattice α] [OrderBot α] {f : ι → α} {i : ι} {x : α} : Disjoint x ((partialSups f) i) ↔ ∀ j ≤ i, Disjoint x (f j)

theorem partialSups_disjoint_of_disjoint {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [DistribLattice α] [OrderBot α] (f : ι → α) (h : Pairwise (Function.onFun Disjoint f)) {i j : ι} (hij : i < j) : Disjoint ((partialSups f) i) (f j)

Lemmas about the supremum over the whole domain

These lemmas require some completeness assumptions on the target space.

theorem partialSups_eq_ciSup_Iic {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [ConditionallyCompleteLattice α] (f : ι → α) (i : ι) : (partialSups f) i = ⨆ (i_1 : ↑(Set.Iic i)), f ↑i_1

@[simp]

theorem ciSup_partialSups_eq {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [ConditionallyCompleteLattice α] {f : ι → α} (h : BddAbove (Set.range f)) : ⨆ (i : ι), (partialSups f) i = ⨆ (i : ι), f i

@[simp]

theorem ciSup_partialSups_eq' {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [ConditionallyCompleteLinearOrder α] (f : ι → α) : ⨆ (i : ι), (partialSups f) i = ⨆ (i : ι), f i

Version of ciSup_partialSups_eq without boundedness assumptions, but requiring a ConditionallyCompleteLinearOrder rather than just a ConditionallyCompleteLattice.

theorem iSup_partialSups_eq {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [CompleteLattice α] (f : ι → α) : ⨆ (i : ι), (partialSups f) i = ⨆ (i : ι), f i

Version of ciSup_partialSups_eq without boundedness assumptions, but requiring a CompleteLattice rather than just a ConditionallyCompleteLattice.

theorem partialSups_eq_biSup {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [CompleteLattice α] (f : ι → α) (i : ι) : (partialSups f) i = ⨆ (j : ι), ⨆ (_ : j ≤ i), f j

theorem iSup_le_iSup_of_partialSups_le_partialSups {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [CompleteLattice α] {f g : ι → α} (h : partialSups f ≤ partialSups g) : ⨆ (i : ι), f i ≤ ⨆ (i : ι), g i

theorem iSup_eq_iSup_of_partialSups_eq_partialSups {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [CompleteLattice α] {f g : ι → α} (h : partialSups f = partialSups g) : ⨆ (i : ι), f i = ⨆ (i : ι), g i

Functions into Set α

theorem partialSups_eq_sUnion_image {α : Type u_1} [DecidableEq (Set α)] (s : ℕ → Set α) (n : ℕ) : (partialSups s) n = ⋃₀ ↑(Finset.image s (Finset.range (n + 1)))

theorem partialSups_eq_biUnion_range {α : Type u_1} (s : ℕ → Set α) (n : ℕ) : (partialSups s) n = ⋃ i ∈ Finset.range (n + 1), s i