The fundamental inequality

Let K be a number field and x ≠ 0 an element of K. Multiply the local factors of x over a finite set S∞ of infinite places, weighted by InfinitePlace.mult, and a finite set S₀ of finite places. The fundamental inequality traps the result between the multiplicative height of x and its reciprocal:

(mulHeight₁ x)⁻¹ ≤ (∏ v ∈ S∞, |x|_v ^ mult v) * ∏ v ∈ S₀, |x|_v ≤ mulHeight₁ x.

The upper bound holds for x = 0 as well. The lower bound follows from the upper bound for x⁻¹, since inversion inverts the product and preserves the height (Height.mulHeight₁_inv).

In the form used by Liouville's inequality and Roth's theorem, every local factor is truncated to min 1 |x|_v and the product is taken over all places. Then it is exactly (mulHeight₁ x)⁻¹, because min 1 t * max t 1 = t turns the product formula into the definition of the height. Every truncated factor is at most 1, so cutting the product down to S∞ and S₀ can only increase it. At a single place the two bounds read (mulHeight₁ x)⁻¹ ≤ min 1 |x|_v and max |x|_v 1 ≤ mulHeight₁ x.

Main results

• NumberField.prod_apply_le_mulHeight₁ and NumberField.inv_mulHeight₁_le_prod_apply: the two halves of the fundamental inequality.
• NumberField.one_le_prod_apply_of_forall_le_one: the product over all infinite places and a finite set of finite places is at least one for a nonzero element integral outside that set.
• NumberField.prod_max_apply_one_le_mulHeight₁: the upper bound with every local factor truncated to max |x|_v 1.
• NumberField.prod_min_one_apply_eq_inv_mulHeight₁: over all places the truncated local factors of x ≠ 0 multiply to (mulHeight₁ x)⁻¹.
• NumberField.inv_mulHeight₁_le_prod_min_one_apply: over finitely many places the truncated product is at least (mulHeight₁ x)⁻¹.
• NumberField.InfinitePlace.max_apply_one_le_mulHeight₁, NumberField.FinitePlace.max_apply_one_le_mulHeight₁, NumberField.InfinitePlace.inv_mulHeight₁_le_min_one_apply and NumberField.FinitePlace.inv_mulHeight₁_le_min_one_apply: the bounds at a single place.
• NumberField.InfinitePlace.max_apply_one_pow_mult_le_mulHeight₁ and NumberField.InfinitePlace.inv_mulHeight₁_le_min_one_apply_pow_mult: the bounds at a single infinite place, keeping the weight mult v.

The logarithmic form of the single-place bounds, for the normalized absolute value at a place, is TauCeti.GlobalNumberFields.abs_log_normalizedAbsValue_le_logHeight₁.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §1.5, the fundamental inequality (1.8).

The same statements, along the same route, are formalized in Ralf Stephan's rwst/Subspace-Theorems at 09835cb23557ae5ae0cf55a9c4ab9055f5d60338, file DiophantineApproximation/FundamentalInequality.lean (Apache 2.0).

The fundamental inequality

theorem NumberField.prod_max_apply_one_le_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] (Sinf : Finset (InfinitePlace K)) (Sfin : Finset (FinitePlace K)) (x : K) : (∏ v ∈ Sinf, max (v x) 1 ^ v.mult) * ∏ v ∈ Sfin, max (v x) 1 ≤ Height.mulHeight₁ x

The truncated local factors max |x|_v 1 of x over finitely many places, weighted by mult at the infinite places, multiply to at most the height of x.

theorem NumberField.prod_apply_le_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] (Sinf : Finset (InfinitePlace K)) (Sfin : Finset (FinitePlace K)) (x : K) : (∏ v ∈ Sinf, v x ^ v.mult) * ∏ v ∈ Sfin, v x ≤ Height.mulHeight₁ x

The fundamental inequality, upper bound (Bombieri–Gubler (1.8)): the product of the local factors of x over finitely many places, weighted by mult at the infinite places, is at most the height of x.

theorem NumberField.inv_mulHeight₁_le_prod_apply {K : Type u_1} [Field K] [NumberField K] (Sinf : Finset (InfinitePlace K)) (Sfin : Finset (FinitePlace K)) {x : K} (hx : x ≠ 0) : (Height.mulHeight₁ x)⁻¹ ≤ (∏ v ∈ Sinf, v x ^ v.mult) * ∏ v ∈ Sfin, v x

