The real period of a Weierstrass curve over ℝ

Let W be a Weierstrass curve over ℝ and ω = dx / (2y + a₁x + a₃) its invariant differential. On the curve (2y + a₁x + a₃)² = Ψ₂Sq(x), where

Ψ₂Sq(x) = 4x³ + b₂x² + 2b₄x + b₆

is Mathlib's WeierstrassCurve.Ψ₂Sq. A real point with abscissa x exists exactly when Ψ₂Sq(x) ≥ 0, and over each x with Ψ₂Sq(x) > 0 there are two real points, on which |ω| = dx / √Ψ₂Sq(x). The real period of W is therefore defined by the explicit integral

Ω(W) = 2 ∫_{Ψ₂Sq(x) > 0} dx / √Ψ₂Sq(x),

the factor 2 counting the two branches of y. It treats curves with one real component (Δ < 0) and with two (Δ > 0) uniformly. The integral is a Lebesgue integral of a nonnegative function, WeierstrassCurve.realPeriodLIntegral, with values in ℝ≥0∞, and WeierstrassCurve.realPeriod is twice its value as a real number. So that a divergent integral cannot silently read as 0, the finiteness is a theorem: for an elliptic curve the integral is finite and positive.

The singularities of the integrand are the real roots of Ψ₂Sq. On an elliptic curve the discriminant of the cubic Ψ₂Sq is 16 Δ ≠ 0, so its three complex roots e₁, e₂, e₃ are distinct, and |Ψ₂Sq(x)| = 4 |x - e₁| |x - e₂| |x - e₃|. Near a root only one factor is small, so the integrand is at most a constant times |x - Re eᵢ|^(-1/2), which is integrable; far from the roots it is at most a constant times (1 + |x|)^(-3/2), which is integrable at infinity.

Under a change of variables C = (u, r, s, t) the invariant differential becomes u ω, and correspondingly Ω(C • W) = |u| Ω(W). In particular the period is unchanged by a change of variables with u = ±1, which is the residual freedom between minimal Weierstrass equations over ℤ. Taking the absolute value |ω| is what makes the period independent of the sign of u: the automorphism [-1] of the curve pulls ω back to -ω.

More generally, a map of curves W → W' given in coordinates by x' = r(x) and 2y' + a₁'x' + a₃' = s(x) (2y + a₁x + a₃), and pulling ω' back to c ω, satisfies Ψ₂Sq'(r(x)) = s(x)² Ψ₂Sq(x) and r'(x) = c s(x). This is the shape of an isogeny, whose x-coordinate is a rational function of x. Then |c| dx / √Ψ₂Sq(x) = |r'(x)| dx / √Ψ₂Sq'(r(x)), and the area formula turns the real period integral of W, scaled by |c|, into the integral of dx' / √Ψ₂Sq'(x') weighted by the number of x with Ψ₂Sq(x) > 0 over each x'. When that number is a constant n, this reads |c| Ω(W) = n Ω(W').

When Ψ₂Sq = 4 (x - e₁)(x - e₂)(x - e₃) has three real roots e₁ < e₂ < e₃, the curve has two real components, over [e₁, e₂] and over [e₃, ∞), and each carries half of the period. The substitution x ↦ e₁ + (e₁ - e₂)(e₁ - e₃) / (x - e₁), which on points is translation by the point of order two over e₁, carries (e₃, ∞) onto (e₁, e₂) and preserves dx / √Ψ₂Sq(x).

Main definitions

• WeierstrassCurve.realPeriodLIntegral: the integral ∫_{Ψ₂Sq(x) > 0} dx / √Ψ₂Sq(x) in ℝ≥0∞.
• WeierstrassCurve.realPeriod: the real period Ω(W), twice the real value of that integral.

Main results

