upper hemicontinuity vs. upper semicontinuity

Stream: maths

[Jireh Loreaux]

There is a standard fact in the theory of complex Banach algebras: the spectrum is upper hemicontinuous (although sometimes in the literature on this subject it is also called upper semicontinuous). I just assumed that it should be possible to unify this with our current definition of docs#UpperSemicontinuous, which would give us access to all that API, but as it stands it is not quite so easy.

[Jireh Loreaux]

For reference:

def UpperSemicontinuousAt {α : Type*} [TopologicalSpace α]
    {β : Type*} [Preorder β] (f : α → β) (x : α) : Prop :=
  ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y

[Jireh Loreaux]

The definition of f : α → Set γbeing upper hemicontinuous at a : α is that for every open set u with f a ⊆ u, there is a neighborhood v ∈ 𝓝 a such that for every x ∈ v, f x ⊆ u. Or, in the language of filters (this definition does not currently exist in Mathlib):

UpperHemicontinuousAt (f : α → Set γ) (a : α) := ∀ u : Set γ, u ∈ nhdsSet (f a) → ∀ᶠ (x : α) in 𝓝 a, u ∈ nhdsSet (f x)

[Jireh Loreaux]

And now you can see the similarity with the definition of upper semicontinuity (by choosing β := Set γ and (s < t) := (t ∈ nhdsSet s)). However, there are two problems with this.

1. t ∈ nhdsSet s is definitely not the LT instance on Set γ
2. t ∈ nhdsSet s doesn't correspond to the < for some Preorder on Set γ as it's not irreflexive (since u ∈ nhdsSet u if u is open).

[Jireh Loreaux]

There is one way to deal with the fact that it doesn't correspond to a Preorder: bundle spectrum ℂ into a function from the complex Banach algebra A to docs#TopologicalSpace.NonemptyCompacts (here you need to assume [Nontrivial A] which is annoying), and then for t s : NonemptyCompacts ℂ, the relation (t : Set ℂ) ∈ nhdsSet (s : Set ℂ) is irreflexive, and so corresponds to the < of a Preorder. However, NonemptyCompacts already has an ordering, and it's just the pullback from the coercion to Set ℂ. So, (a) this only partially solves the problem, and (b) it still doesn't allow us to talk about hemicontinuity as semicontinuity more generally.

[Jireh Loreaux]

Therefore, I wonder if we might replace the definition of UpperSemicontinuousAt (and friends) with:

def UpperSemicontinuousAt {α : Type*} [TopologicalSpace α]
    {β : Type*} (r : β → β → Prop) [hr : IsTrans r] (f : α → β) (x : α) : Prop :=
  ∀ (y : β), r (f x) y → ∀ᶠ (x' : α) in nhds x, r (f x') y

I'm interested to hear comments on this. Another possibility would be to define UpperSemicontinuousAtWith as this more general version, and then let UpperSemicontinuousAt be an abbrev for this with r instantiated as < and assuming a Preorder β.

[Jireh Loreaux]

Of course, I could just define UpperHemicontinuousAt, but duplicating API makes me :mad: and :cry:

[Mario Carneiro]

is it even "upper" anymore at that point? Presumably lower semicontinuous just uses > instead of <

[Mario Carneiro]

I was also thinking you could merge r and f into one relational argument r' x y = r (f x) y, since they don't appear separately

[Jireh Loreaux]

fair point, we should remove the Upper in the name in that case.

[Jireh Loreaux]

I think you don't want to merge r and f, because I think you still want to know that r itself is transitive, otherwise I suspect it will be relatively useless.

[Mario Carneiro]

is knowing r is transitive but f is not monotone good for anything?

[Mario Carneiro]

it might be worth doing some reverse math on theorems using this assumption

[Jireh Loreaux]

I mean, f := spectrum ℂ is certainly not monotone in any sense, so the answer to your question is definitely "yes"

[Jireh Loreaux]

Many Banach algebra don't even have an ordering, and the ones that do (e.g., C⋆-algebras) don't make spectrum ℂ monotone.

[Mario Carneiro]

in that case, it seems the useful application of transitivity in this context is r (f x) y -> r y z -> r (f x) z, and the equivalent of that for r' is r' x y -> r' x z (or \forall x, r' x y -> r' x z) viewed as an inequality relation between y and z

[Mario Carneiro]

