The Arakelov height over a number field

Mathlib's Height.mulHeight measures a tuple by the sup norm at every place. In Arakelov theory one instead uses the ℓ² norm at the archimedean places — the Fubini–Study metric on O(1) — and keeps the sup norm at the finite places. The resulting height is the one in which the constants of the Siegel-lemma literature (Bombieri–Vaaler, Schmidt) are stated.

This file defines that normalization over a number field K and proves its basic API — scaling invariance and the descent to projective space, 1 ≤ H_Ar, invariance under reindexing, and the affine case — together with the two-sided comparison with Height.mulHeight, which is what lets a bound stated in either normalization be read in the other. Not all of Mathlib.NumberTheory.Height.Basic transfers here — see the implementation notes.

Main definitions

• NumberField.arakelovMulHeight x for x : ι → K: the multiplicative Arakelov height ∏_{v | ∞} (∑ i, v (x i)²)^{mult v / 2} · ∏ᶠ_{v ∤ ∞} ⨆ i, v (x i).
• NumberField.arakelovLogHeight x: its logarithm.
• NumberField.arakelovMulHeight₁ x and NumberField.arakelovLogHeight₁ x for x : K: the one-variable (affine) case, the height of the tuple ![x, 1].
• Projectivization.arakelovMulHeight and Projectivization.arakelovLogHeight: the descent of the above to Projectivization K (ι → K), which the scaling invariance below justifies.

Main results

• NumberField.arakelovMulHeight_smul_eq: invariance under scaling by a nonzero element of K, by the product formula. This is what makes the height projective.
• NumberField.one_le_arakelovMulHeight: the Arakelov height is at least 1.
• NumberField.arakelovMulHeight_comp_equiv: invariance under reindexing.
• NumberField.arakelovMulHeight_one and NumberField.arakelovMulHeight₁_one: the values #ι ^ (totalWeight K / 2) and 2 ^ (totalWeight K / 2) on the all-ones tuple and at 1, where the sup-norm height is 1 — the two normalizations genuinely differ.
• NumberField.arakelovLogHeight₁_eq: the local formula for the affine logarithmic height, with log⁺ (v x) at the finite places.
• NumberField.mulHeight_le_arakelovMulHeight and NumberField.arakelovMulHeight_le_mulHeight: the two comparisons with Mathlib's sup-norm height, the second with the constant #ι ^ (totalWeight K / 2). These are what transport a constant stated for one normalization into the other, and the second is sharp: it is an equality at the all-ones tuple.
• NumberField.arakelovMulHeight₁_le_mulHeight₁: the affine case of the same, with constant 2 ^ (totalWeight K / 2) — there is no equality arakelovMulHeight₁ = mulHeight₁.
• Projectivization.mulHeight_le_arakelovMulHeight and Projectivization.arakelovMulHeight_le_mulHeight: the same two comparisons on projective space, where the heights of Layer 3 live. The first is what makes the Northcott property of Layer 1.1 carry over to the Arakelov normalization, since it bounds the sup-norm height by the Arakelov one with no constant at all.

Implementation notes

As for Height.mulHeight, the zero tuple gets the junk value 1: the displayed product is 0 there, which would break 1 ≤ arakelovMulHeight and the comparison with Height.mulHeight. NumberField.arakelovMulHeight_eq recovers the displayed formula for a nonzero tuple, and every statement below holds unconditionally with this convention.

The index type carries Fintype rather than Finite because the archimedean local factor is a Finset.sum over ι; the value does not depend on the instance.

Only the archimedean factor differs from NumberField.mulHeight_eq. Accordingly the proof of scaling invariance does not redo the product-formula bookkeeping at the finite places: the transformation law of the finite part is extracted from Mathlib's Height.mulHeight_smul_eq_mulHeight, which is the only place where the two normalizations interact here.

Not every lemma of Mathlib.NumberTheory.Height.Basic has an Arakelov analogue, and the two that fail are not edge cases. Height.mulHeight_pow is false here — the ℓ² norm is not multiplicative under coordinatewise powers — and with it mulHeight₁_pow and mulHeight₁_zpow. Height.mulHeight_comp_le is false for a non-injective reindexing, since repeating a coordinate raises the ℓ² norm at the archimedean places while no sup norm can see the repetition; it is the injective case that its consumers use. Both are refuted among the examples at the end of this file.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Definition 2.8.1 and 2.8.2–2.8.3 for the local factors and the resulting projective height. Their h_Ar is the absolute logarithmic height, with degree-normalized local weights. Writing H_Ar = exp(h_Ar) for its absolute multiplicative form, arakelovMulHeight here is H_Ar ^ [K : ℚ], relative to K and matching Mathlib's Height.mulHeight convention.

