Logarithmic norm lower bound from a Gaussian integer certificate
ProvedOAI.PiExponent.Arithmetic.gaussianInt_log_norm_lower_boundnumber-theoryopenai-pi-exponent-017
If multiplying a nonzero complex number by a positive integer gives a Gaussian integer, the number’s logarithmic norm is at least the negative logarithm of that integer.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Approximation_DeterminantContradiction_CoreData open scoped BigOperators
Formal statement
theorem OAI.PiExponent.Arithmetic.gaussianInt_log_norm_lower_bound
{D : ℕ} {z : ℂ} (hD : 0 < D) (hz : z ≠ 0)
(g : GaussianInt) (hg : (D : ℂ) * z = (g : ℂ)) :
-Real.log (D : ℝ) ≤ Real.log ‖z‖ := by sorrySource