Zulip Chat Archive

Stream: sphere eversion

Topic: formulating continuity lemmas

Floris van Doorn (Oct 25 2021 at 13:58):

I was struggling quite a lot with formulating the right continuity lemmas for certain functions/operations when proving Lemma 1.13.
I wrote some thoughts in a library note (#9954)
I think many lemmas are not following this principle (both in mathlib and in sphere eversion), and could be improved in generality and/or convenience by following this advice.

Reid Barton (Oct 25 2021 at 14:12):

Looks good, I didn't understand this line though:

- All n-ary function arguments are replaced by n+1-ary functions

Kevin Buzzard (Oct 25 2021 at 14:20):

Oh this is very nice! Yeah I also don't understand that line, it seems that to say addition is continuous you now need four inputs to the predicate not 3

Reid Barton (Oct 25 2021 at 14:20):

Oh, I think I see. You mean if there is a variable that is itself a function.

Reid Barton (Oct 25 2021 at 14:21):

e.g. continuity of function application (when it holds) should be formulated with a conclusion like continuous (\lam i, f i (x i)) where now f has two arguments even though the function in function application has only 1

Reid Barton (Oct 25 2021 at 14:23):

One way to think about this is that you're "reifying" the context Γ\Gamma into a type (called X in the continuous.add example), and all the terms in context Γ\Gamma into explicit functions. I use this perspective a lot in the o-minimality formalization.

Reid Barton (Oct 25 2021 at 14:24):

You can also relate it to the Yoneda embedding, e.g., MM being a topological monoid really just means that the functor it represents on top. spaces (like X) takes values in monoids

Reid Barton (Oct 25 2021 at 14:25):

and that's the relationship between continuous (λ p, p.1 + p.2) and
continuous.add : {f g : X → M} (hf : continuous f) (hg : continuous g) : continuous (λ x, f x + g x)

Floris van Doorn (Oct 25 2021 at 15:03):

Yes, you're adding an X → to all relevant arguments (all arguments where you can add it so that the statement makes sense)

Floris van Doorn (Oct 25 2021 at 15:28):

I added some comments about how to formulate a lemma about a function that has discontinuities. I refer to continuous_at.comp_div_cases which is from #9959

Kevin Buzzard (Oct 26 2021 at 17:29):

It occurred to me today that this proposal involves quantifying over types. Would the idea be that in

continuous.add {f g : X  M} (hf : continuous f) (hg : continuous g) : continuous (λ x, f x + g x)

you would quantify over all X in the same universe as M, or over all X in all universes? My instinct would be to stick to Ms universe rather than introduce another universe variable.

Johan Commelin (Oct 26 2021 at 17:48):

I guess it doesn't matter, because in the end you are proving a Prop. So it's fine to quantify over all universes.

Reid Barton (Oct 26 2021 at 20:25):

Plus these are top-level definitions, so there is no real reason not to quantify over all universes. And it might be useful at use sites, because who knows what kind of stuff could be in the context.

Reid Barton (Oct 26 2021 at 20:25):

The actual definition of topological_monoid can just be phrased in terms of M×MMM \times M \to M and doesn't need to quantify over X at all

Floris van Doorn (Oct 27 2021 at 09:34):

Yeah, my comments are really about the conclusions of lemmas. Hypotheses and type-classes can (and should) still state that some n-ary function is continuous.

Tomas Skrivan (Nov 05 2021 at 15:09):

I have randomly stumbled on this thread and realized I have been doing something very similar recently. In particular, I'm trying to use typeclass system to automatically prove continuity/differentiability/linearity.

In my approach, you can get away with using the "the traditional way" and "the convenient way" is inferred automatically. An example of proving automatically the convenient from traditional:

example (f : α  β  γ) (g : δ  ε  α) (h : δ  ε  β) [IsSmooth f] [ a, IsSmooth (f a)] [IsSmooth g] [IsSmooth h]
        : IsSmooth (λ x y => f (g x y) (h x y)) := by infer_instance

For example f could be add and [IsSmooth f] [∀ a, IsSmooth (f a)] is stating that f is smooth in the first and the second argument.

However, I'm using Lean 4 and I had to do a minor tweak to the typeclass system, see this post for more examples.

Last updated: Dec 20 2023 at 11:08 UTC