• WeierstrassCurve.realPeriodLIntegral_eq_lintegral: the integrand vanishes off the set Ψ₂Sq(x) > 0, so the integral may be taken over all of ℝ.
• WeierstrassCurve.realPeriodLIntegral_pos: the integral is positive, for every curve.
• WeierstrassCurve.realPeriodLIntegral_lt_top: the integral is finite on an elliptic curve.
• WeierstrassCurve.ofReal_realPeriod: on an elliptic curve, Ω(W) is exactly twice the integral.
• WeierstrassCurve.realPeriod_pos: the real period of an elliptic curve is positive.
• WeierstrassCurve.realPeriodLIntegral_variableChange and WeierstrassCurve.realPeriod_variableChange: Ω(C • W) = |u| Ω(W).
• WeierstrassCurve.realPeriod_baseChange_variableChange: the same scaling for the base change to ℝ of a curve over a ring such as ℚ.
• WeierstrassCurve.ofReal_abs_mul_realPeriodLIntegral_eq_setLIntegral_encard: the real period integral under a substitution x' = r(x), with the fibres of r counted.
• WeierstrassCurve.ofReal_abs_mul_realPeriodLIntegral_eq_of_ae_encard_eq and WeierstrassCurve.abs_mul_realPeriod_eq_of_ae_encard_eq: |c| Ω(W) = n Ω(W') when almost every fibre has n elements.
• WeierstrassCurve.setLIntegral_Ioo_eq_setLIntegral_Ioi and WeierstrassCurve.realPeriodLIntegral_eq_two_mul_setLIntegral_Ioi: with three real roots e₁ < e₂ < e₃, the integrals over (e₁, e₂) and over (e₃, ∞) agree, so each is half of the real period integral.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.1 and Appendix C, §16.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §3.3 (the area formula).

noncomputable def WeierstrassCurve.realPeriodLIntegral (W : WeierstrassCurve ℝ) : ENNReal

The integral ∫_{Ψ₂Sq(x) > 0} dx / √Ψ₂Sq(x) of a Weierstrass curve over ℝ, where Ψ₂Sq(x) = 4x³ + b₂x² + 2b₄x + b₆ is the square of 2y + a₁x + a₃ on the curve, as a value in ℝ≥0∞. It is finite for an elliptic curve (WeierstrassCurve.realPeriodLIntegral_lt_top), and whenever it is finite it is half the real period WeierstrassCurve.realPeriod (WeierstrassCurve.ofReal_realPeriod).

noncomputable def WeierstrassCurve.realPeriod (W : WeierstrassCurve ℝ) : ℝ

The real period Ω(W) of a Weierstrass curve over ℝ, defined as twice the real value of WeierstrassCurve.realPeriodLIntegral. When that integral is finite, for instance for an elliptic curve (WeierstrassCurve.ofReal_realPeriod), this is Ω(W) = 2 ∫_{Ψ₂Sq(x) > 0} dx / √Ψ₂Sq(x); when it diverges, Ω(W) = 0. The motivation is that this integral computes ∫ |ω| over the real points, ω = dx / (2y + a₁x + a₃) being the invariant differential and the factor 2 counting the two real points over each x.

theorem WeierstrassCurve.realPeriodLIntegral_def (W : WeierstrassCurve ℝ) : W.realPeriodLIntegral = ∫⁻ (x : ℝ) in {x : ℝ | 0 < Polynomial.eval x W.Ψ₂Sq}, ENNReal.ofReal (√(Polynomial.eval x W.Ψ₂Sq))⁻¹

The defining integral of WeierstrassCurve.realPeriodLIntegral, over the set where Ψ₂Sq > 0.

theorem WeierstrassCurve.realPeriod_def (W : WeierstrassCurve ℝ) : W.realPeriod = 2 * W.realPeriodLIntegral.toReal

The real period is twice the real value of WeierstrassCurve.realPeriodLIntegral.

The integrand

theorem WeierstrassCurve.realPeriodLIntegral_eq_lintegral (W : WeierstrassCurve ℝ) : W.realPeriodLIntegral = ∫⁻ (x : ℝ), ENNReal.ofReal (√(Polynomial.eval x W.Ψ₂Sq))⁻¹

The integrand of the real period vanishes off the set Ψ₂Sq(x) > 0, so the integral may be taken over all of ℝ.

theorem WeierstrassCurve.realPeriodLIntegral_pos (W : WeierstrassCurve ℝ) : 0 < W.realPeriodLIntegral

The integral of the real period is positive, for every Weierstrass curve over ℝ: the cubic Ψ₂Sq has leading coefficient 4, so it is positive on a half-line.

Finiteness

theorem WeierstrassCurve.realPeriodLIntegral_lt_top (W : WeierstrassCurve ℝ) [W.IsElliptic] : W.realPeriodLIntegral < ⊤

The real period integral of an elliptic curve is finite.

theorem WeierstrassCurve.ofReal_realPeriod (W : WeierstrassCurve ℝ) [W.IsElliptic] : ENNReal.ofReal W.realPeriod = 2 * W.realPeriodLIntegral

On an elliptic curve, the real period is exactly twice the integral ∫_{Ψ₂Sq(x) > 0} dx / √Ψ₂Sq(x).

theorem WeierstrassCurve.realPeriod_pos (W : WeierstrassCurve ℝ) [W.IsElliptic] : 0 < W.realPeriod

The real period of an elliptic curve is positive.

Changes of variables

@[simp]

theorem WeierstrassCurve.realPeriodLIntegral_variableChange (W : WeierstrassCurve ℝ) (C : VariableChange ℝ) : (C • W).realPeriodLIntegral = ENNReal.ofReal |↑C.u| * W.realPeriodLIntegral

Under a change of variables C = (u, r, s, t) the integral of the real period scales by |u|, as the invariant differential becomes u ω.

@[simp]

theorem WeierstrassCurve.realPeriod_variableChange (W : WeierstrassCurve ℝ) (C : VariableChange ℝ) : (C • W).realPeriod = |↑C.u| * W.realPeriod

The real period scales by |u| under a change of variables C = (u, r, s, t): Ω(C • W) = |u| Ω(W). In particular it is unchanged when u = ±1.

@[simp]

theorem WeierstrassCurve.realPeriod_baseChange_variableChange {R : Type u_1} [CommRing R] [Algebra R ℝ] (C : VariableChange R) (V : WeierstrassCurve R) : ((C • V).baseChange ℝ).realPeriod = |(algebraMap R ℝ) ↑C.u| * (V.baseChange ℝ).realPeriod

For a Weierstrass curve V over a ring R with an algebra map to ℝ (such as ℚ), the real period of the base change of C • V is |u| times that of V, u being read in ℝ.

Substitutions

theorem WeierstrassCurve.ofReal_abs_mul_realPeriodLIntegral_eq_setLIntegral_encard (W : WeierstrassCurve ℝ) {W' : WeierstrassCurve ℝ} {r s : ℝ → ℝ} {c : ℝ} {Z : Set ℝ} (hc : c ≠ 0) (hZ : Z.Countable) (hr : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → HasDerivAt r (c * s x) x) (hs : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → s x ≠ 0) (hΨ : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → Polynomial.eval (r x) W'.Ψ₂Sq = s x ^ 2 * Polynomial.eval x W.Ψ₂Sq) : ENNReal.ofReal |c| * W.realPeriodLIntegral = ∫⁻ (y : ℝ) in {y : ℝ | 0 < Polynomial.eval y W'.Ψ₂Sq}, ↑({x : ℝ | 0 < Polynomial.eval x W.Ψ₂Sq} ∩ r ⁻¹' {y}).encard * ENNReal.ofReal (√(Polynomial.eval y W'.Ψ₂Sq))⁻¹

The real period integral under a substitution x' = r(x), counting fibres. Suppose that on the set where Ψ₂Sq(x) > 0, away from a countable set Z, the function r has derivative r'(x) = c s(x) with c ≠ 0 and s(x) ≠ 0, and Ψ₂Sq'(r(x)) = s(x)² Ψ₂Sq(x), where Ψ₂Sq' is that of a second curve W'. Then |c| times the real period integral of W is the integral over Ψ₂Sq'(x') > 0 of dx' / √Ψ₂Sq'(x'), weighted by the number of x with Ψ₂Sq(x) > 0 and r(x) = x'. The hypotheses are those of a map (x, y) ↦ (r(x), …) sending 2y + a₁x + a₃ to s(x) (2y + a₁x + a₃) and pulling the invariant differential back to c ω.

theorem WeierstrassCurve.ofReal_abs_mul_realPeriodLIntegral_eq_of_ae_encard_eq (W : WeierstrassCurve ℝ) {W' : WeierstrassCurve ℝ} {r s : ℝ → ℝ} {c : ℝ} {Z : Set ℝ} (hc : c ≠ 0) (hZ : Z.Countable) (hr : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → HasDerivAt r (c * s x) x) (hs : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → s x ≠ 0) (hΨ : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → Polynomial.eval (r x) W'.Ψ₂Sq = s x ^ 2 * Polynomial.eval x W.Ψ₂Sq) {n : ℕ} (hn : ∀ᵐ (y : ℝ), 0 < Polynomial.eval y W'.Ψ₂Sq → ({x : ℝ | 0 < Polynomial.eval x W.Ψ₂Sq} ∩ r ⁻¹' {y}).encard = ↑n) : ENNReal.ofReal |c| * W.realPeriodLIntegral = ↑n * W'.realPeriodLIntegral

The real period integral under a substitution with constant fibre count. Under the hypotheses of WeierstrassCurve.ofReal_abs_mul_realPeriodLIntegral_eq_setLIntegral_encard, if almost every x' with Ψ₂Sq'(x') > 0 is r(x) for exactly n values x with Ψ₂Sq(x) > 0, then |c| times the real period integral of W is n times that of W'.

theorem WeierstrassCurve.abs_mul_realPeriod_eq_of_ae_encard_eq (W : WeierstrassCurve ℝ) {W' : WeierstrassCurve ℝ} {r s : ℝ → ℝ} {c : ℝ} {Z : Set ℝ} (hc : c ≠ 0) (hZ : Z.Countable) (hr : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → HasDerivAt r (c * s x) x) (hs : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → s x ≠ 0) (hΨ : ∀ (x : ℝ), 0 < Polynomial.eval x W.Ψ₂Sq → x ∉ Z → Polynomial.eval (r x) W'.Ψ₂Sq = s x ^ 2 * Polynomial.eval x W.Ψ₂Sq) {n : ℕ} (hn : ∀ᵐ (y : ℝ), 0 < Polynomial.eval y W'.Ψ₂Sq → ({x : ℝ | 0 < Polynomial.eval x W.Ψ₂Sq} ∩ r ⁻¹' {y}).encard = ↑n) : |c| * W.realPeriod = ↑n * W'.realPeriod

The real period under a substitution with constant fibre count: |c| Ω(W) = n Ω(W'), under the hypotheses of WeierstrassCurve.ofReal_abs_mul_realPeriodLIntegral_eq_of_ae_encard_eq.

Curves with three real roots

theorem WeierstrassCurve.setLIntegral_Ioo_eq_setLIntegral_Ioi (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 : ℝ) in Set.Ioo e₁ e₂, ENNReal.ofReal (√(Polynomial.eval x W.Ψ₂Sq))⁻¹ = ∫⁻ (x : ℝ) in Set.Ioi e₃, ENNReal.ofReal (√(Polynomial.eval x W.Ψ₂Sq))⁻¹

The two real components carry the same period. If Ψ₂Sq = 4 (X - e₁)(X - e₂)(X - e₃) with e₁ < e₂ < e₃, then ∫_{e₁}^{e₂} dx / √Ψ₂Sq(x) = ∫_{e₃}^∞ dx / √Ψ₂Sq(x): the substitution x ↦ e₁ + (e₁ - e₂)(e₁ - e₃) / (x - e₁) carries (e₃, ∞) onto (e₁, e₂) and preserves dx / √Ψ₂Sq(x).

theorem WeierstrassCurve.realPeriodLIntegral_eq_two_mul_setLIntegral_Ioi (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₃)) : W.realPeriodLIntegral = 2 * ∫⁻ (x : ℝ) in Set.Ioi e₃, ENNReal.ofReal (√(Polynomial.eval x W.Ψ₂Sq))⁻¹

With three real roots e₁ < e₂ < e₃, the component over (e₃, ∞) carries half of the real period integral: Ψ₂Sq is positive exactly on (e₁, e₂) ∪ (e₃, ∞), and the integrals over the two intervals agree by WeierstrassCurve.setLIntegral_Ioo_eq_setLIntegral_Ioi.