[Merged by Bors] - feat(analysis/seminorm): semilattice_sup on seminorms and lemmas about ball

[mcdoll]

Define bot and the the binary sup on seminorms, and some lemmas about the supremum of a finite number of seminorms.
Shows that the unit ball of the supremum is given by the intersection of the unit balls.

Co-authored-by: Eric Wieser wieser.eric@gmail.com

---

[mcdoll]

There might be quite some room for golfing and I don't know whether there is an easier solution to deal with nnreal.

[eric-wieser]

Can you instead provide a semilattice_sup and order_bot instance on seminorm? That way finset.sup is the definition in this PR.

[eric-wieser]

A template to get you started:

-- this belongs immediately after the `has_coe_to_fun` instance
lemma coe_injective : @function.injective (seminorm 𝕜 E) (E → ℝ) coe_fn
| ⟨x, _, _⟩ ⟨y, _, _⟩ rfl := rfl

instance : has_sup (seminorm 𝕜 E) :=
{ sup := λ x y,
  { to_fun := x ⊔ y,
    triangle' := sorry,
    smul' := sorry }}

@[simp] lemma coe_sup (x y : seminorm 𝕜 E) : ⇑(x ⊔ y) = x ⊔ y := rfl

instance : semilattice_sup (seminorm 𝕜 E) :=
function.injective.semilattice_sup _ coe_injective coe_sup

instance : order_bot (seminorm 𝕜 E) :=
{ bot :=
  { to_fun := 0,
    triangle' := λ x y, by simp,
    smul' := λ k x, by simp },
  bot_le := nonneg }

@[simp] lemma coe_bot : ⇑(⊥ : seminorm 𝕜 E) = 0 := rfl

[mcdoll]

ah thanks, I will try that.

[eric-wieser]

With that in place, the new definition is just:

def seminorm_sup_finset (p : ι → seminorm 𝕜 E) (ι' : finset ι) : seminorm 𝕜 E :=
  ι'.sup p

which of course doesn't need to exist any more.

[mcdoll]

@eric-wieser it works perfectly. I need two lemmas that have nothing to do with seminorms: sup_eq_sup for sup-semilattices and mul_sup for the reals (was written by @user7230724 ), should I make separate PRs for them or is it ok to have them in this PR?

[eric-wieser]

Push them to this PR for now, then we can discuss moving them

[mcdoll]

I don't really understand how to unfold ι'.sup p, I tried to apply in l. 527 finset.sup_induction (which doesn't seems to be the correction thing in the first place), but I failed.

[eric-wieser]

bors d+

[bors]

✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mcdoll]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests