The proof
Source
Main.lean · 393097 lines · 17.7 MB
Showing the first 500 of 393097 lines. The whole file is 17.7 MB; download it to read the rest.
end Bounty
section
-- Source module: OAI.NumberTheory.DirichletL.Arithmetic.EisensteinCoordinates
namespace OAI
open scoped BigOperators
namespace ShortDraft
abbrev EisensteinCoordinates := ℤ × ℤ
def eisensteinMul (x y : EisensteinCoordinates) : EisensteinCoordinates :=
(x.1 * y.1 - x.2 * y.2, x.1 * y.2 + x.2 * y.1 - x.2 * y.2)
def eisensteinNorm (x : EisensteinCoordinates) : ℤ :=
x.1 ^ 2 - x.1 * x.2 + x.2 ^ 2
theorem eisenstein_norm_mul (x y : EisensteinCoordinates) :
eisensteinNorm (eisensteinMul x y) = eisensteinNorm x * eisensteinNorm y := by
rcases x with ⟨a, b⟩
rcases y with ⟨c, d⟩
dsimp [eisensteinNorm, eisensteinMul]
ring
theorem eisenstein_norm_nonneg (x : EisensteinCoordinates) :
0 ≤ eisensteinNorm x := by
rcases x with ⟨a, b⟩
dsimp [eisensteinNorm]
nlinarith [sq_nonneg (2 * a - b), sq_nonneg b]
theorem eisenstein_norm_eq_zero_iff (x : EisensteinCoordinates) :
eisensteinNorm x = 0 ↔ x = (0, 0) := by
rcases x with ⟨a, b⟩
dsimp [eisensteinNorm]
constructor
· intro h
have hb : b = 0 := by
nlinarith [sq_nonneg (2 * a - b), sq_nonneg b]
have ha : a = 0 := by
subst b
nlinarith [sq_nonneg a]
simp [ha, hb]
· intro h
simp_all
def DirichletTarget : Prop :=
∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℂ),
(23 / 24 : ℝ) < s.re → ¬ (χ = 1 ∧ s = 1) →
DirichletCharacter.LFunction χ s ≠ 0
theorem dirichlet_target_of_one_le_re
(q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℂ)
(hs : 1 ≤ s.re) (hprincipal : ¬ (χ = 1 ∧ s = 1)) :
DirichletCharacter.LFunction χ s ≠ 0 := by
exact χ.LFunction_ne_zero_of_one_le_re (not_and_or.mp hprincipal) hs
private lemma square_le_two_squares {x y e : ℝ}
(hx : 0 ≤ x) (hy : 0 ≤ y) (he : 0 ≤ e) (h : x ≤ y + e) :
x ^ 2 ≤ 2 * y ^ 2 + 2 * e ^ 2 := by
have h₁ : 0 ≤ y + e - x := sub_nonneg.mpr h
have h₂ : 0 ≤ y + e + x := by nlinarith
have h₃ := mul_nonneg h₁ h₂
have h₄ := sq_nonneg (y - e)
nlinarith
theorem finite_row_extraction {α β : Type*} [DecidableEq α] [DecidableEq β]
(rows : Finset α) (primes : Finset β) (row : β → α)
(a : α → ℝ) (a₀ error bound : ℝ)
(ha₀ : 0 ≤ a₀) (ha : ∀ u, 0 ≤ a u) (herror : 0 ≤ error)
(hrows : primes.image row ⊆ rows)
(hinj : Set.InjOn row (primes : Set β))
(happrox : ∀ p ∈ primes, a₀ ≤ a (row p) + error)
(hmean : (∑ u ∈ rows, (a u) ^ 2) ≤ bound) :
(primes.card : ℝ) * a₀ ^ 2 ≤
2 * bound + 2 * (primes.card : ℝ) * error ^ 2 := by
have hselected : (∑ p ∈ primes, (a (row p)) ^ 2) ≤ bound := by
calc
(∑ p ∈ primes, (a (row p)) ^ 2) =
∑ u ∈ primes.image row, (a u) ^ 2 := by
rw [Finset.sum_image hinj]
_ ≤ ∑ u ∈ rows, (a u) ^ 2 :=
Finset.sum_le_sum_of_subset_of_nonneg hrows (by
intro u _ _
positivity)
_ ≤ bound := hmean
have hpoint (p : β) (hp : p ∈ primes) :
a₀ ^ 2 ≤ 2 * (a (row p)) ^ 2 + 2 * error ^ 2 :=
square_le_two_squares ha₀ (ha _) herror (happrox p hp)
have hsum :
(∑ p ∈ primes, a₀ ^ 2) ≤
∑ p ∈ primes, (2 * (a (row p)) ^ 2 + 2 * error ^ 2) :=
Finset.sum_le_sum hpoint
simp only [Finset.sum_add_distrib, ← Finset.mul_sum,
Finset.sum_const, nsmul_eq_mul] at hsum
nlinarith
theorem complex_row_extraction {α β : Type*} [DecidableEq α] [DecidableEq β]
(rows : Finset α) (primes : Finset β) (row : β → α)
(A : α → ℂ) (untwisted : α) (error bound : ℝ)
(herror : 0 ≤ error)
(hrows : primes.image row ⊆ rows)
(hinj : Set.InjOn row (primes : Set β))
(happrox : ∀ p ∈ primes, ‖A untwisted - A (row p)‖ ≤ error)
(hmean : (∑ u ∈ rows, ‖A u‖ ^ 2) ≤ bound) :
(primes.card : ℝ) * ‖A untwisted‖ ^ 2 ≤
2 * bound + 2 * (primes.card : ℝ) * error ^ 2 := by
apply finite_row_extraction rows primes row (fun u ↦ ‖A u‖)
‖A untwisted‖ error bound (norm_nonneg _) (fun u ↦ norm_nonneg _) herror
hrows hinj ?_ hmean
intro p hp
calc
‖A untwisted‖ = ‖(A untwisted - A (row p)) + A (row p)‖ := by
rw [sub_add_cancel]
_ ≤ ‖A untwisted - A (row p)‖ + ‖A (row p)‖ := norm_add_le _ _
_ ≤ ‖A (row p)‖ + error := by linarith [happrox p hp]
end ShortDraft
open MulChar AddChar
namespace ShortDraftLocal
variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]
omit [Fintype F] [DecidableEq F] in
theorem sextic_character_exponent (χ : MulChar F ℂ) (hχ : χ ^ 6 = 1) :
χ⁻¹ * χ⁻¹ ^ 2 = χ ^ 3 := by
calc
χ⁻¹ * χ⁻¹ ^ 2 = χ ^ (-3 : ℤ) := by group
_ = χ ^ 3 := by
calc
χ ^ (-3 : ℤ) = χ ^ ((-3 : ℤ) + 6) := by
rw [zpow_add, zpow_ofNat, hχ, mul_one]
_ = χ ^ 3 := by norm_num
theorem gaussSum_mulShift_any (χ : MulChar F ℂ) (ψ : AddChar F ℂ)
(hχ : χ ≠ 1) (a : F) :
gaussSum χ (ψ.mulShift a) = χ⁻¹ a * gaussSum χ ψ := by
by_cases ha : a = 0
· subst a
have hshift : ψ.mulShift (0 : F) = 1 := by
ext x
simp
rw [hshift, gaussSum_one_right hχ]
simp
· have hu : IsUnit a := isUnit_iff_ne_zero.mpr ha
simpa [hu.unit_spec] using gaussSum_mulShift_eq χ ψ hu.unit
theorem gaussSum_eq_units_sum (χ : MulChar F ℂ) (ψ : AddChar F ℂ) :
gaussSum χ ψ = ∑ y : Fˣ, χ (y : F) * ψ (y : F) := by
classical
have hzero : χ (0 : F) * ψ (0 : F) = 0 := by simp
calc
gaussSum χ ψ = ∑ x ∈ (Finset.univ : Finset F).erase 0, χ x * ψ x := by
simpa only [gaussSum, hzero, add_zero] using
(Finset.sum_erase_add (Finset.univ : Finset F)
(fun x => χ x * ψ x) (Finset.mem_univ (0 : F))).symm
_ = ∑ x : {x : F // x ≠ 0}, χ x * ψ x := by
apply Finset.sum_subtype
intro x
simp
_ = ∑ y : Fˣ, χ (y : F) * ψ (y : F) := by
apply (Fintype.sum_equiv (unitsEquivNeZero : Fˣ ≃ {x : F // x ≠ 0})
(fun y : Fˣ => χ (y : F) * ψ (y : F))
(fun x : {x : F // x ≠ 0} => χ x * ψ x) ?_).symm
intro y
rfl
theorem additive_unit_sum (ψ : AddChar F ℂ) (hψ : ψ ≠ 1) (a : F) :
(∑ y : Fˣ, ψ (a * (y : F))) =
if a = 0 then (Fintype.card Fˣ : ℂ) else -1 := by
classical
have hgauss : (∑ y : Fˣ, ψ (a * (y : F))) =
gaussSum (1 : MulChar F ℂ) (ψ.mulShift a) := by
rw [gaussSum_eq_units_sum]
simp only [MulChar.one_apply_coe, one_mul, AddChar.mulShift_apply]
rw [hgauss]
split_ifs with ha
· subst a
simp only [AddChar.mulShift_zero, gaussSum_one_one]
exact_mod_cast (Nat.card_eq_fintype_card (α := Fˣ))
· have hu : IsUnit a := isUnit_iff_ne_zero.mpr ha
have hshift : ψ.mulShift a ≠ 1 := by
intro heq
exact hψ ((AddChar.mulShift_unit_eq_one_iff ψ hu).mp heq)
exact gaussSum_one_left hshift
theorem sextic_fourth_mask (χ : MulChar F ℂ) (ψ : AddChar F ℂ)
(hχ : χ ^ 6 = 1) (hψ : ψ ≠ 1) (a : F) :
(∑ h : Fˣ, ((χ⁻¹) ^ 4 * (χ⁻¹) ^ 2) h *
ψ (a * ((h⁻¹ : Fˣ) : F))) =
if a = 0 then (Fintype.card Fˣ : ℂ) else -1 := by
classical
have hexp : ((χ⁻¹) ^ 4 * (χ⁻¹) ^ 2) = 1 := by
calc
((χ⁻¹) ^ 4 * (χ⁻¹) ^ 2) = (χ ^ 6)⁻¹ := by group
_ = 1 := by rw [hχ, inv_one]
rw [hexp]
simp only [MulChar.one_apply_coe, one_mul]
calc
(∑ h : Fˣ, ψ (a * ((h⁻¹ : Fˣ) : F))) =
∑ y : Fˣ, ψ (a * (y : F)) := by
apply Fintype.sum_equiv (Equiv.inv Fˣ)
intro h
simp
_ = _ := additive_unit_sum ψ hψ a
theorem active_zero_local_row (χ : MulChar F ℂ) (ψ : AddChar F ℂ)
(hχ₂ : χ ^ 2 ≠ 1) (ε x : F) :
(∑ h : Fˣ, ((χ⁻¹) ^ 2) (h : F) *
ψ ((ε * x) * ((h⁻¹ : Fˣ) : F))) =
(χ ^ 2)⁻¹ ε * gaussSum (χ ^ 2) ψ * (χ ^ 2)⁻¹ x := by
classical
have hquad : ((χ⁻¹) ^ 2)⁻¹ = χ ^ 2 := by group
calc
(∑ h : Fˣ, ((χ⁻¹) ^ 2) (h : F) *
ψ ((ε * x) * ((h⁻¹ : Fˣ) : F))) =
∑ y : Fˣ, (χ ^ 2) (y : F) * ψ ((ε * x) * (y : F)) := by
apply Fintype.sum_equiv (Equiv.inv Fˣ)
intro h
simp only [Equiv.inv_apply, Units.val_inv_eq_inv_val]
rw [← hquad, MulChar.inv_apply', inv_inv]
_ = gaussSum (χ ^ 2) (ψ.mulShift (ε * x)) := by
rw [gaussSum_eq_units_sum]
simp only [AddChar.mulShift_apply]
_ = (χ ^ 2)⁻¹ ε * gaussSum (χ ^ 2) ψ * (χ ^ 2)⁻¹ x := by
rw [gaussSum_mulShift_any (χ ^ 2) ψ hχ₂ (ε * x)]
rw [map_mul]
ring
theorem nontrivial_fourier_coefficient (χ : MulChar F ℂ) (ψ : AddChar F ℂ)
(hχ : χ ≠ 1) (h : F) :
(∑ t : F, χ t * ψ (-(h * t))) =
χ⁻¹ h * gaussSum χ (ψ.mulShift (-1)) := by
calc
(∑ t : F, χ t * ψ (-(h * t))) =
gaussSum χ ((ψ.mulShift (-1)).mulShift h) := by
simp only [gaussSum, AddChar.mulShift_apply]
congr 1
funext t
congr 1
ring_nf
_ = χ⁻¹ h * gaussSum χ (ψ.mulShift (-1)) :=
gaussSum_mulShift_any χ (ψ.mulShift (-1)) hχ h
theorem trivial_fourier_coefficient (ψ : AddChar F ℂ)
(hψ : ψ ≠ 1) (h : F) :
(∑ t : F, (1 : MulChar F ℂ) t * ψ (-(h * t))) =
if h = 0 then (Fintype.card Fˣ : ℂ) else -1 := by
calc
(∑ t : F, (1 : MulChar F ℂ) t * ψ (-(h * t))) =
gaussSum (1 : MulChar F ℂ) (ψ.mulShift (-h)) := by
simp only [gaussSum, AddChar.mulShift_apply]
congr 1
funext t
congr 1
ring_nf
_ = ∑ u : Fˣ, ψ ((-h) * (u : F)) := by
rw [gaussSum_eq_units_sum]
simp only [MulChar.one_apply_coe, one_mul, AddChar.mulShift_apply]
_ = if h = 0 then (Fintype.card Fˣ : ℂ) else -1 := by
simpa only [neg_eq_zero] using additive_unit_sum ψ hψ (-h)
end ShortDraftLocal
end OAI
end
section
-- Source module: OAI.NumberTheory.DirichletL.Mellin.ExponentialSmoothing
namespace OAI
open scoped BigOperators
open MulChar AddChar
open scoped BigOperators
namespace AnalyticBridge
variable {Ω : Type*}
theorem weighted_cauchy_sq
(S : Finset Ω) (w U V : Ω → ℂ) :
‖∑ ω ∈ S, w ω * U ω * star (V ω)‖ ^ 2 ≤
(∑ ω ∈ S, ‖w ω‖ * ‖U ω‖ ^ 2) *
(∑ ω ∈ S, ‖w ω‖ * ‖V ω‖ ^ 2) := by
have htri : ‖∑ ω ∈ S, w ω * U ω * star (V ω)‖ ≤
∑ ω ∈ S, ‖w ω‖ * ‖U ω‖ * ‖V ω‖ := by
calc
‖∑ ω ∈ S, w ω * U ω * star (V ω)‖ ≤
∑ ω ∈ S, ‖w ω * U ω * star (V ω)‖ := norm_sum_le _ _
_ = ∑ ω ∈ S, ‖w ω‖ * ‖U ω‖ * ‖V ω‖ := by
apply Finset.sum_congr rfl
intro ω hω
simp [ ]
have hnonneg : 0 ≤ ∑ ω ∈ S, ‖w ω‖ * ‖U ω‖ * ‖V ω‖ :=
Finset.sum_nonneg (by intro ω hω; positivity)
have hsq :
(∑ ω ∈ S, ‖w ω‖ * ‖U ω‖ * ‖V ω‖) ^ 2 ≤
(∑ ω ∈ S, ‖w ω‖ * ‖U ω‖ ^ 2) *
(∑ ω ∈ S, ‖w ω‖ * ‖V ω‖ ^ 2) := by
apply Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul S
(fun ω hω => by positivity) (fun ω hω => by positivity)
intro ω hω
(convert le_refl ((‖w ω‖ * ‖U ω‖ * ‖V ω‖) ^ 2) using 1 ; ring)
exact (sq_le_sq₀ (norm_nonneg _) hnonneg).2 htri |>.trans hsq
structure CRTChoice where
J : ℕ
C : ℕ
e : ℕ
v : ℕ
s : ℕ
J2 : ℕ
b1 : ℕ
b2 : ℕ
A1 : ℕ
A2 : ℕ
d : ℕ
kpp : ℕ
private def CRTChoice.coordinates (q : CRTChoice) :
(ℕ × ℕ × ℕ × ℕ) × (ℕ × ℕ × ℕ × ℕ) × (ℕ × ℕ × ℕ × ℕ) :=
((q.J, q.C, q.e, q.v), (q.s, q.J2, q.b1, q.b2),
(q.A1, q.A2, q.d, q.kpp))
end AnalyticBridge
open Filter Asymptotics MeasureTheory
open scoped Topology
namespace ExpBound
end ExpBound
namespace ShortDraftMellin
theorem inverse_mellin_analytic
(A : ℝ → ℂ) (σ : ℝ)
(hlocal : LocallyIntegrableOn A (Set.Ioi 0))
(htop : A =O[atTop] (fun t : ℝ => t ^ σ))
(hzero : A =ᶠ[𝓝[>] (0 : ℝ)] (fun _ => 0)) :
AnalyticOnNhd ℂ (fun s : ℂ => mellin A (-s)) {s : ℂ | σ < s.re} := by
apply (Complex.analyticOnNhd_iff_differentiableOn (Complex.isOpen_re_gt σ)).2
intro s hs
change σ < s.re at hs
have htop' : A =O[atTop] (fun t : ℝ => t ^ (-(-σ))) := by
simpa only [neg_neg] using htop
have hbot : A =O[𝓝[>] (0 : ℝ)]
(fun t : ℝ => t ^ (-((-s).re - 1))) := by
exact hzero.isBigO.trans (isBigO_zero _ _)
have hdiff : DifferentiableAt ℂ (mellin A) (-s) :=
mellin_differentiableAt_of_isBigO_rpow hlocal htop'
(by simpa using neg_lt_neg hs) hbot (by linarith)
exact (hdiff.comp s (differentiableAt_id.neg)).differentiableWithinAt
Provenance