The canonical height as a limit along all multiples

The canonical height is constructed by averaging the naïve x-height along powers of two. Here we prove the classical formula

canonicalHeight P = lim_{n → ∞} naiveHeight (n • P) / n².

Convergence is uniform in the point: the error is bounded by C / n², with C depending only on the curve. No Northcott or number-field assumption is needed. We also characterize the canonical height as the unique quadratic map at bounded distance from the naïve height. This fixes its normalization without referring to the doubling sequence used to construct it.

Main results

• WeierstrassCurve.Affine.Point.exists_abs_naiveHeight_nsmul_div_sq_sub_le: a uniform error bound.
• WeierstrassCurve.Affine.tendstoUniformly_naiveHeight_nsmul_div_sq: uniform convergence.
• WeierstrassCurve.Affine.Point.tendsto_naiveHeight_nsmul_div_sq: the classical pointwise limit.
• WeierstrassCurve.Affine.canonicalHeightQuadratic_eq_iff: the bounded-distance characterization.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.9.

theorem WeierstrassCurve.Affine.Point.exists_abs_naiveHeight_nsmul_div_sq_sub_le {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] [DecidableEq F] {W : Affine F} [WeierstrassCurve.IsElliptic (toAffine W)] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), n ≠ 0 → ∀ (P : W.Point), |(n • P).naiveHeight / ↑n ^ 2 - P.canonicalHeight| ≤ C / ↑n ^ 2

The normalized naïve heights approximate the canonical height with an error bounded uniformly in the point by C / n², for every nonzero natural number n.

theorem WeierstrassCurve.Affine.tendstoUniformly_naiveHeight_nsmul_div_sq {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] [DecidableEq F] {W : Affine F} [WeierstrassCurve.IsElliptic (toAffine W)] : TendstoUniformly (fun (n : ℕ) (P : W.Point) => (n • P).naiveHeight / ↑n ^ 2) (fun (P : W.Point) => P.canonicalHeight) Filter.atTop

The normalized naïve heights converge to the canonical height uniformly over all points.

theorem WeierstrassCurve.Affine.Point.tendsto_naiveHeight_nsmul_div_sq {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] [DecidableEq F] {W : Affine F} [WeierstrassCurve.IsElliptic (toAffine W)] (P : W.Point) : Filter.Tendsto (fun (n : ℕ) => (n • P).naiveHeight / ↑n ^ 2) Filter.atTop (nhds P.canonicalHeight)

The classical limit formula for the canonical height, along all natural multiples.

theorem WeierstrassCurve.Affine.Point.canonicalHeight_eq_limUnder_naiveHeight_nsmul_div_sq {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] [DecidableEq F] {W : Affine F} [WeierstrassCurve.IsElliptic (toAffine W)] (P : W.Point) : P.canonicalHeight = Filter.atTop.limUnder fun (n : ℕ) => (n • P).naiveHeight / ↑n ^ 2

The canonical height is the limit of the normalized naïve heights along all multiples.

theorem WeierstrassCurve.Affine.canonicalHeightQuadratic_eq_iff {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] [DecidableEq F] (W : Affine F) [WeierstrassCurve.IsElliptic (toAffine W)] (q : QuadraticMap ℤ W.Point ℝ) : W.canonicalHeightQuadratic = q ↔ ∃ (C : ℝ), ∀ (P : W.Point), |q P - P.naiveHeight| ≤ C

The canonical height is exactly the quadratic map at bounded distance from the naïve height.