instance instContinuousSMulRealComplex : ContinuousSMul ℝ ℂ

The scalar multiplication of ℝ on ℂ is continuous, exhibited as a ContinuousSMul instance. This is used downstream when differentiating real-linear maps with complex codomain.

noncomputable def DifferentialOperators.coordCLM {n : ℕ} (i : Fin n) : EuclideanSpace ℝ (Fin n) →L[ℝ] ℂ

The continuous real-linear map sending ξ ∈ EuclideanSpace ℝ (Fin n) to its i-th coordinate, viewed as a complex number (ξ i : ℂ).

@[simp]

theorem DifferentialOperators.coordCLM_apply {n : ℕ} (i : Fin n) (ξ : EuclideanSpace ℝ (Fin n)) : (coordCLM i) ξ = ↑(ξ.ofLp i)

Evaluating coordCLM i at ξ returns (ξ i : ℂ).

theorem DifferentialOperators.evalAtReal_differentiable {n : ℕ} (Q : MvPolynomial (Fin n) ℂ) : Differentiable ℝ (evalAtReal Q)

The evaluation of a multivariate complex polynomial at a real point, viewed as a function EuclideanSpace ℝ (Fin n) → ℂ, is real-differentiable everywhere.

theorem DifferentialOperators.fderiv_evalAtReal_single {n : ℕ} (Q : MvPolynomial (Fin n) ℂ) (j : Fin n) (ξ : EuclideanSpace ℝ (Fin n)) : (fderiv ℝ (evalAtReal Q) ξ) (EuclideanSpace.single j 1) = evalAtReal ((MvPolynomial.pderiv j) Q) ξ

The directional derivative of evalAtReal Q along the j-th standard basis vector equals the evaluation of the formal partial derivative pderiv j Q.

theorem DifferentialOperators.hasDerivAt_curve {n : ℕ} (ξ : EuclideanSpace ℝ (Fin n)) (j : Fin n) : HasDerivAt (fun (t : ℝ) => ξ + t • EuclideanSpace.single j 1) (EuclideanSpace.single j 1) 0

The straight-line curve t ↦ ξ + t · eⱼ from ξ in the direction of the j-th basis vector has derivative eⱼ at t = 0.

theorem DifferentialOperators.quotient_fderiv_step {n : ℕ} (P Q : MvPolynomial (Fin n) ℂ) (k : ℕ) (j : Fin n) (ξ : EuclideanSpace ℝ (Fin n)) (hP : evalAtReal P ξ ≠ 0) : (fderiv ℝ (fun (ξ' : EuclideanSpace ℝ (Fin n)) => evalAtReal Q ξ' / evalAtReal P ξ' ^ k) ξ) (EuclideanSpace.single j 1) = evalAtReal (P * (MvPolynomial.pderiv j) Q - k • (Q * (MvPolynomial.pderiv j) P)) ξ / evalAtReal P ξ ^ (k + 1)

A "quotient rule" for the directional derivative of Q / P^k: at any point where P does not vanish, the directional derivative along eⱼ of ξ' ↦ evalAtReal Q ξ' / (evalAtReal P ξ')^k equals evalAtReal (P · pderiv j Q − k · (Q · pderiv j P)) ξ / (evalAtReal P ξ)^(k+1). This is the inductive step used to compute derivatives of polyReciprocal.