Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_HonestLDatum.lean

definition module

An axiomatic datum for -functions with functional equation

For an index type \iota (thought of as the places at which the Euler factor is good), an LDatum ι records: a norm q_i \in \mathbb{N} and two polynomials P_i, P_i^{\vee} \in \mathbb{C}[X] for each i (the Euler factor of the datum and of its dual); four multisets gammaR, gammaC, gammaRDual, gammaCDual of complex shifts; real numbers abscissa and center; and a natural number degree. From these, LFun is the unconditional infinite product \prod'_i\,\bigl(P_i(q_i^{-s})\bigr)^{-1} (Mathlib's tprod), LFunDual the same with P_i^{\vee}, and archFactor the finite product \prod_{\mu \in \mathrm{gammaR}} \Gamma_{\mathbb{R}}(s+\mu)\cdot\prod_{\mu \in \mathrm{gammaC}} \Gamma_{\mathbb{C}}(s+\mu), with archFactorDual built from the two dual multisets. A finite multiset bad of pairs (q,P) \in \mathbb{N} \times \mathbb{C}[X] gives badFactor bad s = \prod_{(q,P)} P(q^{-s}), and IsBadData bad asks q \ge 2 and P(0)=1 for each entry. Three predicates on a datum D follow: WellFormed (q_i \ge 2; each of P_i, P_i^{\vee} has constant term 1 and degree at most degree; every shift \mu in any of the four multisets satisfies -\operatorname{Re}\mu \le abscissa); Converges (for \operatorname{Re} s > abscissa, the families \|P_i(q_i^{-s})-1\| and \|P_i^{\vee}(q_i^{-s})-1\| are summable and both products LFun s, LFunDual s are nonzero); and BoundedOnStrips Λ, that \Lambda be bounded on each vertical strip a \le \operatorname{Re} s \le b. Finally IsNice conjoins WellFormed and Converges with the existence of bad data on both sides, a number \varepsilon \in \mathbb{C}, a conductor N > 0 and entire functions \Lambda, \Lambda^{\vee}, bounded on vertical strips, such that on \operatorname{Re} s > abscissa one has \Lambda(s)\,\mathrm{badFactor}(s) = \mathrm{archFactor}(s)\,L(s) and the dual identity, together with \Lambda(s) = \varepsilon N^{c-s}\Lambda^{\vee}(2c-s) for all s, where c = center. Thus the archimedean shifts, abscissa, centre and degree bound are pinned by the datum, while the ramified factors, root number, conductor and analytic continuations are existentially quantified. Three small lemmas record that the empty bad multiset gives badFactor \equiv 1 and satisfies IsBadData, and that archFactor reduces to the product of \Gamma_{\mathbb{R}}-factors when gammaC is empty.

Relation to Mathlib

The \Gamma-factors \Gamma_{\mathbb{R}} and \Gamma_{\mathbb{C}} are Mathlib's Complex.Gammaℝ and Complex.Gammaℂ, and the Euler product is Mathlib's tprod; Mathlib has no general notion of an L-function with functional equation, so the LDatum structure and the predicates on it are the project's own.

Where it is used

The structure provides the interface through which the analytic properties of automorphic L-functions — meromorphic continuation, boundedness on vertical strips and the functional equation relating a datum to its dual — enter the Langlands–Tunnell part of the argument, without any number field or automorphic representation being named in the datum itself.

References

  1. H. Jacquet and R. P. Langlands, Automorphic Forms on GL(2), Lecture Notes in Mathematics 114, Springer, 1970
  2. H. Iwaniec and E. Kowalski, Analytic Number Theory, American Mathematical Society Colloquium Publications 53, 2004, Chapter 5

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_HonestLDatum.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.Analysis.SpecialFunctions.Gamma.Deligne ↗

noncomputable section

open Complex Polynomial

namespace LanglandsTunnell

structure LDatum (ι : Type*) where

  norm : ι → ℕ

  euler : ι → ℂ[X]

  dual : ι → ℂ[X]

  gammaR : Multiset ℂ

  gammaC : Multiset ℂ

  gammaRDual : Multiset ℂ

  gammaCDual : Multiset ℂ

  abscissa : ℝ

  center : ℝ

  degree : ℕ

