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 ConditionallyCompleteLattices).
• 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_biSup, 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.

def partialSups {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) : ℕ →o α

The monotone sequence whose value at n is the supremum of the f m where m ≤ n.

Equations

• partialSups f = { toFun := Nat.rec (f 0) fun (n : ℕ) (a : α) => a ⊔ f (n + 1), monotone' := ⋯ }

@[simp]

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

@[simp]

theorem partialSups_succ {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) (n : ℕ) : (partialSups f) (n + 1) = (partialSups f) n ⊔ f (n + 1)

theorem partialSups_iff_forall {α : Type u_1} [SemilatticeSup α] {f : ℕ → α} (p : α → Prop) (hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b) {n : ℕ} : p ((partialSups f) n) ↔ ∀ k ≤ n, p (f k)

@[simp]

theorem partialSups_le_iff {α : Type u_1} [SemilatticeSup α] {f : ℕ → α} {n : ℕ} {a : α} : (partialSups f) n ≤ a ↔ ∀ k ≤ n, f k ≤ a

theorem le_partialSups_of_le {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) {m : ℕ} {n : ℕ} (h : m ≤ n) : f m ≤ (partialSups f) n

theorem le_partialSups {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) : f ≤ ⇑(partialSups f)

theorem partialSups_le {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) (n : ℕ) (a : α) (w : ∀ m ≤ n, f m ≤ a) : (partialSups f) n ≤ a

@[simp]

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

@[simp]

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

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

theorem partialSups_mono {α : Type u_1} [SemilatticeSup α] : Monotone partialSups

theorem partialSups_monotone {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) : Monotone ⇑(partialSups f)

def partialSups.gi {α : Type u_1} [SemilatticeSup α] : 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 partialSups_eq_sup'_range {α : Type u_1} [SemilatticeSup α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = (Finset.range (n + 1)).sup' ⋯ f

theorem partialSups_apply {ι : Type u_2} {π : ι → Type u_3} [(i : ι) → SemilatticeSup (π i)] (f : ℕ → (i : ι) → π i) (n : ℕ) (i : ι) : (partialSups f) n i = (partialSups fun (x : ℕ) => f x i) n

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

@[simp]

theorem disjoint_partialSups_left {α : Type u_1} [DistribLattice α] [OrderBot α] {f : ℕ → α} {n : ℕ} {x : α} : Disjoint ((partialSups f) n) x ↔ ∀ k ≤ n, Disjoint (f k) x

@[simp]

theorem disjoint_partialSups_right {α : Type u_1} [DistribLattice α] [OrderBot α] {f : ℕ → α} {n : ℕ} {x : α} : Disjoint x ((partialSups f) n) ↔ ∀ k ≤ n, Disjoint x (f k)

theorem partialSups_disjoint_of_disjoint {α : Type u_1} [DistribLattice α] [OrderBot α] (f : ℕ → α) (h : Pairwise (Disjoint on f)) {m : ℕ} {n : ℕ} (hmn : m < n) : Disjoint ((partialSups f) m) (f n)

theorem partialSups_eq_ciSup_Iic {α : Type u_1} [ConditionallyCompleteLattice α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i

@[simp]

theorem ciSup_partialSups_eq {α : Type u_1} [ConditionallyCompleteLattice α] {f : ℕ → α} (h : BddAbove (Set.range f)) : ⨆ (n : ℕ), (partialSups f) n = ⨆ (n : ℕ), f n

theorem partialSups_eq_biSup {α : Type u_1} [CompleteLattice α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = ⨆ (i : ℕ), ⨆ (_ : i ≤ n), f i

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

theorem iSup_partialSups_eq {α : Type u_1} [CompleteLattice α] (f : ℕ → α) : ⨆ (n : ℕ), (partialSups f) n = ⨆ (n : ℕ), f n

theorem iSup_le_iSup_of_partialSups_le_partialSups {α : Type u_1} [CompleteLattice α] {f : ℕ → α} {g : ℕ → α} (h : partialSups f ≤ partialSups g) : ⨆ (n : ℕ), f n ≤ ⨆ (n : ℕ), g n

theorem iSup_eq_iSup_of_partialSups_eq_partialSups {α : Type u_1} [CompleteLattice α] {f : ℕ → α} {g : ℕ → α} (h : partialSups f = partialSups g) : ⨆ (n : ℕ), f n = ⨆ (n : ℕ), g n