Constant and first coefficients of a plane equation under a linear one-parameter displacement of one coordinate. These are algebraic coefficient identities, valid for arbitrary commutative target algebras.

noncomputable def CCDN.planeLinearDeformation {K : Type u_1} {A : Type u_2} [CommRing K] [CommRing A] [Algebra K A] (a : Fin 2 → A) (k : Fin 2) (w : A) : MvPolynomial (Fin 2) K →ₐ[K] Polynomial A

Vary one plane coordinate by t*w in an arbitrary target algebra.

Equations

• CCDN.planeLinearDeformation a k w = MvPolynomial.aeval fun (j : Fin 2) => Polynomial.C (a j) + if j = k then Polynomial.X * Polynomial.C w else 0

theorem CCDN.planeLinearDeformation_coeff_zero {K : Type u_1} {A : Type u_2} [CommRing K] [CommRing A] [Algebra K A] (a : Fin 2 → A) (k : Fin 2) (w : A) (f : MvPolynomial (Fin 2) K) : ((planeLinearDeformation a k w) f).coeff 0 = (MvPolynomial.aeval a) f

The constant coefficient of the linear deformation of f at a is the value f(a).

theorem CCDN.planeLinearDeformation_coeff_one {K : Type u_1} {A : Type u_2} [CommRing K] [CommRing A] [Algebra K A] (a : Fin 2 → A) (k : Fin 2) (w : A) (f : MvPolynomial (Fin 2) K) : ((planeLinearDeformation a k w) f).coeff 1 = (MvPolynomial.aeval a) ((MvPolynomial.pderiv k) f) * w

The linear coefficient of the deformation of f at a along coordinate k with speed w is (∂f/∂x_k)(a) * w.