Topology.IsLower vs LowerSemicontinuous

Stream: mathlib4

[Yury G. Kudryashov]

We have 2 ways to say that a function is lower semicontinuous: Continuous (Topology.WithLower.toLower ∘ f) and LowerSemicontinuous f. While they agree for linear orders (formalizing now), they disagree on, e.g., products of linear orders. The former version has a nice property that it corresponds to continuity in a topology. @Sébastien Gouëzel, are there cases when it's important that LowerSemicontinuous uses this definition for partial orders, or is it OK to redefine it to be equivalent to Continuous (Topology.WithLower.toLower ∘ f)?

[Patrick Massot]

@Antoine Chambert-Loir and @Anatole Dedecker are working on this refactor if I understand correctly.

[Antoine Chambert-Loir]

iirc what Anatole had explained to me, the classic definition breaks down for nonlinear order, in the sense that it is very unlikely to hold.

[Yury G. Kudryashov]

UPD: it looks like continuity of toLower ∘ f corresponds to upper semicontinuity of f.

[Antoine Chambert-Loir]

iirc once more, Sébastien had already said that it is crucial that the definition stays the correct one when the codomain is the real numbers, but that otherwise, it could be changed.

[Yury G. Kudryashov]

Sorry, I've missed that discussion (too much happens here, I have a very long backlog of unread messages).

[Antoine Chambert-Loir]

now, the question is whether the definition should invoke toLower or some property that some adequate intervals are open/closed.

[Antoine Chambert-Loir]

(no need to be sorry, that was probably between 6 and 18 months ago!)

[Yury G. Kudryashov]

#xy : I wanted IsCompact s → LowerSemicontinuousOn f s → ∃ x ∈ s, IsMinOn f s x proved by LowerSemicontinuousOn f s implies ContinuousOn (toUpper ∘ f) which implies the goal due to docs#IsCompact.exists_isMinOn

[Anatole Dedecker]

I’ll recall my thoughts a bit later, but about the #xy : Antoine and I need that as well for a version of the minimax theorem, so this should make it into Mathlib at some point

[Yury G. Kudryashov]

I proved the equivalence for a linear order. I'm going to PR it + the goal from #xy today or tomorrow.

[Yury G. Kudryashov]

BTW, do you know why upper topology corresponds to lower semicontinuity, not upper semicontinuity? I mean, why people hcose names this way?

[Yury G. Kudryashov]

For now, see https://github.com/urkud/SardMoreira/blob/main/SardMoreira/UpperLowerSemicontinuous.lean

[Antoine Chambert-Loir]

The point of view depends whether you expect to say something of the neighboring values, or of the limit.

[Antoine Chambert-Loir]

our needs with @Anatole Dedecker is the proof that upper semicontinuous functions reach their supremum on a nonempty compact set. It is exactly the same as for continuous functions HENCE:

• should we have 3 proofs (for usc, lsc, and cont functions)
• should the proof for continuous functions be a call to the proof for usc/lsc functions?
• should the proof for usc/lsc functions be a call to the proof for continuous functions, with the appropriate modification of topology?

[Yury G. Kudryashov]

See link above for a proof taking the 3rd route (proof for LSC calls the proof for continuous functions).

[Yury G. Kudryashov]

Possibly, we should prove for LSC/USC first, then call Continuous.lowerSemiContinuous as needed.

[Yury G. Kudryashov]

(which should be generalized to ClosedI**Topology)