English
For a Dirichlet character χ modulo N with NeZero N, the L-function product |LFunctionTrivChar N(1+x)^3 · LFunction χ(1+x+iy)^4 · LFunction(χ^2)(1+x+2iy)| is bounded below by 1 for x>0 and any y, mirroring the L-series positivity with LFunction versions.
Русский
Для символа Дирихле χ по модулю N с условием NeZero N произведение L-функций удовлетворяет неравенству: |LFunctionTrivChar N(1+x)^3 · LFunction χ(1+x+iy)^4 · LFunction(χ^2)(1+x+2iy)| ≥ 1 при x>0 и любом y.
LaTeX
$$$\|LFunctionTrivChar(N,1+x)^{3} \cdot LFunction(χ,1+x+iy)^{4} \cdot LFunction(χ^{2},1+x+2iy)\| \ge 1$$$
Lean4
/-- A variant of `DirichletCharacter.norm_LSeries_product_ge_one` in terms of the L-functions. -/
theorem norm_LFunction_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :
‖LFunctionTrivChar N (1 + x) ^ 3 * LFunction χ (1 + x + I * y) ^ 4 * LFunction (χ ^ 2) (1 + x + 2 * I * y)‖ ≥ 1 :=
by
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
rw [LFunctionTrivChar, DirichletCharacter.LFunction_eq_LSeries 1 h₀, χ.LFunction_eq_LSeries h₁,
(χ ^ 2).LFunction_eq_LSeries h₂]
exact norm_LSeries_product_ge_one χ hx y
