Zulip Chat Archive

Stream: general

Topic: how far to go with junk theorem


view this post on Zulip Kevin Buzzard (Nov 14 2018 at 19:25):

If noncomputable definition nth_root (x : ℝ) (n : ℕ) : ℝ := exp (log x / n) then because log of a non-positive real is explicitly defined to be zero (log going out of its way to not ask for positivity there), we have that

lemma nth_root_pow_left' {x : } {m n : } (Hn : 0 < n) : --(Hm : 0 < m) (Hx : 0 < x) :
(nth_root x (m * n)) ^ n = nth_root x m := sorry

happens to be true for all m and x. However to prove the result for x <= 0 I would like to use the fact that if x <= 0 then log x = 0. Should this be a named lemma, even though it's a junk theorem? I can't find it.

view this post on Zulip Kevin Buzzard (Nov 14 2018 at 19:26):

Am I supposed to put the effort in to prove the result for x<=0 even though nobody will ever need this case?

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:12):

yes to both questions

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:14):

If you use the fact at least once, there should be a theorem describing "out of domain" behavior of a totalized function (although in general we want to limit the number of such theorems)

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:14):

and if it eliminates a hypothesis you should use "out of domain" behavior of functions in the proof


Last updated: May 14 2021 at 22:15 UTC