The quotient rule for the Fréchet derivative

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.Calculus.FDeriv.Mul, beside HasFDerivAt.mul). BACKLOG #89.

Mathlib has the quotient rule for the one-dimensional derivative (HasDerivAt.div) and, for the Fréchet derivative, multiplication (HasFDerivAt.mul) and inversion in a normed division algebra (hasFDerivAt_inv'), but not the quotient of two maps into a normed field — a gap one meets as soon as a chart is a ratio of coordinates. MATHLIB-ABSENT(HasFDerivAt.div)

• ★ HasFDerivAt.div — f / g is differentiable where g does not vanish, with derivative (g x)⁻¹ • f' − (f x / g x ^ 2) • g'.

The target field K may be larger than the base field 𝕜 (the case this is written for: ℝ-Fréchet derivatives of ℂ-valued coordinate ratios), which is exactly what HasDerivAt.div cannot express and what ContDiffAt.div — stated for f g : E → 𝕜, the base field itself — does not cover either. The corresponding ContDiff statement needs no new lemma: ContDiffAt.inv is already general in the target field, so hf.mul (hg.inv hx) does it.

References: Mathlib/Analysis/Calculus/FDeriv/Mul.lean (HasFDerivAt.mul, hasFDerivAt_inv'); Mathlib/Analysis/Calculus/Deriv/Inv.lean (HasDerivAt.div); specs/BACKLOG.md #89; specs/future-work.md.

theorem HasFDerivAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {K : Type u_3} [NormedField K] [NormedAlgebra 𝕜 K] {f g : E → K} {f' g' : E →L[𝕜] K} {x : E} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) (hx : g x ≠ 0) : HasFDerivAt (fun (y : E) => f y / g y) ((g x)⁻¹ • f' - (f x / g x ^ 2) • g') x

★ The quotient rule for the Fréchet derivative, for maps into a normed field over the base field: where the denominator does not vanish, d(f / g) = (g x)⁻¹ • df − (f x / g x ^ 2) • dg.