Complex.sqrt

Stream: mathlib4

[Yury G. Kudryashov]

What do you think about

• introducing Complex.sqrt?
• adding a notation typeclass SqRt (notation: √) with instances for Real, NNReal, ENNReal, and Complex?

[Yaël Dillies]

Sounds great, but what about just Sqrt? I know it's two words, but nobody really considers them as such nowadays.

[Yury G. Kudryashov]

I don't care about lowercase/uppercase.

[Damiano Testa]

I wish more of mathlib did not care about upper/lower case...

[Yury G. Kudryashov]

(my motivation: I need formulas for the components of $\sqrt{z}$ for a project)

[Eric Wieser]

Should we skip Sqrt and jump to NthRoot?

[Yury G. Kudryashov]

Should it take a docs#Nat or a docs#PNat ?

[Eric Wieser]

That would solve the cbrt (-8) = 2 problem as well (IIRC, we currently have (-8)^(1/3) = -1)

[Yury G. Kudryashov]

How can it be -1?

[Eric Wieser]

The real part of 1 ± √3i

[Yury G. Kudryashov]

Ah, you're right.

[Eric Wieser]

It would be better if I weren't

[Yury G. Kudryashov]

But this means refactoring the existing code.

[Eric Wieser]

I'm not suggesting we change the meaning of (-8)^(1/3); but that if we are going to introduced a new notation, we may as well solve multiple problems at once

[Yury G. Kudryashov]

Because $(\sqrt[n]{x})^n=x$ needs different assumptions depending on parity of n.

[Yury G. Kudryashov]

I meant existing code that uses docs#Real.sqrt.

[Eric Wieser]

I think it's ok to add the notation for all n but only state the existing lemmas for n=2 (in the short term)

[Yury G. Kudryashov]

What notation should we use for general n?

[Eric Wieser]

We could use Mario's superscript parser hack along with √...

[Yury G. Kudryashov]

Can you write the notation/macro part?

[Eric Wieser]

import Mathlib.Util.Superscript

def nthRoot (n : ℕ) (r : ℝ) : ℝ := sorry

local syntax:arg "√" term:max : term
local syntax:arg superscript(term) "√" term:max : term
local macro_rules | `(√ $r:term) => `(nthRoot 2 $r)
local macro_rules | `($n:superscript √ $r:term) => `(nthRoot $n $r)

-- `id` is to check the precedence looks ok
#check id √4 + 1
#check id ³√8 + 1

[Eric Wieser]

Those precedences are almost certainly wrong

[Eric Wieser]

I also don't know how to overload this with √4 notation at the same time

[Eric Wieser]

Maybe @Mario Carneiro can advise, also on whether this is a good idea

[Kevin Buzzard]

If it makes it look more like the textbooks then it's a good idea (until we are allowed to write maths properly in LaTeX and have lean read that)

[Mario Carneiro]

It seems fine to me, this is exactly the sort of thing I wanted the superscript parser to be useful for

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

What do you think about

• introducing Complex.sqrt?
• adding a notation typeclass SqRt (notation: √) with instances for Real, NNReal, ENNReal, and Complex?

• Do you wish to choose a determination? the same that is used for docs#Complex.log?
  so that would be fun z => Complex.exp (Complex.log z / 2)

• SqRt is strange, why not SquareRootor the usual Sqrt?

[Yury G. Kudryashov]

It will be NthRoot

[Yury G. Kudryashov]

Yes, for complex numbers it'll be exp (log z / n).

[Yury G. Kudryashov]

a.k.a. z ^ (1 / n)

[Yury G. Kudryashov]

One more question: should it be

class NthRoot (R : Type*) (n : Nat) where
  nthRoot : R → R

or

class NthRoot (R : Type*) where
  nthRoot : Nat → R → R

[Yury G. Kudryashov]

I.e., should we accomodate for types with, e.g., square root but no cubic root?

[Mario Carneiro]

I think so, especially if it's just supposed to be a "notation typeclass"

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

One more question: should it be

class NthRoot (R : Type*) (n : Nat) where
  nthRoot : R → R

or

class NthRoot (R : Type*) where
  nthRoot : Nat → R → R

Or the opposite: types with a cubic root but no square root (such as Real).

[Yury G. Kudryashov]

We do have docs#Real.sqrt anyway

[Yury G. Kudryashov]

Notation works but doesn't delaborate.

[Yury G. Kudryashov]

Also, how should √x⁻¹ be parsed: √(x⁻¹) or (√x)⁻¹?

[Yury G. Kudryashov]

One more question: should we make it unfold to Real.sqrt/Nat.sqrt/whatever while parsing like coe does?

[Yury G. Kudryashov]

We are not going to have generic lemmas about n-th roots anyway, because every instance has its assumptions.

[Yury G. Kudryashov]

Current version: #7907

[Yaël Dillies]

Yury G. Kudryashov said:

Also, how should √x⁻¹ be parsed: √(x⁻¹) or (√x)⁻¹?

I would expect the latter

[Kevin Buzzard]

I would expect it to depend on the length of the bar on the square root symbol which latex can offer us but unicode can't :-(