Explicit lower bounds for number-field regulators

In degree d and unit rank r, the regulator is at least (log 2 / (unitPowerCountBound d + 1)) ^ r / r!. This is a positive, explicit expression depending only on d and r, including positive unit ranks. The estimate combines the explicit nontorsion-unit height gap with Minkowski's second theorem for the unit logarithmic lattice. It is intentionally coarse; it does not use a minimum obtained from finiteness.

In unit rank zero this bound is 1, which is the exact value of the regulator there (NumberField.Units.regulator_eq_one_of_rank_eq_zero in TauCeti.NumberTheory.NumberField.Units.Regulator.Basic).

Main results

• TauCeti.NumberField.Units.regulatorLowerBound_le_regulator: an explicit positive degree-and-rank bound for every number field.

noncomputable def TauCeti.NumberField.Units.regulatorLowerBound (d r : ℕ) : ℝ

The explicit lower bound for the regulator in degree d and unit rank r.

theorem TauCeti.NumberField.Units.regulatorLowerBound_def (d r : ℕ) : regulatorLowerBound d r = unitHeightLowerBound d ^ r / ↑r.factorial

The degree-and-rank formula for the explicit regulator lower bound.

theorem TauCeti.NumberField.Units.regulatorLowerBound_pos (d r : ℕ) : 0 < regulatorLowerBound d r

The explicit regulator bound is positive, including every positive unit rank.

@[simp]

theorem TauCeti.NumberField.Units.regulatorLowerBound_rank_zero (d : ℕ) : regulatorLowerBound d 0 = 1

The explicit regulator lower bound has the standard value one in rank zero.

theorem TauCeti.NumberField.Units.regulatorLowerBound_le_regulator (K : Type u_1) [Field K] [NumberField K] : regulatorLowerBound (Module.finrank ℚ K) (NumberField.Units.rank K) ≤ NumberField.Units.regulator K

An explicit regulator lower bound in every unit rank. If d = [K : ℚ] and r = rank K, then R_K ≥ (log 2 / (unitPowerCountBound d + 1)) ^ r / r!. The constant depends only on the degree and unit rank and is strictly positive.