formulating continuity lemmas

Stream: sphere eversion

[Floris van Doorn]

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]

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

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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]

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]

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]

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]

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]

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

[Floris van Doorn]

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]

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.