Conjectural prime-local denominator bounds at Gompertz factorial endpoints
OpenEulerMascheroni.Arithmetic.gompertz_prime_local_bounds_conjecturealgebraic-integerseuler-mascheronilocal-global
Assume that the real Borel-summed Euler–Gompertz constant is algebraic. Conjecturally there is such that for every there is a positive integer for which is integral at every finite prime: for each prime , some integer coprime to makes an algebraic integer. The proved local-to-global and recurrence lemmas recover the original simultaneous denominator bound. This is an equivalent local arithmetic formulation, not a proof or a weaker logical conjecture.
Preamble
import Definitions.Def_eulerMascheroni_factorialQuotient open EulerMascheroni.Arithmetic
Formal statement
theorem EulerMascheroni.Arithmetic.gompertz_prime_local_bounds_conjecture (h : IsAlgebraic ℚ EulerMascheroni.gompertzConstant) :
∃ C : ℝ, 1 ≤ C ∧ ∀ n : ℕ, ∃ D : ℕ, 0 < D ∧ (D:ℝ) ≤ C^(n+1) ∧
∀ p : ℕ, p.Prime → ∃ d : ℤ, ¬(p:ℤ) ∣ d ∧
IsIntegral ℤ ((d:ℝ)*((D:ℝ)*quotientCoeff EulerMascheroni.gompertzConstant n)) := by sorry
Source
Integral closedness and principal ideals over the integers; prime-local reformulation of the Euler factorial quotient arithmetic division conjecture. Compare Fischler–Rivoal, https://rivoal.perso.math.cnrs.fr/articles/ssmixte.pdf, Conjecture 2, and Matala-aho–Zudilin, https://arxiv.org/html/1703.02633, Section 2.