Express the root of a number in terms of roots of reals.

[arpie-steele]

These theorems have been created in my mathbox, close to the each last required theorem.

• sqrtcvallem1 expresses an equivalent condition for fifth hypothesis of eqsqrtd.
• reabsifneg , reabsifnpos , reabsifpos , and reabsifnneg express the absolute value of a real number using if in various ways, only reabsifneg is used below. reabssgn was added in to give a parallel proof in terms of df-sgn.
• sqrtcvallem2 , sqrtcvallem3 , sqrtcvallem4 , sqrtcvallem5 relate to a square root having a non-negative real argument thus justifying the universality of the formula. The sum requires more steps than the difference.
• sqrtcval and sqrtcval2 are the main result. A YouTube video by Michael Penn is cited as inspiration.sqrtcval is a slightly longer statement but conforms to the format expected by crred and crimd
• resqrtval and imsqrtval give just the real and imaginary parts, respectively. They have examples now.

[tirix]

Looks good! Why not start off of a Mathbox first ?

[arpie-steele]

I don't need it to be in the main section, but I thought these theorems were of general interest and consistent with current content:

1. Re, Im, * (conjugate), abs, and sqrt are all introduced in the same section, so being able prove a closed form for the real and imaginary part of the square root seemed like natural development of the topic ; while eqsqrtd lets one check a guess of a square root, sqrtcval allows one to calculate it (up to an expressing involving radicals of positive reals).
2. The proofs of lemmas 2/3 expose a potential asymmetry in how the cases abs + Re and abs - Re have supporting theorems
3. Newton's method to find the non-negative square root function is well-behaved while without sqrtcval a naive implementation of complex square root may converge to the wrong root (notably NIST doesn't have advice for the complex square root at https://dlmf.nist.gov/1.9 ) ; (Wikipedia and Handbook of mathematical functions with formulas, graphs, and mathematical tables (1964) both have this formula.)
4. Finally, having convinced myself that it was a strong candidate to eventually move to main, putting it in my sandbox seemed like wasted effort to document the move

Please let me know if you really want it in my mathbox.

[benjub]

This is not ready for the main section: wrong comments, mislabelings of lemmas, redundant statements (only one of the four versions of the absolute value of reals is necessary; probably the one with the condition if 0 <= x$). And link to a youtube video for such a basic formula ? Does this formula have applications ? That's a real question: it may be interesting and I do not know. I'm asking, because many such formulas can be devised.

It would probably be worth introducing the signum function, if it's not already in set.mm.

[tirix]

It would probably be worth introducing the signum function, if it's not already in set.mm.

We do have df-sgn. It's a good remark that it could be used in some of those formulas.

[arpie-steele]

The formula √z = √[½(|z| + Re[z])] ± i √[½(|z| − Re[z])] with the sign chosen based on the sign of Im[z] (but not signum(Im[z])) because we want +1, not 0, for the case when z is a purely real number) appears as 3.7.27 on page 17 of Handbook of mathematical functions with formulas, graphs, and mathematical tables (1965) and probably many other places. The video was my inspiration to formalize this. The lemmas with 2 and 3 in their labels are described with the (equivalent!) expressions that motivate a need for them, as is made clear by the last two theorems. The labels could be improved with a link to those later theorems. I will work on returning these theorems to my sandbox.

[avekens]

I will work on returning these theorems to my sandbox.

I think this is a good idea to avoid any further discussion, and it is good practice to put such theorems in a mathbox first. As soon as these theorems are used by another one, they can be moved (maybe partly) to main.

[benjub]

The formula √z = √[½(|z| + Re[z])] ± i √[½(|z| − Re[z])] with the sign chosen based on the sign of Im[z] (but not signum(Im[z])) because we want +1, not 0, for the case when z is a purely real number) appears as 3.7.27 on page 17 of Handbook of mathematical functions with formulas, graphs, and mathematical tables (1965) and probably many other places. The video was my inspiration to formalize this. The lemmas with 2 and 3 in their labels are described with the (equivalent!) expressions that motivate a need for them, as is made clear by the last two theorems. The labels could be improved with a link to those later theorems. I will work on returning these theorems to my sandbox.

If it's in that book, then that answers my question above and it can probably be put to Main in a later PR (with that reference).

Indeed, the 2-step process of first mathbox, and then, give other viewers some time to see if/what part can go to main, or should be modified or relabeled or recommented... is a sound process.

[arpie-steele]

It would probably be worth introducing the signum function, if it's not already in set.mm.

We do have df-sgn. It's a good remark that it could be used in some of those formulas.

reabssgn was created folloowing your suggestion.

[wlammen]

The last two commits are shortenings, affecting the internals of a proof only.

[david-a-wheeler]

As the perpetrator of df-sgn I always encourage its (appropriate) use :-). I do think that at least some of these should eventually move from the mathbox into the "main" area, but we do often start with mathboxes first.