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 :-(

[Eric Wieser]

Yury G. Kudryashov said:

Current version: #7907

I've pushed what I consider the remaining pieces (defaulting to Real and delaboration) to this PR, and think it is probably ready; does anyone else have opinions?

[Eric Wieser]

Yury G. Kudryashov said:

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

I vote no: this is harder to implement, and it only matters for coe because there we want transitive coercions to be unfolded.

[Eric Wieser]

Kevin Buzzard said:

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 :-(

We could have some bizarre bracketing notation like √‾x⁻¹‾

[Yury G. Kudryashov]

If we don't unfold it, then we can't use it for Nat.sqrt (because it's in Batteries).

[Yury G. Kudryashov]

Or we can backport it to Batteries (without Unicode notation) and define an instance for n-th root on Nat there.

[Yury G. Kudryashov]

@Eric Wieser What's your plan about this notation and Nat.sqrt? Backport the typeclass? Repeat lemmas? Don't use notation for Nat? Something else?

[Michael Stoll]

My 2 cents: I think it is better not to use square root notation for Nat.sqrt, to avoid confusion (since Nat.sqrt n is not actually a square root of n in general).

[Eric Wieser]

I had that thought too, but Real.sqrt r also isn't actually a square root of r when r is negative

[Michael Stoll]

But, contrary to the Nat version, this is because of a junk value, so I don't think this should be an argument. (I'd argue that Nat.sqrt of a non-square is not a junk value, but something that makes sense and is useful.)

[Eric Wieser]

Regarding lemma duplication, I'm thinking of something like

class IsLawfulNthRoot (R n) [NthRoot R n] (P : out_param <| R \to Prop) where
  nthRoot_pow (r) (h : P r) : nthRoot n r ^ n = r

[Eric Wieser]

Though maybe IsSquare is sufficient instead of p

[Yaël Dillies]

Michael, I don't really see how the situation differs. Real.sqrt of a negative real number is also something that makes sense and is useful

[Eric Wieser]

Yael, you had a number-theoretic Nat square root somewhere that rounds down the exponents of primes, rather than the real square root, right?

[Michael Stoll]

I've been using the rounded-down square root of natural numbers purposefully in informal math, but never square roots of negative reals.

[Yaël Dillies]

Eric Wieser said:

Yael, you had a number-theoretic Nat square root somewhere that rounds down the exponents of primes, rather than the real square root, right?

docs#Nat.floorRoot

[Eric Wieser]

Which one should get the nthRoot notation?

[Yaël Dillies]

There's also docs#Nat.ceilRoot

[Eric Wieser]

I guess you could imagine a ceilSqrt too

[Mario Carneiro]

Michael Stoll said:

But, contrary to the Nat version, this is because of a junk value, so I don't think this should be an argument. (I'd argue that Nat.sqrt of a non-square is not a junk value, but something that makes sense and is useful.)

It's been a while since I've seen the galois connection :counterclockwise: emoji...