mathlib3 documentation

order.partial_sups

The monotone sequence of partial supremums of a sequence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define partial_sups : (ℕ → α) → ℕ →o α inductively. For f : ℕ → α, partial_sups 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 conditionally_complete_lattices).
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 partial_sups_eq_bsupr, partial_sups_eq_sup_range, partial_sups_eq_sup'_range and 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.
λ 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 partial_sups.gi.

TODO #

One could generalize partial_sups to any locally finite bot preorder domain, in place of ℕ. Necessary for the TODO in the module docstring of order.disjointed.

def partial_sups {α : Type u_1} [semilattice_sup α] (f : ℕ → α) :

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

Equations

partial_sups f = {to_fun := nat.rec (f 0) (λ (n : ℕ) (a : α), a ⊔ f (n + 1)), monotone' := _}

@[simp]

theorem partial_sups_zero {α : Type u_1} [semilattice_sup α] (f : ℕ → α) :

⇑(partial_sups f) 0 = f 0

@[simp]

theorem partial_sups_succ {α : Type u_1} [semilattice_sup α] (f : ℕ → α) (n : ℕ) :

⇑(partial_sups f) (n + 1) = ⇑(partial_sups f) n ⊔ f (n + 1)

theorem le_partial_sups_of_le {α : Type u_1} [semilattice_sup α] (f : ℕ → α) {m n : ℕ} (h : m ≤ n) :

f m ≤ ⇑(partial_sups f) n

theorem le_partial_sups {α : Type u_1} [semilattice_sup α] (f : ℕ → α) :

f ≤ ⇑(partial_sups f)

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

⇑(partial_sups f) n ≤ a

@[simp]

theorem bdd_above_range_partial_sups {α : Type u_1} [semilattice_sup α] {f : ℕ → α} :

bdd_above (set.range ⇑(partial_sups f)) ↔ bdd_above (set.range f)

theorem monotone.partial_sups_eq {α : Type u_1} [semilattice_sup α] {f : ℕ → α} (hf : monotone f) :

⇑(partial_sups f) = f

theorem partial_sups_mono {α : Type u_1} [semilattice_sup α] :

monotone partial_sups

def partial_sups.gi {α : Type u_1} [semilattice_sup α] :

galois_insertion partial_sups coe_fn

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

Equations

partial_sups.gi = {choice := λ (f : ℕ → α) (h : ⇑(partial_sups f) ≤ f), {to_fun := f, monotone' := _}, gc := _, le_l_u := _, choice_eq := _}

theorem partial_sups_eq_sup'_range {α : Type u_1} [semilattice_sup α] (f : ℕ → α) (n : ℕ) :

⇑(partial_sups f) n = (finset.range (n + 1)).sup' _ f

theorem partial_sups_eq_sup_range {α : Type u_1} [semilattice_sup α] [order_bot α] (f : ℕ → α) (n : ℕ) :

⇑(partial_sups f) n = (finset.range (n + 1)).sup f

theorem partial_sups_disjoint_of_disjoint {α : Type u_1} [distrib_lattice α] [order_bot α] (f : ℕ → α) (h : pairwise (disjoint on f)) {m n : ℕ} (hmn : m < n) :

disjoint (⇑(partial_sups f) m) (f n)

theorem partial_sups_eq_csupr_Iic {α : Type u_1} [conditionally_complete_lattice α] (f : ℕ → α) (n : ℕ) :

⇑(partial_sups f) n = ⨆ (i : ↥(set.Iic n)), f ↑i

@[simp]

theorem csupr_partial_sups_eq {α : Type u_1} [conditionally_complete_lattice α] {f : ℕ → α} (h : bdd_above (set.range f)) :

(⨆ (n : ℕ), ⇑(partial_sups f) n) = ⨆ (n : ℕ), f n

theorem partial_sups_eq_bsupr {α : Type u_1} [complete_lattice α] (f : ℕ → α) (n : ℕ) :

⇑(partial_sups f) n = ⨆ (i : ℕ) (H : i ≤ n), f i

@[simp]

theorem supr_partial_sups_eq {α : Type u_1} [complete_lattice α] (f : ℕ → α) :

(⨆ (n : ℕ), ⇑(partial_sups f) n) = ⨆ (n : ℕ), f n

theorem supr_le_supr_of_partial_sups_le_partial_sups {α : Type u_1} [complete_lattice α] {f g : ℕ → α} (h : partial_sups f ≤ partial_sups g) :

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

theorem supr_eq_supr_of_partial_sups_eq_partial_sups {α : Type u_1} [complete_lattice α] {f g : ℕ → α} (h : partial_sups f = partial_sups g) :

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