6.1. Analytic class number formula for h-minus🔗

Let K=\mathbb{Q}(\zeta_p), K^+=\mathbb{Q}(\zeta_p)^+, and n=\frac{p-1}{2}. Then K has signature (0,n) and K^+ has signature (n,0).

6.1.1. The odd L-product as a residue quotient🔗

The factorisation of the cyclotomic Dedekind zeta function into Dirichlet L-functions gives \zeta_K(s)=\prod_{\chi \bmod p} L(s,\chi), where the product runs over all characters modulo p. The even characters are exactly the characters of \operatorname{Gal}(K^+/\mathbb{Q}), so similarly \zeta_{K^+}(s)=\prod_{\chi\bmod p,\ \chi\text{ even}} L(s,\chi). Dividing yields \frac{\zeta_K(s)}{\zeta_{K^+}(s)}=\prod_{\chi\text{ odd}}L(s,\chi). Since every odd character modulo p is non-trivial, every factor on the right is holomorphic at s=1. Taking residues at s=1 therefore gives the following.

Proposition6.1.1.1

Statement uses 3

Statement dependency previews

Preview

Definition 1.1.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

One has \prod_{\chi\text{ odd}} L(1,\chi) = \frac{\operatorname*{Res}_{s=1}\zeta_K(s)}{\operatorname*{Res}_{s=1}\zeta_{K^+}(s)}.

Definition 1.1.1 Definition 2.2.1 Definition 2.3.1

Lean code for Proposition6.1.1.1●1 theorem

theoremdefined in BernoulliRegular/ZetaFactorisation/Residue.lean

complete

theorem BernoulliRegular.residue_ready_factorization_even_odd.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] :
  NumberField.dedekindZeta_residue K =
    (BernoulliRegular.evenLProduct p 1 *
        BernoulliRegular.oddLProduct p 1).re

theorem BernoulliRegular.residue_ready_factorization_even_odd.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] :
  NumberField.dedekindZeta_residue K =
    (BernoulliRegular.evenLProduct p 1 *
        BernoulliRegular.oddLProduct p
          1).re

Proof for Proposition 6.1.1.1

uses 0

The quotient \zeta_K(s)/\zeta_{K^+}(s) has a removable singularity at s=1, because both numerator and denominator have simple poles there. Its value at s=1 is therefore the ratio of the residues. On the other hand this quotient is exactly the product of the odd Dirichlet L-functions, all of which are regular at s=1.

6.1.2. The relative class number formula🔗

The analytic class number formula gives \operatorname*{Res}_{s=1}\zeta_F(s) = \frac{2^{r_1(F)}(2\pi)^{r_2(F)}h_F R_F}{w_F\sqrt{|D_F|}} for every number field F, where R_F is the regulator, w_F the number of roots of unity, and D_F the discriminant. For the cyclotomic fields under consideration one uses the standard identities w_K=2p, \qquad w_{K^+}=2, \qquad R_K = 2^{n-1}R_{K^+}, \qquad |D_K|=p^n|D_{K^+}|. Combining these with the definition h^- = h_K/h_{K^+} gives the following.

Proposition6.1.2.1

Statement uses 5

Statement dependency previews

Preview

Definition 1.2.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

One has h^- = \frac{2p\,p^{n/2}}{(2\pi)^n}\prod_{\chi\text{ odd}}L(1,\chi).

Proposition 6.1.1.1 Theorem 1.6.4 Definition 1.2.1 Definition 1.2.2 Definition 1.6.3

Lean code for Proposition6.1.2.1●2 theorems

theoremdefined in BernoulliRegular/HMinus/ClassNumberFormula.lean

complete

