Real points of a Weierstrass curve

Over ℝ, completing the square writes the Weierstrass equation as (2y + a₁x + a₃)² = Ψ₂Sq(x), where Ψ₂Sq(x) = 4x³ + b₂x² + 2b₄x + b₆ is Mathlib's WeierstrassCurve.Ψ₂Sq. So the curve has a real point with abscissa x exactly when Ψ₂Sq(x) ≥ 0. The two points (x, y) and -(x, y) over such an x coincide exactly when Ψ₂Sq(x) = 0, that is, at the points of order two. These are the facts that let the real period integral ∫_{Ψ₂Sq(x) > 0} dx / √Ψ₂Sq(x) be read as an integral over the real points that are not 2-torsion.

The shape of the real locus is read off the real roots of the cubic Ψ₂Sq, whose leading coefficient is 4. It has a largest real root e, beyond which it is positive, and the abscissas of the real points are bounded below. On an elliptic curve the roots are simple. So either Ψ₂Sq < 0 below e, and every real point other than O has abscissa at least e, or Ψ₂Sq has three real roots e₁ < e₂ < e, and the abscissas of the real points fill [e₁, e₂] ∪ [e, ∞).

Main results

• WeierstrassCurve.Affine.exists_equation_iff_nonneg_eval_Ψ₂Sq: there is a real point with abscissa x exactly when Ψ₂Sq(x) ≥ 0; exists_nonsingular_of_nonneg_eval_Ψ₂Sq is the same for a nonsingular point on an elliptic curve.
• WeierstrassCurve.Affine.tendsto_eval_Ψ₂Sq_atTop and tendsto_eval_Ψ₂Sq_atBot: Ψ₂Sq tends to ±∞ at ±∞.
• WeierstrassCurve.Affine.bddBelow_setOf_nonneg_eval_Ψ₂Sq: the abscissas of the real points are bounded below.
• WeierstrassCurve.Affine.exists_isRoot_Ψ₂Sq_and_forall_lt_pos_eval: Ψ₂Sq has a real root e beyond which it is positive.
• WeierstrassCurve.Affine.exists_Ψ₂Sq_eq_prod_three_roots: on an elliptic curve with a real point of abscissa below that root e, Ψ₂Sq = 4 (X - e₁)(X - e₂)(X - e) with e₁ < e₂ < e.
• WeierstrassCurve.pos_eval_Ψ₂Sq_iff_of_eq_prod_three_roots: with three real roots e₁ < e₂ < e₃, Ψ₂Sq is positive exactly on (e₁, e₂) ∪ (e₃, ∞).
• WeierstrassCurve.Affine.Point.neg_ne_self_iff_ne_zero_and_pos_eval_Ψ₂Sq: a point is not 2-torsion exactly when it is affine and Ψ₂Sq is positive at its abscissa, over any ordered field; Point.neg_some_ne_some_iff_pos_eval_Ψ₂Sq is the affine case.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.1.

theorem WeierstrassCurve.Affine.exists_equation_iff_nonneg_eval_Ψ₂Sq {W : Affine ℝ} {x : ℝ} : (∃ (y : ℝ), W.Equation x y) ↔ 0 ≤ Polynomial.eval x (Ψ₂Sq W)

A real Weierstrass curve has a point with abscissa x exactly when Ψ₂Sq(x) ≥ 0. One such point has 2y + a₁x + a₃ = √Ψ₂Sq(x).

theorem WeierstrassCurve.Affine.exists_nonsingular_of_nonneg_eval_Ψ₂Sq {W : Affine ℝ} [WeierstrassCurve.IsElliptic W] {x : ℝ} (hx : 0 ≤ Polynomial.eval x (Ψ₂Sq W)) : ∃ (y : ℝ), W.Nonsingular x y

Over each x with Ψ₂Sq(x) ≥ 0, an elliptic curve over ℝ has a real point.

