Reciprocal trigonometric functions

Stream: mathlib4

[Snir Broshi]

There are 3 basic trigonometric functions (sin/cos/tan), and 3 operations one can perform on them to get more functions- reciprocal, inverse, hyperbolic. This produces 3 * 2 * 2 * 2 = 24 functions.
Mathlib has 13 of these- the 12 non-reciprocal functions, plus docs#Complex.cot.
(artanh was recently added :)

Do you think we should add the missing 11, remove cot, or do nothing?
(it's actually adding 16 because non-inverses have a complex and a real version)

While it's easy to just write 1 / ..., an advantage of adding the functions is that HasSum csc ... looks better than HasSum (1 / sin) ... and in other theorems / trig identities, and makes the results easier to Loogle (standardizes spelling between 1 / sin and fun x ↦ 1 / sin x).

OTOH randomly adding 16 functions sounds weird, even if we include some easy trig identities about them.
(maybe proving their Taylor series expansion is enough of a non-trivial theorem to motivate adding them?)

Are these reciprocals used in papers / fancy theorems, or are they a math history relic that is not worth defining?

[Joseph Myers]

I tend to think that if we have separate definitions at all for the reciprocal functions, they should not be simp-normal form (and so not have much API beyond the definition). I think all functions and results in DLMF should be in scope for mathlib, but that doesn't mean every function in informal use needs to get its own formal definition when sin⁻¹ can be used directly (apart from any potential for confusing those people who use that as informal notation for arcsin).

We should definitely add the five missing complex inverse trigonometric / hyperbolic functions to mathlib (which might in turn first require adding Complex.sqrt).

[Weiyi Wang]

Slightly off-topic but I happened to look for Complex.sqrt for other purpose. I ended up just writing ^ (1/2) because I don't care which branch it picks for my purpose, but now I wonder what branch cut it actually uses and whether Complex.sqrt can be simply defined as it

[Joseph Myers]

I expect ^ (1/2) should get the correct branch. I also think that the square root is a case where there's probably enough to say about it that it does make sense to have its own definition and API even if that's defined in terms of ^ (1/2).

[Aaron Liu]

It's just a^b = exp(b log a)

[Aaron Liu]

log is chosen so that the imaginary part is within Ioc (-pi) (pi)

[Aaron Liu]

and there's a special case for when the base is zero

[Snir Broshi]

Joseph Myers said:

I tend to think that if we have separate definitions at all for the reciprocal functions, they should not be simp-normal form (and so not have much API beyond the definition). I think all functions and results in DLMF should be in scope for mathlib, but that doesn't mean every function in informal use needs to get its own formal definition when sin⁻¹ can be used directly (apart from any potential for confusing those people who use that as informal notation for arcsin).

I mostly agree, but I'm not sure how that argument doesn't work for not defining tan. Is it just the case that it's slightly longer to write sin x / cos x than (sin x)⁻¹, so it crosses some threshold that csc doesn't?

I also think this doesn't hold for the inverse reciprocals, since they can't be as easily written; e.g. arccot x is not the same as (arctan x)⁻¹ nor arctan (x⁻¹).

Joseph Myers said:

We should definitely add the five missing complex inverse trigonometric / hyperbolic functions to mathlib

The 5 I mentioned are reciprocals not inverses, specifically Complex.csc/Complex.sec/Complex.csch/Complex.sech/Complex.coth.

There are however 6 missing real inverses, if that's what you meant: Real.arccsc/Real.arcsec/Real.arccot/Real.arcsch/Real.arsech/Real.arcoth

[Weiyi Wang]

A weird reason I'd like to use tan x over of sin x / cos x is that I'd like to have its doc to tell me what junk value it gets, instead of figuring it out by looking at the long expression

[Weiyi Wang]

(though the doc does do it currently)

[Weiyi Wang]

But I think the real "threshold" between tan and csc is just how often it is used?

[Snir Broshi]

Weiyi Wang said:

But I think the real "threshold" between tan and csc is just how often it is used?

I'm not sure we'll be able to find out before creating the definitions, since people change their expressions to accommodate for the lack of definitions. For example:

• Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean uses the expression 1 / 2 * log ((1 + x) / (1 - x)) a few times as a stand-in for artanh, because the theorems were created before the definitions: #31487 vs #32696.
• docs#Complex.Gamma_mul_Gamma_one_sub divides by sin instead of multiplying by csc, similarly for docs#Complex.Gammaℝ_one_sub_mul_Gammaℝ_one_add
• The derivative of tan is sec^2, but Mathlib uses 1 / cos^2
• docs#Complex.tan_pi_div_two_sub is tan (π / 2 - x) = cot x but doesn't use cot because it was created (mathlib3#17024) before cot was (#12758)

and there might be more, but it's very hard to find when there isn't a name for the definition.

btw the cot PR #12758 is weird, it was accepted without any justification or argument.

[Joseph Myers]

The missing inverses I'm referring to are Complex.arcsin, Complex.arccos, Complex.arsinh, Complex.arcosh and Complex.artanh. (We have Complex.arctan.) I think all of those are uncontroversial functions, with well-established standard choices of principal values, and we have all the corresponding real functions.

[Weiyi Wang]

It is probably also related to how people usually write it on paper. For gammaR, I have seen sin more than csc even when there is no mathlib limitation

[Snir Broshi]

Joseph Myers said:

The missing inverses I'm referring to are Complex.arcsin, Complex.arccos, Complex.arsinh, Complex.arcosh and Complex.artanh. (We have Complex.arctan.) I think all of those are uncontroversial functions, with well-established standard choices of principal values, and we have all the corresponding real functions.

Oh I thought there aren't nice complex inverses and that's why only the real ones were defined. Is it just the same expression Mathlib currently uses for the reals but with complex numbers? (assuming Complex.sqrt with a branch cut below the positive real line)

[Joseph Myers]

https://dlmf.nist.gov/4.23 (under "Logarithmic Forms") and https://dlmf.nist.gov/4.37 (likewise) give suitable expressions.

[Snir Broshi]

Weiyi Wang said:

It is probably also related to how people usually write it on paper. For gammaR, I have seen sin more than csc even when there is no mathlib limitation

This might be true for the gamma example, I also saw a division by sin in theorems about Chebyshev polynomial but didn't mention it because Wikipedia uses the same expression.
You could maybe make a similar argument for the derivative of tan though , but searching online seems to yield mostly the sec version. The other examples still hold IMO.

[Joseph Myers]

(These complex inverse trigonometric and hyperbolic functions have been in the C standard library since C99, for example, with the standard choice of principal value.)

[Snir Broshi]

Wow I had no idea that C has complex numbers, very cool

[Violeta Hernández]

I always saw the reciprocal functions as one of those weird things school teaches you that's outdated by two centuries. We do not need twelve new names for what amounts to (f x)⁻¹.

[Snir Broshi]

So the conclusion of this thread is to remove cot?

[Violeta Hernández]

That's my suggestion, not sure if everyone else shares it.

[Weiyi Wang]

cot has some interesting series though, to the point an entire file is dedicated to it https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.html

[Snir Broshi]

Violeta Hernández said:

That's my suggestion, not sure if everyone else shares it.

I'm not against it, but just to challenge it a little:

• Not all of them are (f x)⁻¹ btw, arccsc x = arcsin (x⁻¹). Not sure if that holds for complex inputs though.

• What about arccot? I don't know of a simple expression for it using arctan without an if:
  image.png

  

• What do we do with Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent then? Refactor and rename everything to tan_inv?

[Snir Broshi]

btw this theorem is apparently not in Mathlib, which I find strange:

theorem foo : Complex.cot = Complex.tan⁻¹ := by
  ext x
  simp [Complex.cot, Complex.tan]

[Weiyi Wang]

That's why I tell people "just do your own project on random topic and you will find small things to contribute to mathlib here and there":joy:

[Scott Carnahan]

I’ve seen cotangent appear “in nature” much more than some of the other functions, for example in classical treatments of modular forms (perhaps because it is the log derivative of sin). For this reason, I think we should be hesitant to remove it simply for reasons of symmetry.

[Ruben Van de Velde]

Snir Broshi said:

Complex.cot = Complex.tan

Please make a pr, and for Real as well