namespace LDatum

variable {ι : Type*} (D : LDatum ι)

def LFun (s : ℂ) : ℂ :=
  ∏' i, ((D.euler i).eval ((D.norm i : ℂ) ^ (-s)))⁻¹

def LFunDual (s : ℂ) : ℂ :=
  ∏' i, ((D.dual i).eval ((D.norm i : ℂ) ^ (-s)))⁻¹

def archFactor (s : ℂ) : ℂ :=
  (D.gammaR.map fun μ => Gammaℝ (s + μ)).prod * (D.gammaC.map fun μ => Gammaℂ (s + μ)).prod

def archFactorDual (s : ℂ) : ℂ :=
  (D.gammaRDual.map fun μ => Gammaℝ (s + μ)).prod *
    (D.gammaCDual.map fun μ => Gammaℂ (s + μ)).prod

def badFactor (bad : Multiset (ℕ × ℂ[X])) (s : ℂ) : ℂ :=
  (bad.map fun x => x.2.eval ((x.1 : ℂ) ^ (-s))).prod

def IsBadData (bad : Multiset (ℕ × ℂ[X])) : Prop :=
  ∀ x ∈ bad, 2 ≤ x.1 ∧ x.2.coeff 0 = 1

def WellFormed : Prop :=
  (∀ i, 2 ≤ D.norm i) ∧
  (∀ i, (D.euler i).coeff 0 = 1 ∧ (D.euler i).natDegree ≤ D.degree ∧
    (D.dual i).coeff 0 = 1 ∧ (D.dual i).natDegree ≤ D.degree) ∧
  (∀ μ ∈ D.gammaR, -μ.re ≤ D.abscissa) ∧ (∀ μ ∈ D.gammaC, -μ.re ≤ D.abscissa) ∧
  (∀ μ ∈ D.gammaRDual, -μ.re ≤ D.abscissa) ∧ (∀ μ ∈ D.gammaCDual, -μ.re ≤ D.abscissa)

def Converges : Prop :=
  ∀ s : ℂ, D.abscissa < s.re →
    Summable (fun i => ‖(D.euler i).eval ((D.norm i : ℂ) ^ (-s)) - 1‖) ∧
    Summable (fun i => ‖(D.dual i).eval ((D.norm i : ℂ) ^ (-s)) - 1‖) ∧
    D.LFun s ≠ 0 ∧ D.LFunDual s ≠ 0

def BoundedOnStrips (Λ : ℂ → ℂ) : Prop :=
  ∀ a b : ℝ, ∃ C : ℝ, ∀ s : ℂ, a ≤ s.re → s.re ≤ b → ‖Λ s‖ ≤ C

def IsNice : Prop :=
  D.WellFormed ∧ D.Converges ∧
  ∃ (bad badDual : Multiset (ℕ × ℂ[X])) (ε : ℂ) (N : ℝ) (Λ Λd : ℂ → ℂ),
    IsBadData bad ∧ IsBadData badDual ∧ 0 < N ∧
    Differentiable ℂ Λ ∧ Differentiable ℂ Λd ∧
    BoundedOnStrips Λ ∧ BoundedOnStrips Λd ∧
    (∀ s : ℂ, D.abscissa < s.re → Λ s * badFactor bad s = D.archFactor s * D.LFun s) ∧
    (∀ s : ℂ, D.abscissa < s.re →
      Λd s * badFactor badDual s = D.archFactorDual s * D.LFunDual s) ∧
    (∀ s : ℂ, Λ s = ε * (N : ℂ) ^ ((D.center : ℂ) - s) * Λd (2 * (D.center : ℂ) - s))

@[simp] theorem badFactor_zero (s : ℂ) : badFactor 0 s = 1 := by
  simp [badFactor]

theorem isBadData_zero : IsBadData 0 := fun _ h => (Multiset.notMem_zero _ h).elim

theorem archFactor_of_gammaC_eq_zero (hC : D.gammaC = 0) (s : ℂ) :
    D.archFactor s = (D.gammaR.map fun μ => Gammaℝ (s + μ)).prod := by
  simp [archFactor, hC]

end LDatum

end LanglandsTunnell

end

Statements phrased using this module (52)