This is Layers 0.1 and 0.2 of the ArithmeticHeights roadmap: the normalization and its comparison with Height.mulHeight.

noncomputable def NumberField.arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : ℝ

The Arakelov height of a tuple of elements of a number field: the ℓ² norm at the archimedean places, weighted by InfinitePlace.mult, and the sup norm at the finite places. For the zero tuple we take the junk value 1, as Height.mulHeight does.

This is the normalization in which the constants of the Siegel-lemma literature are stated; Height.mulHeight uses the sup norm at every place. Both live in the library and every bound says which one it is in.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.arakelovMulHeight_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] {x : ι → K} (hx : x ≠ 0) : arakelovMulHeight x = (∏ v : InfinitePlace K, (∑ i : ι, v (x i) ^ 2) ^ (↑v.mult / 2)) * ∏ᶠ (v : FinitePlace K), ⨆ (i : ι), v (x i)

@[simp]

theorem NumberField.arakelovMulHeight_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] : arakelovMulHeight 0 = 1

noncomputable def NumberField.arakelovLogHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : ℝ

The logarithmic Arakelov height. As everywhere in this development, the logarithmic height is defined as the logarithm of the multiplicative one and never independently.

Equations

• NumberField.arakelovLogHeight x = Real.log (NumberField.arakelovMulHeight x)

theorem NumberField.arakelovLogHeight_eq_log_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : arakelovLogHeight x = Real.log (arakelovMulHeight x)

@[simp]

theorem NumberField.arakelovLogHeight_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] : arakelovLogHeight 0 = 0

Scaling invariance

The archimedean local factor scales by v c ^ mult v and the finite one by v c, so the product formula makes the height invariant. The finite half of that computation is already in Mathlib, inside Height.mulHeight_smul_eq_mulHeight; we read it off rather than redo it.

theorem NumberField.arakelovMulHeight_smul_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) {c : K} (hc : c ≠ 0) : arakelovMulHeight (c • x) = arakelovMulHeight x

The Arakelov height is invariant under scaling, by the product formula, so it descends to projective space exactly as Height.mulHeight does.

theorem NumberField.arakelovLogHeight_smul_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) {c : K} (hc : c ≠ 0) : arakelovLogHeight (c • x) = arakelovLogHeight x

theorem NumberField.arakelovMulHeight_neg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : arakelovMulHeight (-x) = arakelovMulHeight x

theorem NumberField.arakelovLogHeight_neg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : arakelovLogHeight (-x) = arakelovLogHeight x

Positivity and reindexing

theorem NumberField.one_le_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : 1 ≤ arakelovMulHeight x

The Arakelov height of a tuple is always at least 1.

