the sequence of partial supremums

Stream: general

[Scott Morrison]

I've recently wanted some API to talk about the sequence of partial supremums of a function f : ℕ → α for [semilattice_sup_bot α].

One alternative is to just use (finset.range n).sup f, but I found that it was nicer if I just made a new definition and proved some API about it, but I'm left feeling uncertain whether it is API-for-its-own-sake or actually useful. Any advice on whether we want the following:

variables {α : Type*}

/-- The monotone sequence of supremums of the first `n` elements of a sequence. -/
def partial_sups [semilattice_sup_bot α] (f : ℕ → α) : ℕ →ₘ α :=
⟨nat.rec ⊥ (λ (n : ℕ) (a : α), a ⊔ f n), monotone_of_monotone_nat (λ n, le_sup_left)⟩

@[simp] lemma partial_sups_zero [semilattice_sup_bot α] (f : ℕ → α) : partial_sups f 0 = ⊥ := rfl
@[simp] lemma partial_sups_succ [semilattice_sup_bot α] (f : ℕ → α) (n : ℕ) :
  partial_sups f (n+1) = partial_sups f n ⊔ f n := rfl

lemma le_partial_sups [semilattice_sup_bot α] (f : ℕ → α) {m n : ℕ} (h : m < n) :
  f m ≤ partial_sups f n :=
begin
  induction n with n ih,
  { cases h, },
  { cases h with h h,
    { exact le_sup_right, },
    { exact (ih h).trans le_sup_left, } },
end

lemma partial_sups_le [semilattice_sup_bot α] (f : ℕ → α) (n : ℕ)
  (a : α) (w : ∀ m, m < n → f m ≤ a) : partial_sups f n ≤ a :=
begin
  induction n with n ih,
  { apply bot_le, },
  { exact sup_le (ih (λ m p, w m (nat.lt.step p))) (w n (lt_add_one n))}
end

lemma partial_sups_eq [semilattice_sup_bot α] (f : ℕ → α) (n : ℕ) :
  partial_sups f n = (finset.range n).sup f :=
begin
  induction n with n ih,
  { refl, },
  { dsimp [partial_sups] at ih ⊢,
    rw [finset.range_succ, finset.sup_insert, sup_comm, ih], },
end

-- Note this lemma requires a distributive lattice,
-- so is not useful (or true) in situations such as submodules.
lemma partial_sups_disjoint_of_disjoint [bounded_distrib_lattice α]
  (f : ℕ → α) (w : pairwise (disjoint on f)) {m n : ℕ} (h : m < n) :
  disjoint (partial_sups f m) (f n) :=
begin
  induction m with m ih,
  exact disjoint_bot_left,
  dsimp [partial_sups],
  rw disjoint_sup_left,
  exact ⟨ih (nat.lt_of_succ_lt h), w m n (nat.lt_of_succ_lt h).ne⟩
end

I can avoid using it (I want it for proving that all noetherian rings has the strong rank condition), at the expense of ever-so-slightly-cruftier proofs in my application.

[Kevin Buzzard]

@Kalle Kytölä you might be interested in this. One should perhaps prove partial_sups (f : ℕ →ₘ α) = f. It's probably a Galois insertion.

[Scott Morrison]

I think unfortunately there's an off-by-one error in this additional statement (partial_sups f 0 is always bot).

[Kevin Buzzard]

Then perhaps you should be taking sups over {x <= n}?

[Scott Morrison]

Sure. For my application I only care about "eventually" stuff anyway.

[Kalle Kytölä]

Kevin Buzzard said:

Kalle Kytölä you might be interested in this. One should perhaps prove partial_sups (f : ℕ →ₘ α) = f. It's probably a Galois insertion.

Although I have no concrete use-case right now, I could very well imagine using Scott's definition of partial_sups, those lemmas about it, and perhaps even the statements Kevin suggested about it. But I clearly don't have enough experience to comment one way or the other about Scott's original question of "whether we want the following". (I'd naively just want all good math in mathlib :big_smile:, certainly including this.)

I suppose this came up because of the monotone limits thing. That was just something I stumbled on while playing my own NNG-sequel: the monotone limits lemma was one of the items I wished I had had in one of the boss levels (for the record, I beat that boss, but not without some hiding in corners). Mainly I was surprised not to find that item by library_search/tidy/simp.

I definitely hope to be able to contribute something at some point, but for now I am still at the beginner stage of playing my own first game, to get an idea about what it takes to translate a bit of math to Lean. I will of course tell about that game soon enough (whether you ask for it or not, I'm afraid): either when give up or when I've played it through. But for now I have chosen to shield myself from spoilers by any scary omnipotent formalizers here :smile:. Perhaps it because I'm the kind of person who prefers to bang my head against a wall until the $\& \! \oint \! \star \#$ washing machine works...

[Patrick Massot]

Did you do all the exercises in the tutorial project? The monotone limit thing is definitely there, without any filters.

[Kalle Kytölä]

I checked and apparently I did tutorials 1-6 in February. Seems I didn't do 7-9... I suspect it might be because I found Kevin's course at that point :grinning_face_with_smiling_eyes:.

You are of course right: tutorials 5 has the monotone limit statement for ℝ, even in the completeness axiom form I asked earlier. So I had played through it and forgotten. But even if my memory were better than it is, I think I would prefer to find these is by library_search... This and the right generality was the question. For the right generality, the answers by you and Kevin were most helpful!