upper semicontinuous functions are bounded below compact

Stream: Is there code for X?

[Antoine Chambert-Loir]

I couldn't find in mathlib that lower semicontinuous functions are bounded below on compact sets.

On the other hand, I expect that it is a consequence of the result for continuous function if \R is endowed with one of the two order topologies, provided that one proves that continuous functions for this topology coincides with the lower semicontinuous functions.

However, since the topologies are given by instances, I am not sure how to change the topology of the goal for a function f : X \to R. (One could compose with the maps (R, classical) -> (R, order topology)…)

[Kevin Buzzard]

You could make a new type def real_with_order_topology := \R and typeclass inference will not unfold this definition, so you are free to put a new topology on real_with_order_topology. The computer scientists call this a "type synonym" I think.

[Antoine Chambert-Loir]

Yes, but my function already takes its values into \R…

[Yaël Dillies]

This is what we've been doing with other topologies

[Kevin Buzzard]

Antoine Chambert-Loir said:

Yes, but my function already takes its values into \R…

Right -- I thought you were asking how to compose with (R,classical) -> (R,order topology) and my answer is "instead compose with id : R -> real_with_order_topology" (which you will be able to prove is continuous)

[Antoine Chambert-Loir]

Yaël Dillies said:

This is what we've been doing with other topologies

Can you refer to some places where you do that?

[Antoine Chambert-Loir]

Also : where is it proved that continuous functions, that they attain they lower bound on nonempty compact sets?

[Patrick Massot]

Look around docs#is_compact.exists_forall_le

[Antoine Chambert-Loir]

Thanks!

[Eric Wieser]

Antoine Chambert-Loir said:

Yaël Dillies said:

This is what we've been doing with other topologies

Can you refer to some places where you do that?

I think docs#weak_dual is such a case? Edit: this one should probably be reducible, the actual type synonym is docs#weak_bilin

[Anatole Dedecker]

On the other hand, I expect that it is a consequence of the result for continuous function if \R is endowed with one of the two order topologies, provided that one proves that continuous functions for this topology coincides with the lower semicontinuous functions.

Note that this won't work directly because docs#is_compact.exists_forall_le assumes [order_topology α], which isn't true for the upper/lower topology (in mathlib order_topology means the bilateral one)

[Anatole Dedecker]

Now I've nerdsniped myself and will spend the rest of the evening searching for the right abstraction for the different order topologies...

[Anatole Dedecker]

Actually in your situation you can get away with that, since you don't need the lower bound to belong in the image, so you should be able to use docs#is_compact.bdd_below (at least in theory, I don't think we have type aliases for lower and upper topologies, do we ? @Yaël Dillies)

[Anatole Dedecker]

Oh but I'm not sure that works either, since you don't even have docs#order_closed_topology

[Anatole Dedecker]

So really the good answer is that the right generality for docs#is_compact.bdd_below is "any linear order where docs#is_open_Ioi holds"

[Jireh Loreaux]

Sorry, I must be missing something: why don't we have docs#order_closed_topology in this context?

[Anatole Dedecker]

