The naïve height and the approximate parallelogram law

This file defines the naïve height on an elliptic curve (over a field K with a theory of heights, i.e., satisfying [Height.AdmissibleAbsValues K]).

The final goal of this file is to prove the approximate parallelogram law for (affine) points on elliptic curves,

  |h(P+Q) + h(P-Q) - 2*(h(P) + h(Q))| ≤ C

where h is the naïve height, P and Q are affine points on a WeierstrassCurve and C is some real constant depending only on the Weierstrass model.

TODO

• Define the naïve height
• Add the further ingredients needed for the approximate parallelogram law
• Add the statement and proof of the approximate parallelogram law

theorem WeierstrassCurve.abs_logHeight_addSubMap_sub_two_mul_logHeight_le {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] (W : WeierstrassCurve K) [W.IsElliptic] : ∃ (C : ℝ), ∀ (x : Fin 3 → K), |(Height.logHeight fun (i : Fin 3) => (MvPolynomial.eval x) (W.addSubMap i)) - 2 * Height.logHeight x| ≤ C

If W is a Weierstrass curve over K, then the map F : ℙ² → ℙ² given by addSubMap W is a morphism.

This implies that |logHeight (F x) - 2 * logHeight x| ≤ C for a constant C, where x = ![s, t, u] and F acts on the coordinate vector.