(which is, incidentally, transitive for any r')

[Jireh Loreaux]

Well, here's the other half of this: if I'm going to make this generalization, I want to make it as seamless as possible for the existing use case, which is Preorder β. Writing SemicontinuousAtWith (· < ·) f, while a bit annoying, wouldn't be nearly as bad as SemicontinuousAtWith (· < ·) (stupid term proving ∀ x, r' x y → r' x z) f. I guess if it's an abbrev, then maybe it's okay, but it's not my favorite thing unless we have yet another use case.

[Mario Carneiro]

I don't think the stupid term needs to be part of the definition, it would just be SemicontinuousAtWith (f · < ·)

[Jireh Loreaux]

aha, I see.

[Mario Carneiro]

you would use the term when applying a theorem that actually uses transitivity in some way

[Antoine Chambert-Loir]

@Anatole Dedecker and I had a discussion about this because we need a lot of semicontinuity for our proof of the von Neumann minimax theorem (Sion's theorem, actually), all of which I can remember is that mathlib's definition of semicontinuity is not the good one (only valid for real numbers) and that a naive extension (for nonlinear orders) is ridiculously uninteresting.

[Antoine Chambert-Loir]

Still, the thread is there: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Semicontinuity.20definition.20for.20non-linear.20orders/near/432898278

[Jireh Loreaux]

I got around to implementing the generalization discussed above in #32521. There are not tons of theorems shared between lower/upper semicontinuity and lower/upper hemicontinuity, but there were just enough that I decided it was worth it. This PR is too big to be a standalone (it splits the Semicontinuous file, generalizes the definitions, and also adds definitions and some basic results for hemicontinuity), and I will split it if the general idea receives approval.

[Yury G. Kudryashov]

Note that we've discussed an incompatible change to these definitions some time ago, namely making these theorems https://urkud.github.io/SardMoreira/docs/SardMoreira/UpperLowerSemicontinuous.html true by definition.

[Yury G. Kudryashov]

I don't know what's the right (i.e., useful) definition of an upper semicontinuous function with codomain ℝ × ℝ though.

[Jireh Loreaux]

@Yury G. Kudryashov what is the incompatible change?

[Jireh Loreaux]

Oh nevermind, I misread. Where was this discussed?

[Jireh Loreaux]

Wait, isn't this the same as the thread Antoine linked above? My generalization is compatible with that suggestion.

[Oliver Nash]

I have some remarks as follows:

1. I agree that the definitional equality Yury highlights is desirable but mostly just because it's a sign that we've set things up nicely, rather than because we should actually use it (beyond some API lemmas having proofs that are rfl).
2. Although Jireh's refactor does not change anything definitionally, I believe it does bring us closer to the desired definitional equality. This is because it gives us control over the relation r here and so it will be very easy in subsequent work to change his new definition of UpperSemiContinuousWithinAt from SemicontinuousWithinAt (f · < ·) s x to SemicontinuousWithinAt (¬ f · ≥ ·) s x. This in turn means that one will prove Yury's lemma via docs#Topology.IsLower.tendsto_nhds_iff_not_le rather than docs#Topology.IsLower.tendsto_nhds_iff_lt (which is proved via the former).
3. My guess is that to get all the way to Yury's definitional equality, we would also need to change the definition of docs#Topology.lower, though as I say I don't think this is especially important.
4. Jireh has highlighted here that Antoine's desired redefinition would also be covered if we built on Jireh's work in the same way.

Taking all this into account, as well as the independent point that this work allows us to unify with hemicontinuity I strongly advocate in favour of #32521

[Yury G. Kudryashov]

Thanks for the explanation, I agree.

[Jireh Loreaux]

Yury, to be clear, your issue wasn't about definitional equality per se, but rather about the provability of https://urkud.github.io/SardMoreira/docs/SardMoreira/UpperLowerSemicontinuous.html with Preorderinstead of LinearOrder. Is that correct?

[Yury G. Kudryashov]

Yes, I'm sorry for the confusion I've caused.

[Jireh Loreaux]

no problem, I just want to make sure we're on the same page and that we're getting the best possible outcome for Mathlib.

[Yury G. Kudryashov]

I think that some proofs about semicontinuity can be simplified by using these lemmas. E.g., exists_isMinOn.

[Jireh Loreaux]

perhaps, I have not attempted to simplify any proofs.

[Yury G. Kudryashov]

But it's a minor convenience, generalization takes priority.