theorem BernoulliRegular.hMinus_formula_via_residues.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd' : p ≠ 2) :
  ↑(BernoulliRegular.hMinus K) =
    NumberField.dedekindZeta_residue K *
        (↑(NumberField.Units.torsionOrder K) *
            √|↑(NumberField.discr K)| /
          (2 ^ NumberField.InfinitePlace.nrRealPlaces K *
              (2 * Real.pi) ^
                NumberField.InfinitePlace.nrComplexPlaces K *
            NumberField.Units.regulator K)) /
      (NumberField.dedekindZeta_residue
          ↥(NumberField.maximalRealSubfield K) *
        (↑(NumberField.Units.torsionOrder
                ↥(NumberField.maximalRealSubfield K)) *
            √|↑(NumberField.discr
                    ↥(NumberField.maximalRealSubfield K))| /
          (2 ^
                NumberField.InfinitePlace.nrRealPlaces
                  ↥(NumberField.maximalRealSubfield K) *
              (2 * Real.pi) ^
                NumberField.InfinitePlace.nrComplexPlaces
                  ↥(NumberField.maximalRealSubfield K) *
            NumberField.Units.regulator
              ↥(NumberField.maximalRealSubfield K))))

theorem BernoulliRegular.hMinus_formula_via_residues.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd' : p ≠ 2) :
  ↑(BernoulliRegular.hMinus K) =
    NumberField.dedekindZeta_residue K *
        (↑(NumberField.Units.torsionOrder
                K) *
            √|↑(NumberField.discr K)| /
          (2 ^
                NumberField.InfinitePlace.nrRealPlaces
                  K *
              (2 * Real.pi) ^
                NumberField.InfinitePlace.nrComplexPlaces
                  K *
            NumberField.Units.regulator
              K)) /
      (NumberField.dedekindZeta_residue
          ↥(NumberField.maximalRealSubfield
              K) *
        (↑(NumberField.Units.torsionOrder
                ↥(NumberField.maximalRealSubfield
                    K)) *
            √|↑(NumberField.discr
                    ↥(NumberField.maximalRealSubfield
                        K))| /
          (2 ^
                NumberField.InfinitePlace.nrRealPlaces
                  ↥(NumberField.maximalRealSubfield
                      K) *
              (2 * Real.pi) ^
                NumberField.InfinitePlace.nrComplexPlaces
                  ↥(NumberField.maximalRealSubfield
                      K) *
            NumberField.Units.regulator
              ↥(NumberField.maximalRealSubfield
                  K))))

Rearranging the analytic class number formulas for `K` and `K⁺` gives a
relative residue expression for `h⁻`. This isolates the remaining analytic
input needed for Theorem 43 to the identification of the `K⁺`-side residue
with the even-character product.

theoremdefined in BernoulliRegular/HMinus/LValueReduction/Final.lean

complete

