English
Let χ be a Dirichlet character modulo N. Then the product of the L-series values at shifted points, involving the trivial character, χ, and χ^2, has strictly positive magnitude: |L(trivial, 1+x)^3 · L(χ, 1+x+iy)^4 · L(χ^2, 1+x+2iy)| ≥ 1 for every real x > 0 and any real y.
Русский
Пусть χ — символ Дирихле modulo N. Тогда модуль произведения значений L-функций в сдвинутых точках, включающее тривиальный символ, χ и χ^2, удовлетворяет: |L(тривиальный, 1+x)^3 · L(χ, 1+x+iy)^4 · L(χ^2, 1+x+2iy)| ≥ 1 для каждого действительного x>0 и любого действительного y.
LaTeX
$$$\big|L(1,1+x)^{3} \cdot L(\chi,1+x+iy)^{4} \cdot L(\chi^{2},1+x+2iy)\big| \ge 1,$$$
Lean4
/-- For positive `x` and nonzero `y` and a Dirichlet character `χ` we have that
`|L(χ^0, 1 + x)^3 L(χ, 1 + x + I * y)^4 L(χ^2, 1 + x + 2 * I * y)| ≥ 1. -/
theorem norm_LSeries_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :
‖L ↗(1 : DirichletCharacter ℂ N) (1 + x) ^ 3 * L ↗χ (1 + x + I * y) ^ 4 * L ↗(χ ^ 2 :) (1 + x + 2 * I * y)‖ ≥ 1 :=
by
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
have H₀ := summable_neg_log_one_sub_mul_prime_cpow (N := N) 1 h₀
have H₁ := summable_neg_log_one_sub_mul_prime_cpow χ h₁
have H₂ := summable_neg_log_one_sub_mul_prime_cpow (χ ^ 2) h₂
have hsum₀ := (hasSum_re H₀.hasSum).summable.mul_left 3
have hsum₁ := (hasSum_re H₁.hasSum).summable.mul_left 4
have hsum₂ := (hasSum_re H₂.hasSum).summable
rw [← LSeries_eulerProduct_exp_log _ h₀, ← LSeries_eulerProduct_exp_log χ h₁, ← LSeries_eulerProduct_exp_log _ h₂]
simp only [← exp_nat_mul, Nat.cast_ofNat, ← exp_add, norm_exp, add_re, mul_re, re_ofNat, im_ofNat, zero_mul, sub_zero,
Real.one_le_exp_iff]
rw [re_tsum H₀, re_tsum H₁, re_tsum H₂, ← tsum_mul_left, ← tsum_mul_left, ← hsum₀.tsum_add hsum₁, ←
(hsum₀.add hsum₁).tsum_add hsum₂]
simpa only [neg_add_rev, neg_re, mul_neg, χ.pow_apply' two_ne_zero, ge_iff_le, add_re, one_re, ofReal_re, ofReal_add,
ofReal_one] using tsum_nonneg fun (p : Nat.Primes) ↦ χ.re_log_comb_nonneg p.prop.two_le h₀ y
