TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.logarithmicMellinWeight (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (y : mixedEmbedding.realSpace K) : ℂ

A logarithmic mellin weight used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.logarithmicMellinWeight K s y = Complex.exp (↑(y NumberField.Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * s)

@[simp]

theorem NumberField.Odlyzko.logarithmicMellinWeight_apply (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (y : mixedEmbedding.realSpace K) : logarithmicMellinWeight K s y = Complex.exp (↑(y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * s)

theorem NumberField.Odlyzko.exp_denominatorLogCoordinates_mul_finrank (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Real.exp (denominatorLogCoordinates K I Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) = ↑|(Algebra.norm ℚ) ((algebraMap (RingOfIntegers K) K) ↑(↑I).den)|

theorem NumberField.Odlyzko.logarithmicMellinWeight_vadd_unitCoordinateLattice (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (g : ↥unitCoordinateLattice) (y : mixedEmbedding.realSpace K) : logarithmicMellinWeight K s (↑g + y) = logarithmicMellinWeight K s y

theorem NumberField.Odlyzko.logarithmicMellinWeight_add (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (y a : mixedEmbedding.realSpace K) : logarithmicMellinWeight K s (y + a) = logarithmicMellinWeight K s a * logarithmicMellinWeight K s y