Stream: math-comp analysis

Topic: continuity and near

Yves Bertot (Jun 29 2021 at 12:46):

I would like to have a lemma with approximately the following statement:

Lemma continuous_near (f : R -> R) (y : R) (P : R -> Prop) :
  {for y, continuous f} ->
  (\forall x \near y, P (f x)) -> (\forall x \near (f y), P x).
Proof.
Admitted.

Does it fell right to you? Is there an easy proof? I first thought I would have an equivalence, but that is probably wrong.

Michael Soegtrop (Jun 29 2021 at 14:34):

If f is a constant function, the premise tells you something about the one point c=f(?) only. I don't see how one could derive something in a neighborhood of c=f(?) from that.

Michael Soegtrop (Jun 29 2021 at 14:35):

(But I am not familiar with the math-comp analysis syntax yet, so I am just guessing what it means).

Yves Bertot (Jun 29 2021 at 14:38):

@Michael Soegtrop , you are right, this rules out the right to left direction.

Cyril Cohen (Jun 29 2021 at 14:40):

sure! f @ nbhs y --> nbhs (f y) (continuity) and \forall x \near y, P (f x) = \forall x \near f @ y, P x definitionally, so it should hold

Michael Soegtrop (Jun 29 2021 at 14:46):

I am confused - doesn't my argument rule out the left to right direction? My gut feeling interpretation of the left side is "For all x in a neighborhood of y, P (f(x)) holds", so if f=c, this gives P c, which is weaker than the right side.

Cyril Cohen (Jun 29 2021 at 14:53):

you are right, it's the other way around

Cyril Cohen (Jun 29 2021 at 14:57):

Lemma continuous_near  {T U : topologicalType}
  (f : T -> U) (y : T) (P : U -> Prop) :
  {for y, continuous f} ->
  (\forall x \near f y, P x) -> \forall x \near y, P (f x).
Proof. exact. Qed.

Cyril Cohen (Jun 29 2021 at 15:00):

However, I guess that if f is continuous at y and locally injective near y, then its local inverse is also continuous atf y and you can get the other direction.

Cyril Cohen (Jun 29 2021 at 15:01):

(which rules out the counter-example with the constant function of @Michael Soegtrop )

Cyril Cohen (Jun 29 2021 at 15:03):

Lemma continuous_inj_near {R : realType} (f : R -> R) (y : R) (P : R -> Prop) :
  {for y, continuous f} -> {near y, injective f} ->
  (\forall x \near f y, P x) = (\forall x \near y, P (f x)).
Proof.
Admitted.

(Fixed after @Sebastien Gouezel post below)

Cyril Cohen (Jun 29 2021 at 15:48):

Cyril Cohen said:

Lemma continuous_near  {T U : topologicalType}
  (f : T -> U) (y : T) (P : U -> Prop) :
  {for y, continuous f} ->
  (\forall x \near f y, P x) -> \forall x \near y, P (f x).
Proof. exact. Qed.

(@Yves Bertot note that you do not need to state it since {for y, continuous f} is def eq to forall P, (\forall x \near f y, P x) -> \forall x \near y, P (f x). :wink: )

Sebastien Gouezel (Jun 29 2021 at 16:13):

The fact that a continuous bijective function has a continuous inverse is false in general (take the identity of the reals, with the discrete topology in the source space and the usual topology in the target space, for instance). However, this holds for functions on $\mathbb{R}^n$ with its usual topology, but this is a difficult theorem.

Yves Bertot (Jun 29 2021 at 19:33):

Thank you all. Yes, now I understand Michael's argument. "P(f x)" only gives information about very specific values, while P x has to cover a wider space. I have to avoid thinking only in terms of points.

Yves Bertot (Jun 29 2021 at 19:58):

My use case is with f instantiated by the opposite function, it has all the nice properties. I wanted to use this as an intermediate step to prove that every monotone surjective function is continuous, itself an intermediate step to prove that the inverse of an injective continuous function is continuous.

I already have a proof for the latter fact, but I thought it was too long and could be shortened.

Cyril Cohen (Jun 30 2021 at 07:53):

Sebastien Gouezel said:

The fact that a continuous bijective function has a continuous inverse is false in general (take the identity of the reals, with the discrete topology in the source space and the usual topology in the target space, for instance). However, this holds for functions on $\mathbb{R}^n$ with its usual topology, but this is a difficult theorem.

Indeed I had $\mathbb{R}$ in mind (with the usual topology) in the initial example of Yves and generalized badly

Yves Bertot (Jun 30 2021 at 10:37):

PR https://github.com/math-comp/analysis/pull/385 now contains a few lemmas to prove the continuity of inverse functions. Sometimes, continuity of the initial funtion is required, sometimes only monotonicity of both the function and the inverse are required. The lemmas probably deserve renaming and fine-tuning of their interface, this can be discussed in the PR.

Michael Soegtrop (Jun 30 2021 at 13:32):

What I like about math-comp analysis compared to the standard library is that the lemma statements in @Yves Bertot's PR are intuitively readable, even knowing nothing about math-comp-analysis. Lemma statements about continuity in the standard library are rather hard to digest. I think this is a very important feature.

I just wonder in how far this improved readability makes it harder to write things - frequently these two goals are a bit contradicting. E.g. advanced notations easily lead to rather obscure error messages or unexpected effects if say a certain "notation product space" is incomplete. I would be interested in experience in this area.

Yves Bertot (Jun 30 2021 at 14:28):

The notations make for readable statements. The difficulty lies in finding lemmas to progress. I wanted to follow the abstraction barriers that are suggested by notations and existing lemmas, but I sometimes hit a difficulty. Personally, I would not have come with using the {mono f : x y / x <= y} notation, that was suggested to my when @Laurent Théry proofread one of my first attempts. He also suggested a more systematic use of ltrgtP to reason by cases comparisons between values. This kind of lemma is likely to fly under the radar of newcomers, but it is equipped to simplify many sub-expressions of your goal as you go. The tactic remains a simple case tactic, but the lemma packs a host of automatic behavior. I find this kind of advanced proof programming is an extra layer of knowledge that is under-documented.

Yves Bertot (Jun 30 2021 at 14:31):

Anyway, these proof are still in draft state.

Reynald Affeldt (Jun 30 2021 at 14:32):

mono and ltrgtP are not mathcomp-analysis specific, right?

Cyril Cohen (Jun 30 2021 at 14:32):

Reynald Affeldt said:

mono and ltrgtP are not mathcomp-analysis specific, right?

Nop they are not

Yves Bertot (Jun 30 2021 at 14:34):

It is worth clarifying, but I still mean that I often ignore how to make the best usage of math-comp or math-comp analysis features.

Yves Bertot (Jun 30 2021 at 14:41):

When proving lemma near_opp, it is the first time I broke the abstraction barrier of the (\forall _ \near _, _) . Until then, I did not know that this was "only" a notation for an existential statement with an espilon and a ball of that radius (I guess this is related to exact topology currently in use).

Michael Soegtrop (Jul 01 2021 at 07:02):

To summarize, you are saying that the main difficulty is that despite the nice and intuitive notations you have to see through them and know what they really mean going down at least a few layers of abstraction to actually work with them?

Do you think this is so because lemmas are missing at the higher levels of abstraction so that one frequently needs to go into lower layers, or do you think this is more a principal problem which cannot be overcome by better "closing" (I am searching for a better word here ...) each layer of abstraction?

Last updated: Aug 19 2022 at 20:03 UTC