## Stream: general

### Topic: how far to go with junk theorem

#### 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.

#### 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?

#### Mario Carneiro (Nov 14 2018 at 20:12):

yes to both questions

#### 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)

#### 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: Dec 20 2023 at 11:08 UTC