Zulip Chat Archive

Stream: maths

Topic: Unique differentiability and definitional equality


view this post on Zulip Gabriel Ebner (Apr 12 2021 at 17:17):

The types Π i, E i and pi_Lp p hp E are definitionally equal, but they have different norms (L^∞ and L^p, resp.). Is there a reason why unique_diff_on (s : Π i, E i) and unique_diff_on (s : pi_Lp p hp) should be definitionally equal?
(It is clear that they should be equivalent because everything is finite-dimensional. I'm asking because this broke while debugging #7124. Apparently you could use a proof of unique_diff_on for L^∞ where a proof for L^2 was expected.)

view this post on Zulip Gabriel Ebner (Apr 12 2021 at 17:32):

On second thought, this is probably because unique_diff_on never mentions the norm of the tuple, and the topologies are definitionally equal.

view this post on Zulip Sebastien Gouezel (Apr 12 2021 at 17:37):

I had never noticed that this definition only depends on the topology! We should probably refactor the typeclasses in unique_diff_on to make this more obvious.

view this post on Zulip Yury G. Kudryashov (Apr 12 2021 at 20:01):

/me used unique_diff_on.pi without realizing that Lean does some heavy identifying under the hood.


Last updated: May 09 2021 at 10:11 UTC