English
The derivative of the addPolynomial along slope is the negative sum of pairwise products of linear factors corresponding to x1, x2, and x3 = addX(x1,x2,slope).
Русский
Производная по переменной X от addPolynomial, взятая вдоль slope, равна минусу суммы попарных произведений линейных множителей (X−Cx1), (X−Cx2), (X−C x3).
LaTeX
$$$ \frac{d}{dX} W'.addPolynomial x_1 y_1 (W.slope x_1 x_2 y_1 y_2) = -\left[(X - C x_1)(X - C x_2) + (X - C x_1)(X - C (W.addX x_1 x_2 (W.slope x_1 x_2 y_1 y_2))) + (X - C x_2)(X - C (W.addX x_1 x_2 (W.slope x_1 x_2 y_1 y_2)))\right]$$$
Lean4
theorem derivative_addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
derivative (W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
-((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)) +
(X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) :=
by
rw [addPolynomial_slope h₁ h₂ hxy]
derivative_simp
ring1