theorem BernoulliRegular.hMinus_formula_of_residue_and_hPlus_cyclotomic_and_gauss.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] (hp_odd' : p ≠ 2)
  (hres :
    ↑(NumberField.dedekindZeta_residue K) =
      (∏ χ ∈ BernoulliRegular.evenNontrivialCharacters p,
          BernoulliRegular.evenLValueRhs p χ) *
        ∏ χ ∈ BernoulliRegular.oddCharacters p,
          DirichletCharacter.LFunction χ 1)
  (hplus :
    ↑(BernoulliRegular.hPlus K) =
      BernoulliRegular.cyclotomicHPlusFactor K *
        ∏ χ ∈ BernoulliRegular.evenNontrivialCharacters p,
          BernoulliRegular.evenLValueRhs p χ)
  (hgauss : BernoulliRegular.cyclotomicHGaussGoal p K) :
  ↑(BernoulliRegular.hMinus K) =
    2 * ↑p *
      ∏ χ ∈ BernoulliRegular.oddCharacters p,
        -(1 / 2) * BernoulliRegular.BernoulliGen χ⁻¹ 1

theorem BernoulliRegular.hMinus_formula_of_residue_and_hPlus_cyclotomic_and_gauss.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd' : p ≠ 2)
  (hres :
    ↑(NumberField.dedekindZeta_residue
          K) =
      (∏
          χ ∈
            BernoulliRegular.evenNontrivialCharacters
              p,
          BernoulliRegular.evenLValueRhs p
            χ) *
        ∏
          χ ∈
            BernoulliRegular.oddCharacters
              p,
          DirichletCharacter.LFunction χ
            1)
  (hplus :
    ↑(BernoulliRegular.hPlus K) =
      BernoulliRegular.cyclotomicHPlusFactor
          K *
        ∏
          χ ∈
            BernoulliRegular.evenNontrivialCharacters
              p,
          BernoulliRegular.evenLValueRhs p
            χ)
  (hgauss :
    BernoulliRegular.cyclotomicHGaussGoal
      p K) :
  ↑(BernoulliRegular.hMinus K) =
    2 * ↑p *
      ∏
        χ ∈
          BernoulliRegular.oddCharacters
            p,
        -(1 / 2) *
          BernoulliRegular.BernoulliGen
            χ⁻¹ 1

Proof for Proposition 6.1.2.1

uses 0

Applying the analytic class number formula to K and K^+ gives h_K = \operatorname*{Res}_{s=1}\zeta_K(s)\cdot \frac{w_K\sqrt{|D_K|}}{(2\pi)^n R_K} and h_{K^+} = \operatorname*{Res}_{s=1}\zeta_{K^+}(s)\cdot \frac{w_{K^+}\sqrt{|D_{K^+}|}}{2^n R_{K^+}}. Taking the quotient, h^- = \frac{\operatorname*{Res}_{s=1}\zeta_K(s)}{\operatorname*{Res}_{s=1}\zeta_{K^+}(s)} \cdot \frac{w_K}{w_{K^+}} \cdot \frac{2^n R_{K^+}}{(2\pi)^n R_K} \cdot \sqrt{\frac{|D_K|}{|D_{K^+}|}}. Substituting the four identities above gives h^- = \frac{2p\,p^{n/2}}{(2\pi)^n} \frac{\operatorname*{Res}_{s=1}\zeta_K(s)}{\operatorname*{Res}_{s=1}\zeta_{K^+}(s)}. Now apply Proposition 6.1.1.1.

6.1.3. The product of the odd Gauss sums🔗

For a primitive character \chi modulo p, write \tau(\chi)=\sum_{a\in \mathbb{Z}/p\mathbb{Z}}\chi(a)e^{2\pi i a/p}. The standard identity \tau(\chi)\tau(\chi^{-1}) = \chi(-1)p shows that each inverse pair of odd characters contributes -p to the product of all odd Gauss sums.

Lemma6.1.3.1

Statement uses 3

Statement dependency previews

Preview

Definition 2.3.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

One has \prod_{\chi\text{ odd}} \tau(\chi) = i^n p^{n/2}.

Definition 4.1.1 Proposition 4.1.2 Definition 2.3.1

Lean code for Lemma6.1.3.1●2 theorems

theoremdefined in BernoulliRegular/HMinus/LValueReduction/GaussProduct.lean

complete

theorem BernoulliRegular.rawGaussProduct (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp_odd' : p ≠ 2) :
  ∏ χ ∈ BernoulliRegular.oddCharacters p, gaussSum χ ZMod.stdAddChar =
    Complex.I ^ ((p - 1) / 2) * ↑√(↑p ^ ((p - 1) / 2))

theorem BernoulliRegular.rawGaussProduct (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (hp_odd' : p ≠ 2) :
  ∏ χ ∈ BernoulliRegular.oddCharacters p,
      gaussSum χ ZMod.stdAddChar =
    Complex.I ^ ((p - 1) / 2) *
      ↑√(↑p ^ ((p - 1) / 2))

**T023d6**: Merge the two `mod 4` branches into the clean raw odd
Gauss-product formula used downstream.

theoremdefined in BernoulliRegular/HMinus/LValueReduction/GaussProduct.lean

complete

theorem BernoulliRegular.cyclotomicHGaussGoal_holds.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd' : p ≠ 2) : BernoulliRegular.cyclotomicHGaussGoal p K

theorem BernoulliRegular.cyclotomicHGaussGoal_holds.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd' : p ≠ 2) :
  BernoulliRegular.cyclotomicHGaussGoal p
    K

**T023d7**: Package the raw odd Gauss-product formula as the exact
cyclotomic `hgauss` hypothesis consumed by the final `hMinus` assembly
theorem.

Proof for Lemma 6.1.3.1

uses 0

If p\equiv 1\pmod 4, then the quadratic character is even, so no odd character is self-inverse. The odd characters split into n/2 inverse pairs, each contributing -p. Therefore \prod_{\chi\text{ odd}}\tau(\chi)=(-p)^{n/2}=i^n p^{n/2}.

If p\equiv 3\pmod 4, then the quadratic character \lambda is odd and is the unique self-inverse odd character. The remaining odd characters split into (n-1)/2 inverse pairs, so \prod_{\chi\text{ odd}}\tau(\chi) = \tau(\lambda)(-p)^{(n-1)/2}. The classical quadratic Gauss sum evaluation gives \tau(\lambda)=i\sqrt p. Hence \prod_{\chi\text{ odd}}\tau(\chi) = i\sqrt p\,(-p)^{(n-1)/2} = i^n p^{n/2}.

Theorem6.1.3.2

Statement uses 4

Statement dependency previews

Preview

Definition 3.1.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Analytic formula for \hminus. The relative class number satisfies h^- = 2p\prod_{\chi\text{ odd}} \left(-\frac12\,B_{1,\chi^{-1}}\right).

Proposition 6.1.2.1 Corollary 5.2.2 Lemma 6.1.3.1 Definition 3.1.1

Lean code for Theorem6.1.3.2●1 theorem

theoremdefined in BernoulliRegular/HMinus/LValueReduction/Final.lean

complete

theorem BernoulliRegular.hMinus_formula.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd' : p ≠ 2) :
  ↑(BernoulliRegular.hMinus K) =
    2 * ↑p *
      ∏ χ ∈ BernoulliRegular.oddCharacters p,
        -(1 / 2) * BernoulliRegular.BernoulliGen χ⁻¹ 1

theorem BernoulliRegular.hMinus_formula.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd' : p ≠ 2) :
  ↑(BernoulliRegular.hMinus K) =
    2 * ↑p *
      ∏
        χ ∈
          BernoulliRegular.oddCharacters
            p,
        -(1 / 2) *
          BernoulliRegular.BernoulliGen
            χ⁻¹ 1

Diekmann Theorem 43: the relative class number of a cyclotomic field of
prime conductor is the odd-character Bernoulli product.

This is the explicit statement ultimately obtained by combining the cyclotomic
class-number formula with the odd and even `L(1, χ)` evaluations.

Proof for Theorem 6.1.3.2

uses 0

There are exactly n=(p-1)/2 odd characters modulo p. By Proposition 6.1.2.1, h^- = \frac{2p\,p^{n/2}}{(2\pi)^n} \prod_{\chi\text{ odd}}L(1,\chi). For each odd character \chi, Corollary 5.2.2 gives L(1,\chi)=\frac{\pi i\,\tau(\chi)}{p}\,B_{1,\chi^{-1}}. Multiplying over all odd characters yields \prod_{\chi\text{ odd}}L(1,\chi) = \left(\frac{\pi i}{p}\right)^n \left(\prod_{\chi\text{ odd}}\tau(\chi)\right) \left(\prod_{\chi\text{ odd}}B_{1,\chi^{-1}}\right). By Lemma 6.1.3.1, this becomes \prod_{\chi\text{ odd}}L(1,\chi) = \frac{\pi^n i^{2n}}{p^{n/2}} \prod_{\chi\text{ odd}}B_{1,\chi^{-1}} = \frac{\pi^n(-1)^n}{p^{n/2}} \prod_{\chi\text{ odd}}B_{1,\chi^{-1}}. Substituting back gives h^- = \frac{2p\,p^{n/2}}{(2\pi)^n} \cdot \frac{\pi^n(-1)^n}{p^{n/2}} \prod_{\chi\text{ odd}}B_{1,\chi^{-1}} = 2p\left(-\frac12\right)^n \prod_{\chi\text{ odd}}B_{1,\chi^{-1}}. Since there are exactly n odd characters, this is precisely 2p\prod_{\chi\text{ odd}} \left(-\frac12\,B_{1,\chi^{-1}}\right).