Documentation

Mathlib.Order.PartialSups

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_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.

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

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' := (_ : Monotone (Nat.rec (f 0) fun n a => a ⊔ f (n + 1))) }

@[simp]

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

↑(partialSups f) 0 = f 0

@[simp]

theorem partialSups_succ {α : Type u_1} [inst : SemilatticeSup α] (f : ℕ → α) (n : ℕ) :

↑(partialSups f) (n + 1) = ↑(partialSups f) n ⊔ f (n + 1)

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

f m ≤ ↑(partialSups f) n

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

f ≤ ↑(partialSups f)

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

↑(partialSups f) n ≤ a

@[simp]

theorem bddAbove_range_partialSups {α : Type u_1} [inst : SemilatticeSup α] {f : ℕ → α} :

BddAbove (Set.range ↑(partialSups f)) ↔ BddAbove (Set.range f)

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

↑(partialSups f) = f

theorem partialSups_mono {α : Type u_1} [inst : SemilatticeSup α] :

Monotone partialSups

def partialSups.gi {α : Type u_1} [inst : SemilatticeSup α] :

GaloisInsertion partialSups OrderHom.toFun

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

Equations

One or more equations did not get rendered due to their size.

theorem partialSups_eq_sup'_range {α : Type u_1} [inst : SemilatticeSup α] (f : ℕ → α) (n : ℕ) :

↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f

theorem partialSups_eq_sup_range {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (f : ℕ → α) (n : ℕ) :

↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f

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

Disjoint (↑(partialSups f) m) (f n)

theorem partialSups_eq_csupᵢ_Iic {α : Type u_1} [inst : ConditionallyCompleteLattice α] (f : ℕ → α) (n : ℕ) :

↑(partialSups f) n = ⨆ i, f ↑i

@[simp]

theorem csupᵢ_partialSups_eq {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : ℕ → α} (h : BddAbove (Set.range f)) :

(⨆ n, ↑(partialSups f) n) = ⨆ n, f n

theorem partialSups_eq_bsupᵢ {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) (n : ℕ) :

↑(partialSups f) n = ⨆ i, ⨆ h, f i

theorem supᵢ_partialSups_eq {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) :

(⨆ n, ↑(partialSups f) n) = ⨆ n, f n

theorem supᵢ_le_supᵢ_of_partialSups_le_partialSups {α : Type u_1} [inst : CompleteLattice α] {f : ℕ → α} {g : ℕ → α} (h : partialSups f ≤ partialSups g) :

(⨆ n, f n) ≤ ⨆ n, g n

theorem supᵢ_eq_supᵢ_of_partialSups_eq_partialSups {α : Type u_1} [inst : CompleteLattice α] {f : ℕ → α} {g : ℕ → α} (h : partialSups f = partialSups g) :

(⨆ n, f n) = ⨆ n, g n