theorem WeierstrassCurve.Affine.Point.neg_ne_self_iff_ne_zero_and_pos_eval_Ψ₂Sq {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {W : Affine F} {P : W.Point} : -P ≠ P ↔ P ≠ 0 ∧ 0 < Polynomial.eval P.xCoord (Ψ₂Sq W)

A point is not 2-torsion exactly when it is affine and Ψ₂Sq is positive at its abscissa, over an ordered field such as ℝ. At an affine point (x, y), Ψ₂Sq(x) = (2y + a₁x + a₃)², which vanishes exactly at the points of order two.

theorem WeierstrassCurve.Affine.Point.neg_some_ne_some_iff_pos_eval_Ψ₂Sq {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : -some x y h ≠ some x y h ↔ 0 < Polynomial.eval x (Ψ₂Sq W)

An affine point (x, y) is not 2-torsion exactly when Ψ₂Sq(x) > 0, over an ordered field such as ℝ.

The real roots of Ψ₂Sq

theorem WeierstrassCurve.Affine.tendsto_eval_Ψ₂Sq_atTop {W : Affine ℝ} : Filter.Tendsto (fun (x : ℝ) => Polynomial.eval x (Ψ₂Sq W)) Filter.atTop Filter.atTop

Ψ₂Sq(x) → ∞ as x → ∞: it is a cubic with leading coefficient 4.

theorem WeierstrassCurve.Affine.tendsto_eval_Ψ₂Sq_atBot {W : Affine ℝ} : Filter.Tendsto (fun (x : ℝ) => Polynomial.eval x (Ψ₂Sq W)) Filter.atBot Filter.atBot

Ψ₂Sq(x) → -∞ as x → -∞: it is a cubic with leading coefficient 4.

theorem WeierstrassCurve.Affine.bddBelow_setOf_nonneg_eval_Ψ₂Sq {W : Affine ℝ} : BddBelow {x : ℝ | 0 ≤ Polynomial.eval x (Ψ₂Sq W)}

The abscissas of the real points are bounded below: Ψ₂Sq is a cubic with positive leading coefficient, so it is negative far to the left.

theorem WeierstrassCurve.Affine.exists_isRoot_Ψ₂Sq_and_forall_lt_pos_eval (W : Affine ℝ) : ∃ (e : ℝ), (Ψ₂Sq W).IsRoot e ∧ ∀ ⦃x : ℝ⦄, e < x → 0 < Polynomial.eval x (Ψ₂Sq W)

Ψ₂Sq has a real root beyond which it is positive: its largest real root. It exists since Ψ₂Sq is a cubic with positive leading coefficient.

theorem WeierstrassCurve.Affine.exists_Ψ₂Sq_eq_prod_three_roots {W : Affine ℝ} [WeierstrassCurve.IsElliptic W] {e : ℝ} (he : (Ψ₂Sq W).IsRoot e) (hpos : ∀ ⦃x : ℝ⦄, e < x → 0 < Polynomial.eval x (Ψ₂Sq W)) {x₀ : ℝ} (hx₀ : x₀ < e) (h₀ : 0 ≤ Polynomial.eval x₀ (Ψ₂Sq W)) : ∃ (e₁ : ℝ) (e₂ : ℝ), e₁ < e₂ ∧ e₂ < e ∧ Ψ₂Sq W = Polynomial.C 4 * (Polynomial.X - Polynomial.C e₁) * (Polynomial.X - Polynomial.C e₂) * (Polynomial.X - Polynomial.C e)

Three real roots. Let e be a root of Ψ₂Sq beyond which it is positive, on an elliptic curve over ℝ. If Ψ₂Sq(x₀) ≥ 0 for some x₀ < e, that is, if some real point has abscissa below e, then Ψ₂Sq = 4 (X - e₁)(X - e₂)(X - e) with e₁ < e₂ < e.

theorem WeierstrassCurve.pos_eval_Ψ₂Sq_iff_of_eq_prod_three_roots (W : WeierstrassCurve ℝ) {e₁ e₂ e₃ : ℝ} (h₁₂ : e₁ < e₂) (h₂₃ : e₂ < e₃) (h : W.Ψ₂Sq = Polynomial.C 4 * (Polynomial.X - Polynomial.C e₁) * (Polynomial.X - Polynomial.C e₂) * (Polynomial.X - Polynomial.C e₃)) (x : ℝ) : 0 < Polynomial.eval x W.Ψ₂Sq ↔ x ∈ Set.Ioo e₁ e₂ ∪ Set.Ioi e₃

Where Ψ₂Sq is positive, with three real roots: if Ψ₂Sq = 4 (X - e₁)(X - e₂)(X - e₃) with e₁ < e₂ < e₃, then Ψ₂Sq(x) > 0 exactly on (e₁, e₂) ∪ (e₃, ∞).