English
There is a lattice structure on Seminorm with infimum (defined by inf convolution) giving the meet operation.
Русский
Существует решётка над семинормами, где inf задаёт операция meet через инф-конволюцию.
LaTeX
$$Min (Seminorm 𝕜 E) defined by (p ⊓ q)(x) = inf_u (p(u) + q(x-u))$$
Lean4
/-- We define the supremum of an arbitrary subset of `Seminorm 𝕜 E` as follows:
* if `s` is `BddAbove` *as a set of functions `E → ℝ`* (that is, if `s` is pointwise bounded
above), we take the pointwise supremum of all elements of `s`, and we prove that it is indeed a
seminorm.
* otherwise, we take the zero seminorm `⊥`.
There are two things worth mentioning here:
* First, it is not trivial at first that `s` being bounded above *by a function* implies
being bounded above *as a seminorm*. We show this in `Seminorm.bddAbove_iff` by using
that the `Sup s` as defined here is then a bounding seminorm for `s`. So it is important to make
the case disjunction on `BddAbove ((↑) '' s : Set (E → ℝ))` and not `BddAbove s`.
* Since the pointwise `Sup` already gives `0` at points where a family of functions is
not bounded above, one could hope that just using the pointwise `Sup` would work here, without the
need for an additional case disjunction. As discussed on Zulip, this doesn't work because this can
give a function which does *not* satisfy the seminorm axioms (typically sub-additivity).
-/
noncomputable instance instSupSet : SupSet (Seminorm 𝕜 E) where
sSup
s :=
if h : BddAbove ((↑) '' s : Set (E → ℝ)) then
{ toFun := ⨆ p : s, ((p : Seminorm 𝕜 E) : E → ℝ)
map_zero' := by
rw [iSup_apply, ← @Real.iSup_const_zero s]
congr!
rename_i _ _ _ i
exact map_zero i.1
add_le' := fun x y => by
rcases h with ⟨q, hq⟩
obtain rfl | h := s.eq_empty_or_nonempty
· simp [Real.iSup_of_isEmpty]
haveI : Nonempty ↑s := h.coe_sort
simp only [iSup_apply]
refine
ciSup_le fun i =>
((i : Seminorm 𝕜 E).add_le' x y).trans <|
add_le_add (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun x) ⟨q x, ?_⟩ i)
(le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun y) ⟨q y, ?_⟩ i) <;>
rw [mem_upperBounds, forall_mem_range] <;>
exact fun j => hq (mem_image_of_mem _ j.2) _
neg' := fun x => by
simp only [iSup_apply]
congr! 2
rename_i _ _ _ i
exact i.1.neg' _
smul' := fun a x => by
simp only [iSup_apply]
rw [← smul_eq_mul, Real.smul_iSup_of_nonneg (norm_nonneg a) fun i : s => (i : Seminorm 𝕜 E) x]
congr!
rename_i _ _ _ i
exact i.1.smul' a x }
else ⊥
