The logarithmic height as a sum over the places

For a number field K and x : K, write ℓ_v(x) = log ‖x‖_v for the logarithm of the normalized absolute value of x at a place v of K, finite or infinite. At an infinite place w this is w.mult * log (w x), the weighted logarithm, and at a finite place it is the logarithm of the v-adic absolute value. For x ≠ 0 only finitely many ℓ_v(x) are nonzero, and:

• ∑ᶠ v, ℓ_v(x) = 0: the product formula in logarithmic form;
• logHeight₁ x = ∑ᶠ v, ℓ_v(x)⁺: the logarithmic height is the sum of the positive parts;
• 2 * logHeight₁ x = ∑ᶠ v, |ℓ_v(x)|: since the ℓ_v(x) sum to zero, their positive and negative parts have the same total;
• |ℓ_v(x)| ≤ logHeight₁ x at every single place.

These identities say that the height of x is half the ℓ¹ norm of its vector of weighted logarithms. Applied to the units of 𝓞 K, whose vector is supported on the infinite places, they compare the height of a unit with its image under the logarithmic embedding of Dirichlet's unit theorem, and applied to S-units they do the same for the S-logarithmic embedding. Every statement holds for x = 0 as well, where all the terms vanish.

The multiplicative height of a tuple x is likewise the product over all places of its largest normalized absolute value, mulHeight x = ∏ᶠ v, max_i ‖x_i‖_v.

Main results

• TauCeti.GlobalNumberFields.mulHeight_eq_finprod_iSup_normalizedAbsValue: mulHeight x = ∏ᶠ v, ⨆ i, ‖x i‖_v for a nonzero tuple x.
• TauCeti.GlobalNumberFields.finsum_log_normalizedAbsValue: the product formula, ∑ᶠ v, log ‖x‖_v = 0.
• TauCeti.GlobalNumberFields.logHeight₁_eq_finsum_posLog_normalizedAbsValue: logHeight₁ x = ∑ᶠ v, log⁺ ‖x‖_v.
• TauCeti.GlobalNumberFields.two_mul_logHeight₁_eq_finsum_abs_log_normalizedAbsValue: 2 * logHeight₁ x = ∑ᶠ v, |log ‖x‖_v|.
• TauCeti.GlobalNumberFields.abs_log_normalizedAbsValue_le_logHeight₁: |log ‖x‖_v| ≤ logHeight₁ x.
• IsDedekindDomain.HeightOneSpectrum.abs_log_valuation_mul_log_absNorm_le_logHeight₁: Liouville's inequality at a finite place, |ord_v(x)| log N(v) ≤ logHeight₁ x.
• TauCeti.GlobalNumberFields.finsum_comp_log_normalizedAbsValue_eq_sum: for f with f 0 = 0 and x a unit outside a finite set S of finite places, ∑ᶠ v, f (log ‖x‖_v) is a finite sum over S and the infinite places.
• TauCeti.GlobalNumberFields.sum_log_adicAbv_add_sum_mult_mul_log_eq_zero and TauCeti.GlobalNumberFields.two_mul_logHeight₁_eq_sum_abs_log_adicAbv_add_sum_mult_mul_abs_log: the same identities as finite sums over the infinite places and a finite set S of finite places outside which x is a unit.

References

• Y. Bugeaud and K. Győry, Bounds for the solutions of unit equations, Acta Arith. 74 (1996), 67–80, §3, formula (12).
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, §1.5.

theorem TauCeti.GlobalNumberFields.hasFiniteSupport_log_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] (x : K) : Function.HasFiniteSupport fun (v : Place K) => Real.log ((normalizedAbsValue v) x)

The logarithms of the normalized absolute values of an element of a number field vanish at all but finitely many places.

@[simp]

theorem TauCeti.GlobalNumberFields.finsum_log_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] (x : K) : ∑ᶠ (v : Place K), Real.log ((normalizedAbsValue v) x) = 0

The product formula in logarithmic form: the logarithms of the normalized absolute values of an element of a number field sum to zero over all places.

theorem TauCeti.GlobalNumberFields.logHeight₁_eq_finsum_posLog_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] (x : K) : Height.logHeight₁ x = ∑ᶠ (v : Place K), ((normalizedAbsValue v) x).posLog

The logarithmic height of an element of a number field is the sum, over all places, of the positive parts log⁺ ‖x‖_v of the logarithms of its normalized absolute values.

theorem TauCeti.GlobalNumberFields.two_mul_logHeight₁_eq_finsum_abs_log_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] (x : K) : 2 * Height.logHeight₁ x = ∑ᶠ (v : Place K), |Real.log ((normalizedAbsValue v) x)|

