SunConj_ChayoteG6: shared definitions
DefinitionSunConj_ChayoteG6Shared Lean definitions SunConj_ChayoteG6 used by the statements of this project.
chayoteB6: Gamma part of Sun'sgof Conjecture 5.6, as a function of a complex variable;4096 ^ zis writtenexp (z * log 4096).chayoteP6: The polynomial factor of Sun'sgof Conjecture 5.6.chayoteG6: Complex extension ofg6.chayoteS6: The shifted seriesS(z) = ∑_{k ≥ 0} g(k + z).
Definition code
import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic
noncomputable section
namespace SunConj
/-- Gamma part of Sun's `g` of Conjecture 5.6, as a function of a complex variable;
`4096 ^ z` is written `exp (z * log 4096)`. -/
def chayoteB6 (z : ℂ) : ℂ :=
Complex.Gamma (4 * z + 1) ^ 2 /
(Complex.exp (z * (Real.log 4096 : ℂ)) * Complex.Gamma (z + 1) ^ 2 * Complex.Gamma (2 * z + 1) ^ 3)
/-- The polynomial factor of Sun's `g` of Conjecture 5.6. -/
def chayoteP6 (z : ℂ) : ℂ := 48 * z ^ 2 + 32 * z + 3
/-- Complex extension of `g6`. -/
def chayoteG6 (z : ℂ) : ℂ := chayoteP6 z * chayoteB6 z / (2 * z + 1)
/-- The shifted series `S(z) = ∑_{k ≥ 0} g(k + z)`. -/
def chayoteS6 (z : ℂ) : ℂ := ∑' k : ℕ, chayoteG6 ((k : ℂ) + z)
end SunConj
Source