The fundamental inequality, lower bound (Bombieri–Gubler (1.8)): the product of the local factors of a nonzero x over finitely many places, weighted by mult at the infinite places, is at least the reciprocal of the height of x.

theorem NumberField.one_le_prod_apply_of_forall_le_one {K : Type u_1} [Field K] [NumberField K] (Sfin : Finset (FinitePlace K)) {x : K} (hx : x ≠ 0) (h : ∀ v ∉ Sfin, v x ≤ 1) : 1 ≤ (∏ v : InfinitePlace K, v x ^ v.mult) * ∏ v ∈ Sfin, v x

A nonzero element integral at every finite place outside Sfin has product of local absolute values at least one over all infinite places and Sfin.

The truncated product

theorem NumberField.prod_min_one_apply_eq_inv_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : (∏ v : InfinitePlace K, min 1 (v x) ^ v.mult) * ∏ᶠ (v : FinitePlace K), min 1 (v x) = (Height.mulHeight₁ x)⁻¹

The truncated local factors min 1 |x|_v of a nonzero x, taken over all places and weighted by mult at the infinite places, multiply to the reciprocal of the height of x. This is the product formula read through min 1 t * max t 1 = t.

theorem NumberField.inv_mulHeight₁_le_prod_min_one_apply {K : Type u_1} [Field K] [NumberField K] (Sinf : Finset (InfinitePlace K)) (Sfin : Finset (FinitePlace K)) {x : K} (hx : x ≠ 0) : (Height.mulHeight₁ x)⁻¹ ≤ (∏ v ∈ Sinf, min 1 (v x) ^ v.mult) * ∏ v ∈ Sfin, min 1 (v x)

The fundamental inequality in truncated form: the truncated local factors min 1 |x|_v of a nonzero x over finitely many places, weighted by mult at the infinite places, multiply to at least the reciprocal of the height of x.

One place at a time

theorem NumberField.InfinitePlace.max_apply_one_pow_mult_le_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] (v : InfinitePlace K) (x : K) : max (v x) 1 ^ v.mult ≤ Height.mulHeight₁ x

The truncated local factor of x at an infinite place, weighted by mult, is at most the height of x: max |x|_v 1 ^ mult v ≤ H(x).

theorem NumberField.InfinitePlace.max_apply_one_le_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] (v : InfinitePlace K) (x : K) : max (v x) 1 ≤ Height.mulHeight₁ x

The value of x at an infinite place is at most the height of x: max |x|_v 1 ≤ H(x).

theorem NumberField.FinitePlace.max_apply_one_le_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) (x : K) : max (v x) 1 ≤ Height.mulHeight₁ x

The value of x at a finite place is at most the height of x: max |x|_v 1 ≤ H(x).

theorem NumberField.InfinitePlace.inv_mulHeight₁_le_min_one_apply_pow_mult {K : Type u_1} [Field K] [NumberField K] (v : InfinitePlace K) {x : K} (hx : x ≠ 0) : (Height.mulHeight₁ x)⁻¹ ≤ min 1 (v x) ^ v.mult

The truncated local factor of a nonzero x at an infinite place, weighted by mult, is at least the reciprocal of the height of x: H(x)⁻¹ ≤ min 1 |x|_v ^ mult v.

theorem NumberField.InfinitePlace.inv_mulHeight₁_le_min_one_apply {K : Type u_1} [Field K] [NumberField K] (v : InfinitePlace K) {x : K} (hx : x ≠ 0) : (Height.mulHeight₁ x)⁻¹ ≤ min 1 (v x)

The value of a nonzero x at an infinite place is at least the reciprocal of the height of x: H(x)⁻¹ ≤ min 1 |x|_v.

theorem NumberField.FinitePlace.inv_mulHeight₁_le_min_one_apply {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) {x : K} (hx : x ≠ 0) : (Height.mulHeight₁ x)⁻¹ ≤ min 1 (v x)

The value of a nonzero x at a finite place is at least the reciprocal of the height of x: H(x)⁻¹ ≤ min 1 |x|_v.

Examples