Zulip Chat Archive

Stream: general

Topic: Sup of seminorms

Anatole Dedecker (Sep 14 2022 at 18:18):

The TODO at https://github.com/leanprover-community/mathlib/blob/db0c0a79afe25e59baaf233e4817f37f077b3c53/src/analysis/seminorm.lean#L195 seems strange to me, because I think the linked skeleton is false. Take $E=\mathbb{R}^2$ and consider the family of seminorms $p_\alpha(x,y) = \alpha|x| + |y|$ for $\alpha>0$ , and let $q$ be their "pointwise supremum" (with mathlib conventions). Then for $a = (1,1)$ and $b = (-1, 1)$ , we have $q(a+b) = 2 > 0 = q(a) + q(b)$ . Am I missing something @Yaël Dillies @Moritz Doll ?

Eric Wieser (Sep 14 2022 at 18:23):

The skeleton for reference

Eric Wieser (Sep 14 2022 at 18:24):

Isn't the pointwise supremum in that example $q = 0$ because the set is unbounded?

Anatole Dedecker (Sep 14 2022 at 18:31):

It is bounded at $a+b$ , right ?

Yaël Dillies (Sep 14 2022 at 19:58):

What you've proven is that seminorm E is not a complete_lattice (which was already obvious by the fact there's no top seminorm), but it might still be a conditionally_complete_lattice.

Anatole Dedecker (Sep 14 2022 at 20:26):

No, I'm claiming that your proposed Sup operation does not give a seminorm. Indeed I think we could get conditional completeness, but we need to be smarter than taking the pointwise supremum

Anatole Dedecker (Sep 14 2022 at 20:28):

To be clear I wasn't expecting a true supremum of course, but the thing is that even in the dumb case we still want the sup to be a seminorm, even if it is a stupid one

Anatole Dedecker (Sep 14 2022 at 20:30):

I will try something like the following tomorrow

noncomputable instance : has_Sup (seminorm 𝕜 E) :=
{ Sup := λ s, if ∀ x, bdd_above (function.eval x ∘ coe_fn '' s) then
  { to_fun := ⨆ p : s, p,
    map_zero' := sorry,
    add_le' := sorry,
    neg' := sorry,
    smul' := sorry }
  else ⊥ }

Yaël Dillies (Sep 14 2022 at 21:15):

That just means that in the dumb case you can't take the supremum pointwise, right? But when it is not dumb, you can take it pointwise.

Yaël Dillies (Sep 14 2022 at 21:16):

Also the condition you're splitting by very much looks like bdd_above s to me

Yaël Dillies (Sep 14 2022 at 21:17):

(the direction we're interested in is obvious, the other I don't think, which means your condition is probably strictly weaker than necessary)

Anatole Dedecker (Sep 15 2022 at 07:51):

Yes of course this is bdd_above s, thanks for that. Of course this is irrelevant in the interesting case, the only thing I'm saying is that taking care of the dumb case pointwise (which is what the skeleton suggested) isn't enough, we need to take care of it globally instead.

Anatole Dedecker (Sep 21 2022 at 13:32):

#16582

Anatole Dedecker (Sep 21 2022 at 13:38):

Yaël Dillies said:

Also the condition you're splitting by very much looks like bdd_above s to me

There is actually a subtelty here, because it's not obvious that being bounded above by a function is the same as being bounded above as a seminorm, and to prove that it is indeed equivalent requires constructing the Sup of a family of seminorm bounded by a function.

Yaël Dillies (Sep 21 2022 at 13:43):

Yaël Dillies said:

(the direction we're interested in is obvious, the other I don't think, which means your condition is probably strictly weaker than necessary)

This is what I meant here :point_up:

Last updated: Dec 20 2023 at 11:08 UTC