Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_AnalyticGates.lean

definition module

Analytic gates: twisted Dirichlet sums and a Tauberian hypothesis

Throughout, L is a number field that is Galois over \mathbb{Q}. Three predicates are introduced, each packaging an analytic condition as a named hypothesis.

OrderEightNonvanishing L asserts: for every \sigma \in \mathrm{Gal}(L/\mathbb{Q}) of order exactly 8, every finite set S_0 of naturals, every primitive eighth root of unity \zeta \in \mathbb{C} and every j \in oddJ =\{1,3,5,7\}, the function s \mapsto \sum_{\ell} \Bigl(\sum_{m=0}^{7} \mathrm{labelledCount}(\sigma,S_0,m,\ell)\,\zeta^{jm}\Bigr)\ell^{-s} is o\bigl(\log((s-1)^{-1})\bigr) along the filter of right-hand neighbourhoods of 1 in \mathbb{R}. Here labelledCount σ S₀ m ℓ is 0 for \ell \in S_0 and for \ell not prime, and otherwise counts the primes \mathfrak{q} of the ring of integers of the fixed field of \langle \sigma \rangle lying over (\ell) \subseteq \mathbb{Z} with residue field of cardinality exactly \ell, such that some prime Q of \mathcal{O}_L lies over both \mathfrak{q} and (\ell), has trivial inertia subgroup, and has arithmetic Frobenius equal to \sigma^m. The sums are unconditional tsums, so no summability is assumed.

OrderEightBounded L is the same statement with o(\log((s-1)^{-1})) replaced by O(1) as s \to 1^{+}.

TauberianHypothesis L asserts, for every \sigma and every real c: if \sum_{\ell} \mathrm{classIndicator}(\sigma,\ell)\,\ell^{-s} converges for all s > 1 and \sum_{\ell} \mathrm{classIndicator}(\sigma,\ell)\,\ell^{-s} + c\log(s-1) is O(1) as s \to 1^{+}, then the proportion of \ell < N with \mathrm{classIndicator}(\sigma,\ell) = 1 among the primes < N tends to c as N \to \infty. Here classIndicator σ ℓ is 1 precisely when \ell is prime and some prime Q of \mathcal{O}_L over (\ell) has trivial inertia and arithmetic Frobenius conjugate to \sigma, and 0 otherwise. Thus the predicate converts a Dirichlet-density estimate into a natural density among the primes.

Relation to Mathlib

Mathlib supplies the asymptotic relations =o/=O along 𝓝[>] 1, primitive roots of unity, and the arithmetic Frobenius and inertia subgroup of a prime in a Galois extension; the three predicates here, and the counting functions they use, are the project's own, Mathlib having no notion of Dirichlet or natural density of Frobenius classes.

Where it is used

These predicates are the analytic inputs to a Chebotarev-style density argument on the Galois side of the Langlands–Tunnell step: the twisted sums over eighth roots of unity control the contribution of order-eight elements, and the Tauberian hypothesis turns the resulting Dirichlet-density estimate for the Frobenius class of \sigma into a count of primes, which is what produces primes with prescribed Frobenius behaviour.

References

  1. J.-P. Serre, Quelques applications du théorème de densité de Chebotarev, Publications Mathématiques de l'IHÉS 54 (1981), 323–401
  2. W. Narkiewicz, Elementary and Analytic Theory of Algebraic Numbers, 3rd edition, Springer, 2004
  3. J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_LanglandsTunnell_AnalyticGates.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_LanglandsTunnell_TowerCounting
import Mathlib.Analysis.Asymptotics.Lemmas ↗
import Mathlib.Analysis.SpecialFunctions.Log.Basic ↗
import Mathlib.Analysis.SpecialFunctions.Pow.Real ↗
import Mathlib.Analysis.Complex.Basic ↗
import Mathlib.RingTheory.RootsOfUnity.Complex ↗
import Mathlib.Topology.Algebra.InfiniteSum.Real ↗

set_option autoImplicit false

namespace LanglandsTunnell

open NumberField FrobeniusDensity Filter Topology Asymptotics

def OrderEightNonvanishing (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L] : Prop :=
  ∀ (σ : L ≃ₐ[ℚ] L), orderOf σ = 8 →
  ∀ (S₀ : Finset ℕ) (ζ : ℂ), IsPrimitiveRoot ζ 8 →
  ∀ j ∈ oddJ, (fun s : ℝ => ∑' ℓ : ℕ,
    (∑ m : Fin 8, (labelledCount σ S₀ m ℓ : ℂ) * ζ ^ (j * m.val)) *
    (↑((ℓ : ℝ) ^ (-s)) : ℂ)) =o[𝓝[>] 1] (fun s : ℝ => Real.log ((s - 1)⁻¹))

def OrderEightBounded (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L] : Prop :=
  ∀ (σ : L ≃ₐ[ℚ] L), orderOf σ = 8 →
  ∀ (S₀ : Finset ℕ) (ζ : ℂ), IsPrimitiveRoot ζ 8 →
  ∀ j ∈ oddJ, (fun s : ℝ => ∑' ℓ : ℕ,
    (∑ m : Fin 8, (labelledCount σ S₀ m ℓ : ℂ) * ζ ^ (j * m.val)) *
    (↑((ℓ : ℝ) ^ (-s)) : ℂ)) =O[𝓝[>] 1] (fun _ => (1 : ℝ))

def TauberianHypothesis (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L] : Prop :=
  ∀ (σ : L ≃ₐ[ℚ] L) (c : ℝ),
    ((∀ s : ℝ, 1 < s → Summable (fun ℓ : ℕ => (classIndicator σ ℓ : ℝ) * (ℓ : ℝ) ^ (-s))) ∧
     (fun s : ℝ => (∑' ℓ : ℕ, (classIndicator σ ℓ : ℝ) * (ℓ : ℝ) ^ (-s))
       + c * Real.log (s - 1)) =O[𝓝[>] 1] (fun _ => (1 : ℝ)))
    → Tendsto
        (fun N : ℕ =>
          (((Finset.range N).filter (fun ℓ => classIndicator σ ℓ = 1)).card : ℝ)
          / (((Finset.range N).filter Nat.Prime).card : ℝ))
        atTop (𝓝 c)

end LanglandsTunnell

Statements phrased using this module (1)