Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: small lemmas about moebius #11770

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat: small lemmas about moebius #11770

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 14 additions & 5 deletions Mathlib/NumberTheory/ArithmeticFunction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1073,12 +1073,17 @@ theorem moebius_ne_zero_iff_squarefree {n : ℕ} : μ n ≠ 0 ↔ Squarefree n :
· simp [h, pow_ne_zero]
#align nat.arithmetic_function.moebius_ne_zero_iff_squarefree ArithmeticFunction.moebius_ne_zero_iff_squarefree

theorem moebius_eq_or (n : ℕ) : μ n = 0 ∨ μ n = 1 ∨ μ n = -1 := by
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To me this looks like an argument to change the return type to be SignType

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't this just add yet another layer of coercions that you have to translate everything through whenever you want to do arithmetic with μ?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To push this further, I guess one could argue that ArithmeticFunction.zeta should take values in Fin 2...

Copy link
Member

@eric-wieser eric-wieser Apr 1, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suspect that the coercions aren't really a problem; and in exchange, you get results like this and the abs one for free

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(if the coercions were really that bad, then presumably SignType wouldn't exist at all!)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#10883. See also #10920, which was some API additions for SignType which I had to add to get #10883 working.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW, I just had a stab at reimplementing μ to be SignType-valued, just to check how bad it would be. It's every bit as bad as I expected. Literally every single lemma in the library about μ would need to be rewritten, with clunkier statements and longer proofs. We'd also need to add a whole load of tedious boilerplate code about coercions ArithmeticFunction SignType → ArithmeticFunction R for appropriate R, and compatibility of these with morphisms between R's. This is really, really not the way to go.

Copy link
Member

@eric-wieser eric-wieser Apr 1, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the cross-links. I'll have a think about this some more later, but actually changing this probably isn't a blocker for this PR (I'll let another maintainer decide).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW, I just had a stab at reimplementing μ to be SignType-valued, just to check how bad it would be

Would you mind sharing the branch with this stab on? No need to PR it, but if you put in the work it's nice to refer back to if this comes up again in future.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I deleted it, sorry.

simp only [moebius, coe_mk]
split_ifs
· right
exact neg_one_pow_eq_or ..
· left
rfl

theorem moebius_ne_zero_iff_eq_or {n : ℕ} : μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1 := by
constructor <;> intro h
· rw [moebius_ne_zero_iff_squarefree] at h
rw [moebius_apply_of_squarefree h]
apply neg_one_pow_eq_or
· rcases h with (h | h) <;> simp [h]
have := moebius_eq_or n
aesop
#align nat.arithmetic_function.moebius_ne_zero_iff_eq_or ArithmeticFunction.moebius_ne_zero_iff_eq_or

theorem moebius_sq_eq_one_of_squarefree {l : ℕ} (hl : Squarefree l) : μ l ^ 2 = 1 := by
Expand All @@ -1100,6 +1105,10 @@ theorem abs_moebius {n : ℕ} :
· exact abs_moebius_eq_one_of_squarefree h
· simp only [moebius_eq_zero_of_not_squarefree h, abs_zero]

theorem abs_moebius_le_one {n : ℕ} : |μ n| ≤ 1 := by
rw [abs_moebius, apply_ite (· ≤ 1)]
simp

theorem moebius_apply_prime {p : ℕ} (hp : p.Prime) : μ p = -1 := by
rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]
#align nat.arithmetic_function.moebius_apply_prime ArithmeticFunction.moebius_apply_prime
Expand Down
Loading