feat(NumberTheory/Bernoulli): von Staudt-Clausen theorem

[seewoo5]

---

Rado's proof ("A New Proof of a Theorem of v. Staudt", JLMS 1935) of von Staudt-Clausen theorem. Initially written by AxiomProver (see commit 97a308e) with further golfs with Claude and Codex.

[github-actions]

PR summary 216d48f3de

Import changes exceeding 2%

%	File
+25.38%	Mathlib.NumberTheory.Bernoulli

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Bernoulli	1639	2055	+416 (+25.38%)

Import changes for all files

Files	Import difference
8 files Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion	6
Mathlib.NumberTheory.LSeries.HurwitzZetaValues	77
Mathlib.NumberTheory.ZetaValues	78
Mathlib.NumberTheory.BernoulliPolynomials	414
Mathlib.NumberTheory.Bernoulli	416

---

Declarations diff

+ bernoulli_add_indicator_den_not_dvd
+ bernoulli_add_indicator_eq_sub
+ choose_two_mul_succ_mul_div_eq
+ exists_int_sum_pow_add_indicator_eq
+ factorization_succ_le_sub_one
+ faulhaber_sum_div_prime_eq
+ pIntegral
+ pIntegral_bernoulli_even_term
+ pIntegral_bernoulli_one_term
+ pIntegral_choose_mul_pow_div
+ pIntegral_faulhaber_sum
+ pIntegral_iff_not_dvd
+ pIntegral_mul
+ pIntegral_ofInt
+ pIntegral_pow_div
+ pIntegral_sub
+ pIntegral_sum
+ prod_one_div_prime_den_coprime
+ sum_den_dvd_prod_den
+ sum_one_div_prime_eq_indicator_div_add
+ sum_pow_add_indicator_eq_zero
+ sum_pow_filter_eq_faulhaber
+ vonStaudtIndicator
+ vonStaudt_clausen
+ vonStaudt_sum_den_not_dvd

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[seewoo5]

I made some changes addressing comments but still WIP - I'll re open when I think it is more ready (probably in few days).

[seewoo5]

@MichaelStollBayreuth I think I addressed some parts of your comments - I can do further cleanups, but it might be better to get second round of feedbacks. The proofs also shortened from 500-ish lines to 400-ish lines.

[MichaelStollBayreuth]

You'll have to merge master to fix the build. (git fetch upstream; git merge upstream/master)

[MichaelStollBayreuth]

If you make this an abbrev instead of a def, then you can inline the proofs of all the private pIntegral_... lemmas where they are currently used. This saves a lot of boilerplate.

[MichaelStollBayreuth]

Suggested change

	private lemma sum_den_dvd_prod_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :
	private lemma den_sum_dvd_prod_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :

(it's really Rat.den (∑ i ∈ s, f i) ...)

[MichaelStollBayreuth]

Suggested change

	(hv : M.factorization p ≤ N) : pIntegral p ((p : ℚ)^N / M) := by
	(hv : M.factorization p ≤ N) : pIntegral p ((p : ℚ) ^ N / M) := by

[MichaelStollBayreuth]

Suggested change

	/-- Indicator function that is `1` if `(p - 1) ∣ k` and `0` otherwise. -/
	/- Indicator function that is `1` if `(p - 1) ∣ k` and `0` otherwise. -/

Docstrings for private declarations don't make sense (private declarations are not shown in the docs anyway), so this should just be a regular comment. Similarly below.

[MichaelStollBayreuth]

It may make sense to introduce an abbrev for the Finset of all primes q < 2*k+2 such that q-1 ∣ 2*k and use that.

[MichaelStollBayreuth]

Suggested change

	exact absurd hdvd (by letI : Fact p.Prime := ⟨hp⟩; exact vonStaudt_sum_den_not_dvd k p hk)
	exact absurd hdvd (by let : Fact p.Prime := ⟨hp⟩; exact vonStaudt_sum_den_not_dvd k p hk)

In Lean 4, the "I" in letI/haveI has nothing to do with instances (terms of class type in the context are always available as instances), rather, "I" means "inline", which is unnecessary in proofs.