Skip to content

Commit

Permalink
make BadChar and associated decls private
Browse files Browse the repository at this point in the history
  • Loading branch information
MichaelStollBayreuth committed Oct 31, 2024
1 parent 0098e07 commit cb12d0c
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean
Original file line number Diff line number Diff line change
Expand Up @@ -84,13 +84,13 @@ lemma zetaMul_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (n : ℕ
### "Bad" Dirichlet characters
Our goal is to show that `L(χ, 1) ≠ 0` when `χ` is a (nontrivial) quadratic Dirichlet character.
To do that, we package the contradictory properties in a structure `DirichletCharacter.BadChar`
and derive further statements eventually leading to a contradiction.
To do that, we package the contradictory properties in a (private) structure
`DirichletCharacter.BadChar` and derive further statements eventually leading to a contradiction.
-/

/-- The object we're trying to show doesn't exist: A nontrivial quadratic Dirichlet character
whose L-function vanishes at `s = 1`. -/
structure BadChar (N : ℕ) [NeZero N] where
private structure BadChar (N : ℕ) [NeZero N] where
/-- The character we want to show cannot exist. -/
χ : DirichletCharacter ℂ N
χ_ne : χ ≠ 1
Expand All @@ -106,19 +106,19 @@ namespace BadChar
/-- The product of the Riemann zeta function with the L-function of `B.χ`.
We will show that `B.F (-2) = 0` but also that `B.F (-2)` must be positive,
giving the desired contradiction. -/
noncomputable
private noncomputable
def F (B : BadChar N) : ℂ → ℂ :=
Function.update (fun s : ℂ ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)

lemma F_differentiableAt_of_ne (B : BadChar N) {s : ℂ} (hs : s ≠ 1) :
private lemma F_differentiableAt_of_ne (B : BadChar N) {s : ℂ} (hs : s ≠ 1) :
DifferentiableAt ℂ B.F s := by
apply DifferentiableAt.congr_of_eventuallyEq
· exact (differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)
· filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_noteq ht ..

open ArithmeticFunction in
/-- `B.F` agrees with the L-series of `zetaMul χ` on `1 < s.re`. -/
lemma F_eq_LSeries (B : BadChar N) {s : ℂ} (hs : 1 < s.re) :
private lemma F_eq_LSeries (B : BadChar N) {s : ℂ} (hs : 1 < s.re) :
B.F s = LSeries B.χ.zetaMul s := by
rw [F, zetaMul, ← coe_mul, LSeries_convolution']
· have hs' : s ≠ 1 := fun h ↦ by simp only [h, one_re, lt_self_iff_false] at hs
Expand All @@ -132,7 +132,7 @@ lemma F_eq_LSeries (B : BadChar N) {s : ℂ} (hs : 1 < s.re) :
ZMod.LSeriesSummable_of_one_lt_re B.χ hs

/-- If `χ` is a bad character, then `F` is an entire function. -/
lemma F_differentiable (B : BadChar N) : Differentiable ℂ B.F := by
private lemma F_differentiable (B : BadChar N) : Differentiable ℂ B.F := by
intro s
rcases ne_or_eq s 1 with hs | rfl
· exact B.F_differentiableAt_of_ne hs
Expand All @@ -157,7 +157,7 @@ lemma F_differentiable (B : BadChar N) : Differentiable ℂ B.F := by

/-- The trivial zero at `s = -2` of the zeta function gives that `F (-2) = 0`.
This is used later to obtain a contradction. -/
lemma F_neg_two (B : BadChar N) : B.F (-2 : ℝ) = 0 := by
private lemma F_neg_two (B : BadChar N) : B.F (-2 : ℝ) = 0 := by
have := riemannZeta_neg_two_mul_nat_add_one 0
rw [Nat.cast_zero, zero_add, mul_one] at this
rw [F, ofReal_neg, ofReal_ofNat, Function.update_noteq (mod_cast (by omega : (-2 : ℤ) ≠ 1)),
Expand Down

0 comments on commit cb12d0c

Please sign in to comment.