Directional derivatives of surfaces with absolutely irreducible top form.

noncomputable def CCDN.directionalDerivative {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] (v : σ → R) (f : MvPolynomial σ R) : MvPolynomial σ R

The derivative ∑ i, v i * ∂f/∂xᵢ of the polynomial f in the direction v.

Equations

• CCDN.directionalDerivative v f = ∑ i : σ, MvPolynomial.C (v i) * (MvPolynomial.pderiv i) f

theorem CCDN.directionalDerivative_totalDegree_le {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] (v : σ → K) (f : MvPolynomial σ K) : (directionalDerivative v f).totalDegree ≤ f.totalDegree - 1

A directional derivative of f has total degree at most f.totalDegree - 1.

theorem CCDN.surface_directionalDerivative_ne_zero (f : MvPolynomial (Fin 3) ℤ) (hir : HasAbsIrreducibleTopForm f) (hd : 2 ≤ f.totalDegree) (v : Fin 3 → ℚ) (hv : v ≠ 0) : directionalDerivative v ((MvPolynomial.map (Int.castRingHom ℚ)) f) ≠ 0

If the integer surface equation f has degree at least two and an absolutely irreducible top-degree form, then its derivative over ℚ in every nonzero direction v is nonzero.

@[simp]

theorem CCDN.directionalDerivative_C {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] (v : σ → R) (a : R) : directionalDerivative v (MvPolynomial.C a) = 0

Every directional derivative of a constant polynomial is zero.

@[simp]

theorem CCDN.directionalDerivative_X {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] (v : σ → R) (j : σ) : directionalDerivative v (MvPolynomial.X j) = MvPolynomial.C (v j)

The derivative of the coordinate X j in the direction v is the constant v j.

theorem CCDN.rationalAffineLine_contained_directionalDerivative {n : ℕ} (a v : RatPoint n) (f : CoordinatePolynomial n) (hline : rationalAffineLine a v ⊆ zeroLocus f) : rationalAffineLine a v ⊆ zeroLocus (directionalDerivative v f)

If the rational affine line through a with direction v lies on the hypersurface f = 0, then it also lies on the zero set of the derivative of f in the direction v.