theorem NumberField.arakelovMulHeight_pos {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : 0 < arakelovMulHeight x

theorem NumberField.arakelovMulHeight_ne_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : arakelovMulHeight x ≠ 0

theorem NumberField.arakelovLogHeight_nonneg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : 0 ≤ arakelovLogHeight x

theorem NumberField.arakelovMulHeight_comp_equiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Fintype ι'] (e : ι ≃ ι') (x : ι' → K) : arakelovMulHeight (x ∘ ⇑e) = arakelovMulHeight x

The Arakelov height does not change under re-indexing.

theorem NumberField.arakelovLogHeight_comp_equiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Fintype ι'] (e : ι ≃ ι') (x : ι' → K) : arakelovLogHeight (x ∘ ⇑e) = arakelovLogHeight x

theorem NumberField.arakelovMulHeight_swap {K : Type u_1} [Field K] [NumberField K] (x y : K) : arakelovMulHeight ![x, y] = arakelovMulHeight ![y, x]

Swapping the two coordinates leaves the Arakelov height of a pair unchanged.

theorem NumberField.arakelovLogHeight_swap {K : Type u_1} [Field K] [NumberField K] (x y : K) : arakelovLogHeight ![x, y] = arakelovLogHeight ![y, x]

Special values

Height.mulHeight (1 : ι → K) = 1 by the product formula, but the Arakelov height of the same tuple is #ι ^ (totalWeight K / 2): these are the values that exhibit the difference between the two normalizations without touching the junk value.

theorem NumberField.arakelovMulHeight_one {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Nonempty ι] : arakelovMulHeight 1 = ↑(Fintype.card ι) ^ (↑(Height.totalWeight K) / 2)

The Arakelov height of the all-ones tuple. Its sup-norm counterpart Height.mulHeight_one has value 1.

@[simp]

theorem NumberField.arakelovMulHeight_eq_one_of_subsingleton {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Subsingleton ι] (x : ι → K) : arakelovMulHeight x = 1

On a subsingleton index type every tuple has Arakelov height 1, by the product formula. This is the degenerate case in which the Arakelov and sup-norm normalizations agree.

@[simp]

theorem NumberField.arakelovLogHeight_eq_zero_of_subsingleton {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Subsingleton ι] (x : ι → K) : arakelovLogHeight x = 0

The comparison with the sup-norm height

‖·‖_∞ ≤ ‖·‖_2 ≤ √(#ι) · ‖·‖_∞ at each archimedean place, raised to the weight mult v and multiplied over the places; the finite parts of the two heights are the same number and factor out. This is Layer 0.2 of the roadmap: the pair of lemmas that transports a constant stated for the Arakelov height into Mathlib's normalization and back, and so the reason a bound in either normalization is a bound in the other.

The constant of the upper comparison cannot be improved: at the all-ones tuple it is an equality, by arakelovMulHeight_one against Height.mulHeight_one.

theorem NumberField.mulHeight_le_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : Height.mulHeight x ≤ arakelovMulHeight x

The sup-norm height is at most the Arakelov height. The finite parts agree and the archimedean ones compare place by place, since ‖·‖_∞ ≤ ‖·‖_2.

theorem NumberField.arakelovMulHeight_le_mulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Nonempty ι] (x : ι → K) : arakelovMulHeight x ≤ ↑(Fintype.card ι) ^ (↑(Height.totalWeight K) / 2) * Height.mulHeight x

The Arakelov height is at most #ι ^ (totalWeight K / 2) times the sup-norm height — the lemma that carries the constants of the Siegel-lemma literature into Mathlib's normalization, from ‖·‖_2 ≤ √(#ι) · ‖·‖_∞ at each archimedean place.

ι must be nonempty: on the empty index type both heights take the junk value 1 while the right-hand side is 0. The constant is sharp — arakelovMulHeight_one is the case of equality.

theorem NumberField.arakelovMulHeight_eq_mulHeight_of_subsingleton {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Subsingleton ι] (x : ι → K) : arakelovMulHeight x = Height.mulHeight x

On a subsingleton index type the two normalizations agree: both are 1, by the product formula. This is the only index type on which they agree unconditionally.

theorem NumberField.logHeight_le_arakelovLogHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : ι → K) : Height.logHeight x ≤ arakelovLogHeight x

theorem NumberField.arakelovLogHeight_le_logHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Nonempty ι] (x : ι → K) : arakelovLogHeight x ≤ ↑(Height.totalWeight K) / 2 * Real.log ↑(Fintype.card ι) + Height.logHeight x

theorem NumberField.arakelovLogHeight_eq_logHeight_of_subsingleton {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Subsingleton ι] (x : ι → K) : arakelovLogHeight x = Height.logHeight x

The one-variable case

arakelovMulHeight₁ x is the Arakelov height of the point (x : 1) of the projective line. Unlike the sup-norm normalization, its archimedean local factor is ((v x) ^ 2 + 1) ^ (mult v / 2) rather than max (v x) 1 ^ mult v, so it does not agree with Height.mulHeight₁.

noncomputable def NumberField.arakelovMulHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : ℝ

The multiplicative Arakelov height of an element of a number field, i.e. of the point (x : 1) of the projective line.

Equations

• NumberField.arakelovMulHeight₁ x = NumberField.arakelovMulHeight ![x, 1]

noncomputable def NumberField.arakelovLogHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : ℝ

The logarithmic Arakelov height of an element of a number field.

Equations

• NumberField.arakelovLogHeight₁ x = Real.log (NumberField.arakelovMulHeight₁ x)

theorem NumberField.arakelovMulHeight₁_eq_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovMulHeight₁ x = arakelovMulHeight ![x, 1]

theorem NumberField.arakelovLogHeight₁_eq_log_arakelovMulHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovLogHeight₁ x = Real.log (arakelovMulHeight₁ x)

