Bounded supremum on conditionally_complete_lattice

Stream: maths

[Eric Wieser]

I was hoping to be able to prove:

lemma finset.sup'_eq_csupr [conditionally_complete_lattice β] (s : finset α) (H) (f : α → β) :
  s.sup' H f = (⨆ a ∈ s, f a) :=

However, I'm starting to think it might be false. The problem is that (⨆ a ∈ s, f a) expands to (⨆ a, ⨆ (h : a ∈ s), f a), but ⨆ (h : a ∈ s), f a is not defined when a ∉ s. Am I right then in concluding that ⨆ a ∈ s, f a is completely unusable given conditionally_complete_lattice β and (f : α → β)?

[Eric Wieser]

The best I could do was;

import data.finset.lattice
import order.conditionally_complete_lattice

namespace finset

variables {α : Type*} { β : Type*}

-- `⨆ a ∈ s, f a` means the wrong thing :(
lemma sup'_eq_csupr_subtype [conditionally_complete_lattice β] (s : finset α) (H) (f : α → β) :
  s.sup' H f = (⨆ a : {a // a ∈ s}, f a) :=
begin
  apply le_antisymm,
  { refine (finset.sup'_le _ _ $ λ a ha, _),
    refine @le_csupr _ _ _ (f ∘ coe) ⟨s.sup' H f, _⟩ (⟨a, ha⟩ : subtype _),
    rintros i ⟨j, rfl⟩,
    rw function.comp_app,
    apply finset.le_sup' _ j.prop,
  },
  haveI : nonempty {x // x ∈ s} := H.rec (λ x hx, nonempty.intro $ subtype.mk x hx),
  apply csupr_le,
  exact λ a, finset.le_sup' _ a.prop,
end

end finset

[Eric Wieser]

I guess this is a bit like @Oliver Nash's nested "finprod" thread

[Oliver Nash]

Eric Wieser said:

Am I right then in concluding that ⨆ a ∈ s, f a is completely unusable given conditionally_complete_lattice β and (f : α → β)?

Hmm, I think you're right. I guess the issue is that if there are values a : α such that a ∉ s then for such an a we have ⨆ (H : a ∈ s), f a = Sup ∅ and we know nothing about Sup ∅ so everything becomes a mess.

[Oliver Nash]

So if β has a ⊥ and Sup ∅ = ⊥ then presumably everything is fine but in general there is a problem.

[Oliver Nash]

I _think_ I could use the following to cook up a counterexample to finset.sup'_eq_csupr:

import data.finset.lattice
import order.conditionally_complete_lattice

namespace finset

variables {α : Type*} {β : Type*}

lemma uhoh [conditionally_complete_lattice β] (s : finset α) (a' : α) (hs : a' ∉ s) (f : α → β) :
  set.range (λ (a : α), (⨆ (H : a ∈ s), f a)) = f '' ↑s ⊔ {Sup ∅} :=
begin
  -- Avert your eyes from the horrendous proof below.
  classical,
  have h₁ : ∀ (a : α), (⨆ (H : a ∈ s), f a) = if a ∈ s then f a else Sup ∅,
  { intros a,
    by_cases ha' : a ∈ s,
    { simp [ha'], },
    { simp [ha'], unfold supr, congr,
      apply le_antisymm,
      { intros b hb, simp only [set.mem_range, exists_false_left] at hb, contradiction, },
      { simp only [set.le_eq_subset, set.empty_subset], }, }, },
  have h₂ : set.range (λ (a : α), ite (a ∈ s) (f a) (Sup ∅)) = (f '' s) ⊔ {Sup ∅},
  { simp,
    ext b, split; intros h; simp; simp at h,
    { obtain ⟨a, ha⟩ := h,
      by_cases ha' : a ∈ s,
      { right, use a, finish, },
      { left, finish, }, },
    { cases h,
      { use a', finish, },
      { obtain ⟨a, ha⟩ := h, use a, finish, }, }, },
  simp_rw [h₁, h₂],
end

lemma ohdear [conditionally_complete_lattice β] (s : finset α) (a' : α) (hs : a' ∉ s) (f : α → β) :
  (⨆ a ∈ s, f a) = Sup (f '' ↑s ⊔ {Sup ∅}) :=
by rw [supr, uhoh s a' hs f]

[Oliver Nash]

This might not be a bad time to remind you about #7439 !

[Oliver Nash]

So yeah, this is a bit like my "finprod" thread: I presume it's convenient that supr is always defined for conditionally complete lattices, but appropriate hypotheses are needed in order to get sensible results etc.

[Rémy Degenne]

I had the same issue recently. I was defining the projective (semi)norm on a tensor product, and wrote something of the form ⨅ x (hx : p x), f x for some predicate p and a function with nonnegative real values f. I thought that it would take the infimum of f over those x for which p x, but that's not how it works. It took me 2 hours to realize that it was not at all what I thought: there was always an x for which the property was not true, and my definition was in fact always equal to 0 (due to the default value for Inf being 0 on ℝ). I could prove that it was a seminorm without issues :)
So indeed, the bounded supremum/infimum notation on a conditionally complete lattice did not conform at all to my intuition.

[Eric Wieser]

I ended up stating my lemma as finset.sup'_eq_cSup_image : s.sup' H f = Sup (f '' s) in #7689 to avoid awkwardness with supr

[Eric Wieser]

Your oh_dear lemma might be worth having simply to caution against using supr over Prop for conditionally_complete lattices

[Eric Wieser]

Oliver Nash said:

This might not be a bad time to remind you about #7439 !

I was hoping to leave that for Yury, but they've been absent for a while.

[Patrick Massot]

I also fall into this trap every now and then. The most recent iteration was https://github.com/leanprover-community/lean-liquid/blob/master/src/prop_92/concrete.lean#L118-L119 that I initially stated wrong because of this (it seems very close to Eric's example).