What Antoine wanted to say (if I understand well) is that lower semicontinuous functions are exactly continuous functions when you replace the topology on the codomain with the upper (I'm risking it...) order topology, i.e the one generated by upwards-closed open intervals, and then apply docs#is_compact.bdd_below to the image of the compact K under f (which is compact for this new topology). The problem is that this "upper order topology" does not satisfy docs#order_closed_topology (I think).

[Jireh Loreaux]

ah, oops, sorry for the noise, in my head I was interpreting lower order topology as lower limit topology, which is wrong; the former is coarser than the usual topology, while the latter is finer.

[Anatole Dedecker]

Oh I understand the confusion, sorry for that !

[Anatole Dedecker]

Here is at least a working version directly adapted from docs#is_compact.bdd_below, but that's not very satisfying in terms of code duplication.

import topology.semicontinuous

open set

section

variables {β α : Type*} [topological_space α] [topological_space β] [linear_order β]
  [order_closed_topology β] [nonempty β]

example {f : α → β} (hf : lower_semicontinuous f) {K : set α} (hK : is_compact K) :
  bdd_below (f '' K) :=
begin
  by_contra H,
  rcases hK.elim_finite_subcover_image (λ x (_ : x ∈ K), @lower_semicontinuous.is_open_preimage _ _ _ _ _ hf (f x)) _
    with ⟨t, st, ft, ht⟩,
  { refine H ((ft.image f).bdd_below.imp $ λ C hC, _),
    rintros _ ⟨x, hx, rfl⟩,
    rcases mem_Union₂.1 (ht hx) with ⟨x', hx', fx_le_fx'⟩,
    exact le_trans (hC $ mem_image_of_mem f hx') (le_of_lt fx_le_fx') },
  { refine λ x' hx', mem_Union₂.2 (not_imp_comm.1 _ H),
    exact λ h, ⟨f x', λ y ⟨x, hx, hxy⟩, le_of_not_lt (h.imp $ λ ys, ⟨_, hx, hxy.symm ▸ ys⟩)⟩ }
end

end

[Anatole Dedecker]

Aha, we do have docs#with_lower_topology, but no "upper topology"

[Anatole Dedecker]

I'm a bit hesitant to make a PR for that right now, but the plan would be :

• add the dual version of the whole docs#lower_topology file
• make the links between these and semicontinuity
• add has_open_Iio and has_open_Ioi typeclasses (*) and prove docs#is_compact.bdd_below (and its consequences) using these

(*): this is not very important, but it seems to me that in the context of non-linearly-ordered spaces, working with closed intervals is much better, so maybe we should have has_closed_Iic and has_closed_Ici typeclasses, and also redefine docs#lower_semicontinuous in terms of $\le$ rather than $<$.

[Antoine Chambert-Loir]

Another possibility would be to define the bdd_above functions for upper_semicontinuous functions, as well as the existence of maximum on compact subset, and to deduce it for continuous one. And replacing the order by the opposite order, having the similar results for lower_semicontinuous functions.

[Anatole Dedecker]

Yes but that means some code duplication in any cases. The nice thing in the continuous case is that we don't have to redo the covering argument, since we can just apply docs#is_compact.bdd_below. But that can't work for semicontinuous functions of course, unless we change the topology, so we would have to redo the covering argument for the special case of the image of a compact set by a semicontinuous function (which is essentially what I did above).
I agree that's not a ton of code duplication, but the plan I described would avoid it so I would try and do that if we weren't in the middle of the port :sweat_smile:

[Yaël Dillies]

Anatole Dedecker said:

• add the dual version of the whole docs#lower_topology file

I did insist in @Christopher Hoskin's original PR that we should keep the API fully dualised, but I wasn't heard :sad:

[Yaël Dillies]

I agree with having typeclasses like has_closed_Ici/has_closed_Iic. I haven't gone forward with it yet because I want to have enough order topologies in mathlib to decide what mixins are worth having and refactor everything at once.

[Yaël Dillies]

Anatole Dedecker said:

Aha, we do have docs#with_lower_topology, but no "upper topology"

Yeah that's the type synonym I was thinking of.

[Christopher Hoskin]

I did insist in @Christopher Hoskin's original PR that we should keep the API fully dualised, but I wasn't heard :sad:

https://github.com/leanprover-community/mathlib/pull/17037#issuecomment-1288205983

[Anatole Dedecker]

I spent some time thinking about this, and I think I have a pretty good idea on which typeclass to add so that we can just use docs#is_compact.exists_forall_le.

• add closed_Ici_class and closed_Iic_class to have a "one-sided" generalization of docs#order_closed_topology (docs#is_compact.bdd_below could be proven in this context for example)
• add left_order_topology and right_order_topology to have a "one-sided" generalization of docs#order_topology. This one is a bit more tricky, because we want to have a predicate that generalizes both for docs#order_topology and docs#lower_topology (which are incompatible in most cases). I think that the right notion then is for docs#nhds_within_Iic_basis to hold (with special condition for maximal elements), and that it should be enough to get docs#is_compact.exists_forall_le

[Anatole Dedecker]

Fun fact : we have both docs#nhds_within_Ici_basis and docs#nhds_within_Ici_basis_Ico

[Anatole Dedecker]

I'm more and more tempted to do this refactor right now since it shouldn't really touch a lot of files (we don't have to do all the generalizing at once, and everything assuming order_topology should keep working), but I'm sure I underestimate how much trouble this will be to port.

[Yaël Dillies]

You have my backing for at least closed_Ici_class/closed_Iic_class

[Yaël Dillies]

I've thought a bit about the other problems, but apparently in a disjoint way to yours.

[Yaël Dillies]

Since you seem to have a headstart on me here, let me set you a testcase: Can you replace docs#has_upper_lower_closure by a more sensible typeclass of yours?

[Anatole Dedecker]

Discussing about this with Antoine, I realized that the hypotheses of docs#is_compact.exists_is_least are way too strong because of conditional completeness: the current version works by saying "take the Inf, it is well behaved because of docs#is_compact.bdd_below, and it's in the set because of docs#is_glb". But the proof of docs#is_compact.bdd_below can be tweaked to give a docs#is_least element without any stronger assumptions, so we can use this one directly.
To be more concrete, take a compact subset of $\mathbb{Q}$. The current version of the lemma wouldn't apply because rat is not conditionally complete. But we can still construct a least element of our set, just using compactness.
I've just opened #18991 to fix that.

[Anatole Dedecker]

This has the added benefit of making half of my proposed refactor unnecessary to make Antoine's argument work, because closed_Iic_class will be enough to prove docs#is_compact.exists_is_least and the upper topology satisfies that.

[Anatole Dedecker]

Yaël Dillies said:

Since you seem to have a headstart on me here, let me set you a testcase: Can you replace docs#has_upper_lower_closure by a more sensible typeclass of yours?

Hmmmm it's not immediately obvious that this is related, but I'll have a closer look

[Yaël Dillies]

It's not obviously related, but the reason I suggest it is that has_upper_lower_closure holds in $\R^n$ but there's no other typeclass that can currently cover the lemmas, because the product of order_topologys (even finite) isn't an order_topology.

[Anatole Dedecker]

I opened #6345, adding classes LowerClosedTopology and UpperClosedTopology expressing that Iics/Icis are closed, and generalizing boundedness of compacts to these classes. As @Jireh Loreaux rightfully pointed out, these names are a bit terrible because they mean that the UpperTopology is a LowerClosedTopology... I can think of other names, but I'm not sure which one is best, so let's poll!

[Anatole Dedecker]

/poll How to name classes for "Iics are closed"/"Icis are closed"?
LowerClosedTopology/UpperClosedTopology
ClosedIicTopology/ClosedIciTopology
ClosedIicClass/ClosedIciClass

[Anatole Dedecker]

Ping @Yaël Dillies

[Anatole Dedecker]

Now that I think about it, it would also be nice to get @Christopher Hoskin's opinion

[Kevin Buzzard]

(Yael is up a mountain I believe)

[Anatole Dedecker]

Well not high enough to not answer the poll apparently :upside_down:

[Yaël Dillies]

You got lucky. Today is rest day. :campsite:️

[Eric Rodriguez]

The lake district has annoyingly good mobile reception!

[Patrick Massot]

You should go to Yellowstone, I can attest there is no connection at all. I can post because I just left the park to fly back to Pittsburgh.