2 * n * π vs n * (2 * π)

Stream: mathlib4

[Yury G. Kudryashov]

Some lemmas (e.g., docs#Real.cos_eq_one_iff) use n * (2 * π), other lemmas (e.g., docs#Complex.cos_eq_cos_iff) use 2 * n * π. IMHO, we should write it the same way everywhere. What do you think?

[Yury G. Kudryashov]

/poll 2 * n * π or n * (2 * π)?
change all lemmas to 2 * n * π
change all lemmas to n * (2 * π)
leave as is

[Frédéric Dupuis]

n being sandwiched between two constants feels more awkward to use.

[Yury G. Kudryashov]

Also, see docs#Complex.cos_eq_zero_iff

[Yury G. Kudryashov]

/poll How should we spell (2 * k + 1) * π / 2?
(2 * k + 1) * π / 2
π / 2 + k * π

[Yury G. Kudryashov]

#xy: I want to add lemmas Complex.cos_eq_one_iff, cos_eq_neg_one_iff etc for the cases when cos_eq_cos_iff doesn't immediately give the answer we want. So, I want to have a standard way to spell all these angles.

[Yury G. Kudryashov]

Frédéric Dupuis said:

n being sandwiched between two constants feels more awkward to use.

OTOH, we have 2 * n a.k.a. "any even number". BTW, another way to spell this lemma is ∃ k, Even k ∧ k * π = x

[Ruben Van de Velde]

n * \tau?

[Yury G. Kudryashov]

Do you really want to introduce yet another constant?

[Ruben Van de Velde]

No

[Yaël Dillies]

I mean this is where you start feeling like tau isn't a bad idea after all...

[Yaël Dillies]

I strongly refuse to break up the 2 * π appearing in those theorems, and as I said previously I think we should introduce a new definition (an abbrev would be fine) to enforce it.

[Eric Rodriguez]

Yaël Dillies said:

I strongly refuse to break up the 2 * π

why?

[Yury G. Kudryashov]

@Yaël Dillies How would you spell docs#Complex.sin_eq_sin_iff and docs#Complex.cos_eq_zero_iff?

[Jeremy Tan]

Eric Rodriguez said:
why?

I would not break up 2 * pi either since it has meaning by itself in as many places as pi / 2 does

[Antoine Chambert-Loir]

Yaël Dillies said:

I strongly refuse to break up the 2 * π appearing in those theorems, and as I said previously I think we should introduce a new definition (an abbrev would be fine) to enforce it.

What about $2 i \pi$ ?

[Yury G. Kudryashov]

docs#Complex.exp_eq_exp_iff_exists_int uses n * (2 * π * I)

[Yury G. Kudryashov]

It looks like I'm the only one who prefers π / 2 + n * π. My reason: this way the period is separate from the "base value".

[Antoine Chambert-Loir]

And I know docs#mul_assoc is not ‘simp‘ but what is the preferred way of writing ‘a * b * c‘ in lemmas?

[Yury G. Kudryashov]

I usually write a * b * c unless there is a reason to group b * c.

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

It looks like I'm the only one who prefers π / 2 + n * π. My reason: this way the period is separate from the "base value".

That's a good reason. It suggests the lemmas be written in one style but an adequate ‘iff‘ stuff allows to rewrite them as desired.

[Jireh Loreaux]

Yury G. Kudryashov said:

It looks like I'm the only one who prefers π / 2 + n * π. My reason: this way the period is separate from the "base value".

This reasoning caused me to change my vote.

[Jeremy Tan]

Jireh Loreaux said:

Yury G. Kudryashov said:

It looks like I'm the only one who prefers π / 2 + n * π. My reason: this way the period is separate from the "base value".

This reasoning caused me to change my vote.

I changed my vote too; I'm trying to define the complex arctangent using the log definition and the "n * period + offset" formulation is slightly easier with the algebraic manipulation

[Jeremy Tan]

import Mathlib.Analysis.SpecialFunctions.Complex.Log

noncomputable section

namespace Complex

open scoped Real

/-- The complex arctangent, defined through the complex logarithm. -/
def arctan (z : ℂ) : ℂ := -I / 2 * log ((I - z) / (I + z))

[Jeremy Tan]

I've defined the complex arctangent at #9889

[Yaël Dillies]

@Yury G. Kudryashov said:

Yaël Dillies How would you spell docs#Complex.sin_eq_sin_iff and docs#Complex.cos_eq_zero_iff?

x ≡ y |PMOD (2 * π)] ∨ x + y ≡ π [PMOD (2 * π)]

[Yaël Dillies]

Yury G. Kudryashov said:

It looks like I'm the only one who prefers π / 2 + n * π. My reason: this way the period is separate from the "base value".

I would say x ≡ π / 2 [PMOD π] there. Then you can avoid arguing about spelling by adding more docs#AddCommGroup.ModEq API instead.

[Yury G. Kudryashov]

This is a nice way to spell it.

[Yaël Dillies]

For context, AddCommGroup.ModEq was added while David Loeffler wanted to port the preliminary material for zeta function and it made it just about before the port reached its file. As such, it is pretty new and there are probably many potential use cases in mathlib that we haven't exploited yet.

[Yury G. Kudryashov]

BTW, why ModEq isn't defined by reusing leftCosets?

[Eric Wieser]

The definition was rushed during the port to try and avoid causing too much issue in mathlib4

[Eric Wieser]

So we defined it the fastest way, not necessarily the best way

[Yaël Dillies]

Note that the file containing docs#LeftCosetEquivalence is a mess and should probably be deleted entirely and the material spread across several (possibly existing) files.

[Yaël Dillies]

Also note that it would be good for a ≡ b [PMOD n] to mean the right thing when a b n : ℕ. This is currently not the case.

[Yury G. Kudryashov]

... and to be an addCon

[Yaël Dillies]

It's just a matter of changing the definition from ∃ z : ℤ, b - a = z • p to ∃ m n : ℕ, a + m • p = b + n • p.

[Yaël Dillies]

Then we could actually phase out docs#Nat.ModEq and docs#Int.ModEq entirely, which I think is nice.

[Michael Stoll]

... and then rename PMOD to MOD?

[Yaël Dillies]

Yes of course! That was the plan all along :wink:

[Yury G. Kudryashov]

I added PMOD answers to the polls

[Eric Wieser]

Another option is to use equalities inReal.angle or addCircle π (which could be given a name)

[Yury G. Kudryashov]

We have lemmas about complex numbers as well.

[Eric Wieser]

Can you give an example?

[Eric Wieser]

PMOD feels like it might be quite strange there

[Yury G. Kudryashov]

docs#Complex.cos_eq_cos_iff

[Eric Wieser]

That raises another question; 2 * ↑k * ↑Real.pi or ↑(2 * k * Real.pi) or ↑k * ↑(2 * Real.pi)or ...

[Yury G. Kudryashov]

Coercion outside of multiplication makes it non-simp-normal form.

[Eric Wieser]

You could write it as (2 * k * Real.pi) +ᵥ x to fix that... (maybe that instance doesn't exist, but it probably should)

[Yury G. Kudryashov]

... and it should simplify to ↑a + b as we do it for docs#nsmul_eq_mul

[Yury G. Kudryashov]

What I like about PMOD is that we can have dot-notation API about it.

[Eric Wieser]

What's the PMOD spelling of that lemma?

[Yury G. Kudryashov]

x ≡ y [PMOD 2 * π] ∨ x ≡ -y [PMOD 2 * π]