[Merged by Bors] - feat(analysis/special_functions): `real.log` is infinitely smooth away from zero #5116

urkud · 2020-11-25T21:41:48Z

Also redefine it using order_iso.to_homeomorph and prove more lemmas about limits of exp/log.

depends on: [Merged by Bors] - chore(order/rel_iso): add a few lemmas #5106 order_iso lemmas
depends on: [Merged by Bors] - chore(order/basic): add strict_mono_??cr_on.dual and dual_right #5107 strict_mono_incr_on.dual
depends on: [Merged by Bors] - chore(topology/algebra/ordered): add order_iso.to_homeomorph #5111 order_iso.to_homeomorph
depends on: [Merged by Bors] - feat(topology/algebra/ordered): add lemmas about map coe at_top/at_bot #5238 map/comap at_top in open intervals
depends on: [Merged by Bors] - chore(topology/algebra/ordered): generalize intermediate_value_Icc etc #5235 generalize IVT

We can use these to avoid `@strict_mono_??cr_on (order_dual α) (order_dual β)`.

* add lemmas `order_iso.apply_eq_iff_eq` etc; * define `order_iso.symm`.

hrmacbeth · 2020-11-27T20:39:37Z

Since you're taking this opportunity to do a general refactor of log, I wanted to discuss what the cleanest way is to set up this and similar functions. You're deriving the main properties from strict_mono_incr_on.continuous_at, but it should also be possible to do it by analogy with the method for arctan (#4138), which uses homeomorph_of_strict_mono_continuous_Ioo.
I think the homeomorph_of_strict_mono_continuous_Ioo method slightly reduces code duplication, by eliminating the need for lemmas like tendsto_log_at_top (or rather, permitting them to be deduced from general theory for the inverses of monotone functions). Alternatively we could refactor arctan to follow the method you take here. What do you think?

urkud · 2020-11-27T21:22:27Z

I have a refactor of arcsin and arctan in https://github.com/leanprover-community/mathlib/blob/arcsin-redefine/src/analysis/special_functions/trigonometric.lean
I use an order_iso and the corresponding homeomorph to define the inverse function. Possibly I should redefine log in the same way: define exp_order_iso : \R ≃o Ioi 0, then take the inverse.

hrmacbeth · 2020-11-27T21:55:43Z

I use an order_iso and the corresponding homeomorph to define the inverse function.

Ah, fantastic!

Possibly I should redefine log in the same way: define exp_order_iso : \R ≃o Ioi 0, then take the inverse.

In my opinion that is definitely the most elegant method. If you have the energy, that would be great! I guess it requires one of the other 9^2 variants of surj_on_Ioo_of_continuous_on, namely

lemma surj_on_Ioi_of_continuous_on' {f : α → β} {a : β}
  (hf : continuous f) (h_top : tendsto f at_top at_top)
  (h_bot : tendsto f at_bot (𝓝[Ioi a] a)) :
  surj_on f univ (Ioi a) :=

hrmacbeth · 2020-11-27T22:10:03Z

If I understand correctly, that would allow you to slim down #5111, since order_iso.to_homeomorph would be the only theorem required for external purposes (no need for strict_mono_incr_on.continuous_at, which you're currently using for log). And I think that in such a slimmed-down version, there could be a very direct proof of order_iso.to_homeomorph, essentially by noting that an order isomorphism induces an isomorphism of the order topology.

On the other hand, maybe it's worth keeping the local results such as strict_mono_incr_on.continuous_at, even if they're not used elsewhere. What do you think?

urkud · 2020-11-27T22:23:33Z

I would prefer to keep local results. I have no particular applications in mind right now but I don't want to prove them once more when they will be needed. UPD: I already have a use case for a local lemma.

hrmacbeth

Looks good to me. Since the redefinition of log is a moderately fundamental change (a big improvement in my opinion!), let's leave the PR open for a day or so, for greater visibility?