Derivations and the sum of two points

For two nonzero points P, Q of a Weierstrass curve W⁄K with P + Q ≠ 0, and a derivation D on K over R, the derivation of the x-coordinate of P + Q is expressed through the derivations of the x-coordinates of P and Q: this is Affine/Formula/Derivation.lean's identity for the coordinates of the addition law, read on the points through Point.xCoord and Point.yCoord.

Main statements

• WeierstrassCurve.Affine.Point.derivation_xCoord_add: if W_Y = 2Y + a₁X + a₃ does not vanish at P and Q (when their x-coordinates differ), then D x(P + Q) = W_Y(P + Q) • (W_Y(P)⁻¹ • D x(P) + W_Y(Q)⁻¹ • D x(Q)).
• WeierstrassCurve.Affine.Point.inv_smul_derivation_xCoord_add: for nonzero P, Q with P + Q ≠ 0, if W_Y does not vanish at P + Q, nor at P and Q when their x-coordinates differ, then W_Y(P + Q)⁻¹ • D x(P + Q) = W_Y(P)⁻¹ • D x(P) + W_Y(Q)⁻¹ • D x(Q).

theorem WeierstrassCurve.Affine.Point.derivation_xCoord_add {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) [DecidableEq K] {P Q : (toAffine (Affine.baseChange W K)).Point} (hP : P ≠ 0) (hQ : Q ≠ 0) (h : P + Q ≠ 0) (huP : P.xCoord ≠ Q.xCoord → Polynomial.evalEval P.xCoord P.yCoord (toAffine (Affine.baseChange W K)).polynomialY ≠ 0) (huQ : P.xCoord ≠ Q.xCoord → Polynomial.evalEval Q.xCoord Q.yCoord (toAffine (Affine.baseChange W K)).polynomialY ≠ 0) : D (P + Q).xCoord = Polynomial.evalEval (P + Q).xCoord (P + Q).yCoord (toAffine (Affine.baseChange W K)).polynomialY • ((Polynomial.evalEval P.xCoord P.yCoord (toAffine (Affine.baseChange W K)).polynomialY)⁻¹ • D P.xCoord + (Polynomial.evalEval Q.xCoord Q.yCoord (toAffine (Affine.baseChange W K)).polynomialY)⁻¹ • D Q.xCoord)

The derivation of the x-coordinate of a sum of points. For nonzero points P, Q of W⁄K with P + Q ≠ 0, at both of which W_Y = 2Y + a₁X + a₃ does not vanish when their x-coordinates differ, D x(P + Q) = W_Y(P + Q) • (W_Y(P)⁻¹ • D x(P) + W_Y(Q)⁻¹ • D x(Q)).

theorem WeierstrassCurve.Affine.Point.inv_smul_derivation_xCoord_add {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) [DecidableEq K] {P Q : (toAffine (Affine.baseChange W K)).Point} (hP : P ≠ 0) (hQ : Q ≠ 0) (h : P + Q ≠ 0) (huP : P.xCoord ≠ Q.xCoord → Polynomial.evalEval P.xCoord P.yCoord (toAffine (Affine.baseChange W K)).polynomialY ≠ 0) (huQ : P.xCoord ≠ Q.xCoord → Polynomial.evalEval Q.xCoord Q.yCoord (toAffine (Affine.baseChange W K)).polynomialY ≠ 0) (hu : Polynomial.evalEval (P + Q).xCoord (P + Q).yCoord (toAffine (Affine.baseChange W K)).polynomialY ≠ 0) : (Polynomial.evalEval (P + Q).xCoord (P + Q).yCoord (toAffine (Affine.baseChange W K)).polynomialY)⁻¹ • D (P + Q).xCoord = (Polynomial.evalEval P.xCoord P.yCoord (toAffine (Affine.baseChange W K)).polynomialY)⁻¹ • D P.xCoord + (Polynomial.evalEval Q.xCoord Q.yCoord (toAffine (Affine.baseChange W K)).polynomialY)⁻¹ • D Q.xCoord

The differential dx / W_Y is additive on points: for nonzero points P, Q of W⁄K with P + Q ≠ 0, if W_Y does not vanish at P + Q, nor at P and Q when their x-coordinates differ, then W_Y(P + Q)⁻¹ • D x(P + Q) = W_Y(P)⁻¹ • D x(P) + W_Y(Q)⁻¹ • D x(Q).