Twice the logarithmic height of an element of a number field is the sum, over all places, of the absolute values |log ‖x‖_v|. Since these logarithms sum to zero, their positive and negative parts contribute equally.

theorem TauCeti.GlobalNumberFields.log_normalizedAbsValue_le_logHeight₁ {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) : Real.log ((normalizedAbsValue v) x) ≤ Height.logHeight₁ x

The logarithm of the normalized absolute value of x at any single place is at most the logarithmic height of x.

theorem TauCeti.GlobalNumberFields.abs_log_normalizedAbsValue_le_logHeight₁ {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) : |Real.log ((normalizedAbsValue v) x)| ≤ Height.logHeight₁ x

The logarithm of the normalized absolute value of x at any single place is at most the logarithmic height of x in absolute value. This sharpens the classical bound by 2 * h(x).

theorem TauCeti.GlobalNumberFields.exists_mem_log_normalizedAbsValue_le_neg_logHeight₁_div {K : Type u_1} [Field K] [NumberField K] {T : Finset (Place K)} (hT : T.Nonempty) {x : K} (hx : ∀ v ∉ T, (normalizedAbsValue v) x = 1) : ∃ v ∈ T, Real.log ((normalizedAbsValue v) x) ≤ -Height.logHeight₁ x / ↑T.card

If x has normalized absolute value 1 outside a nonempty finite set T of places, then at some place v ∈ T the logarithm log ‖x‖_v is at most -logHeight₁ x / #T. Indeed, by the product formula the negative parts of these logarithms sum to -logHeight₁ x.

theorem TauCeti.GlobalNumberFields.mulHeight_eq_finprod_iSup_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : x ≠ 0) : Height.mulHeight x = ∏ᶠ (v : Place K), ⨆ (i : ι), (normalizedAbsValue v) (x i)

The multiplicative height of a nonzero tuple of elements of a number field is the product, over all places, of its largest normalized absolute value.

theorem TauCeti.GlobalNumberFields.finsum_comp_log_normalizedAbsValue_eq_sum {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {x : K} {f : ℝ → ℝ} (hf : f 0 = 0) (hS : ∀ v ∉ S, (NumberField.HeightOneSpectrum.adicAbv K v) x = 1) : ∑ᶠ (v : Place K), f (Real.log ((normalizedAbsValue v) x)) = ∑ v ∈ S, f (Real.log ((NumberField.HeightOneSpectrum.adicAbv K v) x)) + ∑ w : NumberField.InfinitePlace K, f (↑w.mult * Real.log (w x))

If x is a unit outside a finite set S of finite places and f 0 = 0, then the sum of f (log ‖x‖_v) over all places is a sum over the places of S plus a sum over the infinite places.

theorem TauCeti.GlobalNumberFields.sum_log_adicAbv_add_sum_mult_mul_log_eq_zero {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {x : K} (hS : ∀ v ∉ S, (NumberField.HeightOneSpectrum.adicAbv K v) x = 1) : ∑ v ∈ S, Real.log ((NumberField.HeightOneSpectrum.adicAbv K v) x) + ∑ w : NumberField.InfinitePlace K, ↑w.mult * Real.log (w x) = 0

The product formula in logarithmic form, for an element x of a number field which is a unit outside a finite set S of finite places: the logarithms of its absolute values at the places of S, and its weighted logarithms at the infinite places, sum to zero.

theorem TauCeti.GlobalNumberFields.two_mul_logHeight₁_eq_sum_abs_log_adicAbv_add_sum_mult_mul_abs_log {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {x : K} (hS : ∀ v ∉ S, (NumberField.HeightOneSpectrum.adicAbv K v) x = 1) : 2 * Height.logHeight₁ x = ∑ v ∈ S, |Real.log ((NumberField.HeightOneSpectrum.adicAbv K v) x)| + ∑ w : NumberField.InfinitePlace K, ↑w.mult * |Real.log (w x)|

Twice the logarithmic height of an element x of a number field which is a unit outside a finite set S of finite places is the ℓ¹ norm of its vector of logarithms at the places of S and weighted logarithms at the infinite places.

theorem IsDedekindDomain.HeightOneSpectrum.abs_log_valuation_mul_log_absNorm_le_logHeight₁ {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) : ↑|((valuation K v) x).log| * Real.log ↑(Ideal.absNorm v.asIdeal) ≤ Height.logHeight₁ x

Liouville's inequality at a finite place. The absolute value of the order -WithZero.log (v.valuation K x) of an element x of a number field at a finite place v, weighted by the logarithm of the norm of v, is at most the logarithmic height of x. Both sides vanish at x = 0.