theorem NumberField.arakelovLogHeight₁_eq_arakelovLogHeight {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovLogHeight₁ x = arakelovLogHeight ![x, 1]

theorem NumberField.arakelovMulHeight₁_eq {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovMulHeight₁ x = (∏ v : InfinitePlace K, (v x ^ 2 + 1) ^ (↑v.mult / 2)) * ∏ᶠ (v : FinitePlace K), max (v x) 1

The familiar formula for the Arakelov height of a single element.

@[simp]

theorem NumberField.arakelovMulHeight₁_zero {K : Type u_1} [Field K] [NumberField K] : arakelovMulHeight₁ 0 = 1

@[simp]

theorem NumberField.arakelovLogHeight₁_zero {K : Type u_1} [Field K] [NumberField K] : arakelovLogHeight₁ 0 = 0

theorem NumberField.one_le_arakelovMulHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : 1 ≤ arakelovMulHeight₁ x

theorem NumberField.arakelovMulHeight₁_pos {K : Type u_1} [Field K] [NumberField K] (x : K) : 0 < arakelovMulHeight₁ x

theorem NumberField.arakelovMulHeight₁_ne_zero {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovMulHeight₁ x ≠ 0

theorem NumberField.arakelovLogHeight₁_nonneg {K : Type u_1} [Field K] [NumberField K] (x : K) : 0 ≤ arakelovLogHeight₁ x

theorem NumberField.arakelovLogHeight₁_eq {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovLogHeight₁ x = ∑ v : InfinitePlace K, ↑v.mult / 2 * Real.log (v x ^ 2 + 1) + ∑ᶠ (v : FinitePlace K), (v x).posLog

The local formula for the affine logarithmic Arakelov height: the finite places contribute log⁺ (v x), the positive part of the logarithm.

theorem NumberField.arakelovMulHeight₁_one {K : Type u_1} [Field K] [NumberField K] : arakelovMulHeight₁ 1 = 2 ^ (↑(Height.totalWeight K) / 2)

The value of the affine Arakelov height at 1: 2 ^ (totalWeight K / 2), not 1. This is the positive form of the warning that arakelovMulHeight₁ is not Height.mulHeight₁; the two one-variable heights are related only by the comparison lemmas of Layer 0.2.

theorem NumberField.arakelovMulHeight₁_neg {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovMulHeight₁ (-x) = arakelovMulHeight₁ x

theorem NumberField.arakelovLogHeight₁_neg {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovLogHeight₁ (-x) = arakelovLogHeight₁ x

theorem NumberField.arakelovMulHeight₁_inv {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovMulHeight₁ x⁻¹ = arakelovMulHeight₁ x

The affine Arakelov height is invariant under inversion: H_Ar(x⁻¹ : 1) = H_Ar(x : 1), since both are the height of the projective point (x : 1) = (1 : x⁻¹).

theorem NumberField.arakelovLogHeight₁_inv {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovLogHeight₁ x⁻¹ = arakelovLogHeight₁ x

The comparison of Layer 0.2, applied to ![x, 1]. This is the only relation between the two one-variable heights: arakelovMulHeight₁ = mulHeight₁ is false, already at x = 1.

theorem NumberField.mulHeight₁_le_arakelovMulHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : Height.mulHeight₁ x ≤ arakelovMulHeight₁ x

theorem NumberField.arakelovMulHeight₁_le_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovMulHeight₁ x ≤ 2 ^ (↑(Height.totalWeight K) / 2) * Height.mulHeight₁ x

theorem NumberField.logHeight₁_le_arakelovLogHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : Height.logHeight₁ x ≤ arakelovLogHeight₁ x

theorem NumberField.arakelovLogHeight₁_le_logHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : arakelovLogHeight₁ x ≤ ↑(Height.totalWeight K) / 2 * Real.log 2 + Height.logHeight₁ x

The descent to projective space

Scaling invariance makes the Arakelov height a well-defined function on Projectivization K (ι → K), exactly as for Projectivization.mulHeight.

noncomputable def Projectivization.arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : ℝ

The multiplicative Arakelov height of a point of projective space over a number field.

Equations

• x.arakelovMulHeight = Projectivization.lift (fun (r : { v : ι → K // v ≠ 0 }) => NumberField.arakelovMulHeight ↑r) ⋯ x

noncomputable def Projectivization.arakelovLogHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : ℝ

The logarithmic Arakelov height of a point of projective space over a number field.

Equations

• x.arakelovLogHeight = Projectivization.lift (fun (r : { v : ι → K // v ≠ 0 }) => NumberField.arakelovLogHeight ↑r) ⋯ x

theorem Projectivization.arakelovMulHeight_mk {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] {x : ι → K} (hx : x ≠ 0) : (mk K x hx).arakelovMulHeight = NumberField.arakelovMulHeight x

theorem Projectivization.arakelovLogHeight_mk {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] {x : ι → K} (hx : x ≠ 0) : (mk K x hx).arakelovLogHeight = NumberField.arakelovLogHeight x

theorem Projectivization.arakelovLogHeight_eq_log_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : x.arakelovLogHeight = Real.log x.arakelovMulHeight

theorem Projectivization.one_le_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : 1 ≤ x.arakelovMulHeight

theorem Projectivization.arakelovMulHeight_pos {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : 0 < x.arakelovMulHeight

theorem Projectivization.arakelovMulHeight_ne_zero {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : x.arakelovMulHeight ≠ 0

theorem Projectivization.arakelovLogHeight_nonneg {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : 0 ≤ x.arakelovLogHeight

@[simp]

theorem Projectivization.arakelovMulHeight_eq_one_of_subsingleton {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Subsingleton ι] (x : Projectivization K (ι → K)) : x.arakelovMulHeight = 1

On a subsingleton index type every point of projective space has Arakelov height 1; the projective form of NumberField.arakelovMulHeight_eq_one_of_subsingleton, and the degenerate case in which the Arakelov and sup-norm normalizations agree.

@[simp]

theorem Projectivization.arakelovLogHeight_eq_zero_of_subsingleton {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Subsingleton ι] (x : Projectivization K (ι → K)) : x.arakelovLogHeight = 0

Comparison of the two normalizations on projective space

NumberField.mulHeight_le_arakelovMulHeight and NumberField.arakelovMulHeight_le_mulHeight read on Projectivization K (ι → K). Both sides are computed on any representative, so the comparisons descend to projective space with the same constant.

theorem Projectivization.mulHeight_le_arakelovMulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : x.mulHeight ≤ x.arakelovMulHeight

The projective sup-norm height is at most the projective Arakelov height.

theorem Projectivization.arakelovMulHeight_le_mulHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Nonempty ι] (x : Projectivization K (ι → K)) : x.arakelovMulHeight ≤ ↑(Fintype.card ι) ^ (↑(Height.totalWeight K) / 2) * x.mulHeight

The projective Arakelov height is at most #ι ^ (totalWeight K / 2) times the projective sup-norm height, with the constant — sharp — of NumberField.arakelovMulHeight_le_mulHeight.

theorem Projectivization.logHeight_le_arakelovLogHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (x : Projectivization K (ι → K)) : x.logHeight ≤ x.arakelovLogHeight

theorem Projectivization.arakelovLogHeight_le_logHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [Nonempty ι] (x : Projectivization K (ι → K)) : x.arakelovLogHeight ≤ ↑(Height.totalWeight K) / 2 * Real.log ↑(Fintype.card ι) + x.logHeight

positivity extensions

The Arakelov heights are positive (multiplicative) resp. nonnegative (logarithmic), exactly as their sup-norm counterparts in Mathlib.NumberTheory.Height.Basic.

def Mathlib.Meta.Positivity.evalArakelovMulHeight : PositivityExt

Extension for the positivity tactic: NumberField.arakelovMulHeight is always positive.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalArakelovLogHeight : PositivityExt

Extension for the positivity tactic: NumberField.arakelovLogHeight is always nonnegative.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalArakelovMulHeight₁ : PositivityExt

Extension for the positivity tactic: NumberField.arakelovMulHeight₁ is always positive.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalArakelovLogHeight₁ : PositivityExt

Extension for the positivity tactic: NumberField.arakelovLogHeight₁ is always nonnegative.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalProjArakelovMulHeight : PositivityExt

Extension for the positivity tactic: Projectivization.arakelovMulHeight is always positive.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalProjArakelovLogHeight : PositivityExt

Extension for the positivity tactic: Projectivization.arakelovLogHeight is always nonnegative.

Equations

• One or more equations did not get rendered due to their size.

Worked examples

Cheap checks that the definition means what it should. Over ℚ the two normalizations of the height of the point (1 : 1) genuinely differ, so the √N factors in the Siegel-lemma literature are not cosmetic and a proof that silently interchanges the two heights is wrong.

The third shows that the constant of arakelovMulHeight_le_mulHeight is attained, so it cannot be improved. The last two are rejection tests: they refute the two lemmas of Mathlib.NumberTheory.Height.Basic that a reader would expect to carry over to this normalization and that do not.