lemmastandardinferred_dep

Basic properties of the height

Lemma·ht:height·§4.1 A weighted product formula

Statement (paper)

The value

h(u)

is independent of the chosen finite normal field and of the extensions of the prime absolute values in . For

u\in\mathcal N^\times

h(u^{-1})=h(u),\qquad \sum_v^*|\log|u|_v|=2h(u).

For arbitrary

u,v\in\mathcal N

h(uv)\le h(u)+h(v),\qquad h(u+v)\le h(u)+h(v)+\log2.

If a random

X\in\mathcal N

is independent of a uniformly sampled embedding

\sigma:\mathcal N\to\C

, then, for

B>1

and

0<r<1

\begin{aligned} \Prob\{|\sigma(X)|>B\}&\le\frac{\E h(X)}{\log B}, \\ \Prob\{X\ne0,\ |\sigma(X)|<r\} &\le\frac{\E h(X)}{\log(1/r)}. \end{aligned}

In plain English

The height

h(u)

does not depend on the chosen finite normal field or on the extensions of absolute values, satisfies

h(u^{-1})=h(u)

and

\sum_v^*|\log|u|_v|=2h(u)

for nonzero

u

, and obeys

h(uv)\le h(u)+h(v)

and

h(u+v)\le h(u)+h(v)+\log 2

. If a random

X\in\mathcal N

is independent of a uniform random embedding

\sigma

, then

\Prob\{|\sigma(X)|>B\}\le \E h(X)/\log B

and

\Prob\{X\ne0,\,|\sigma(X)|<r\}\le \E h(X)/\log(1/r)

Why it's here

Using the weighted product formula, the positive and negative parts of

\log|u|_v

have equal total weight, which gives the inversion symmetry and the identity

\sum_v^*|\log|u|_v|=2h(u)

. The ultrametric and triangle inequalities then give the product and sum bounds. Averaging over the uniform embedding and applying Markov's inequality turns the mean height into tail bounds, which later arguments use to control how large or small coordinates can be.

Classified standard:

These are the textbook properties of the absolute logarithmic Weil height: independence of the field, invariance under inversion, subadditivity for products and sums, and Markov-type tail bounds from the archimedean part (cf. Bombieri–Gubler, Heights in Diophantine Geometry). The probabilistic tail bounds are a direct Markov-inequality consequence of these properties.

Uses

lemWeighted product formula for number fields

Used by

propTotal variation S cannot stay boundedlemNegligible-height elements form an algebraically closed subfieldclaimNormalized coordinates with bounded mean heightsclaimCoupling tail bounds uniform in history

Sources

PaperOpen

Section: §4.1 A weighted product formula
Page: —
Label: ht:height
Line: sections/03-heights.tex:73

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
The proof invokes the normalized extensions and the "product formula" for the height, which is the weighted product formula of Lemma 4.1 ().