Derivative rules on local domains

Logarithms and square roots need not be smooth everywhere. Their jet laws use smoothness near the evaluation point and a nonzero denominator or argument there. Continuity gives the same domain condition nearby, where mathlib's derivative rules identify the remaining jet coefficients.

The quotient law in NN.Proofs.Autograd.Dual supplies their division prerequisite and follows the runtime's arithmetic safeguards. These theorems concern exact-real coefficients, not native floating-point execution.

The principal angle is the imaginary part of the complex logarithm. Its dual tangent agrees with the classical derivative on the slit plane, away from the origin and negative real axis. Constant powers use the polynomial rule instead of an unused logarithm, including at zero when the exponent permits a derivative there.

theorem Runtime.Autograd.Model.Dual.jet_log_comp_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (directions : Fin n → E) {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ (↑n) f x) (hzero : f x ≠ 0) : jet directions (fun (y : E) => Real.log (f y)) x = MathFunctions.log (jet directions f x)

The runtime logarithm preserves mixed derivatives at nonzero inputs. This uses mathlib's real logarithm, which is smooth for negative as well as positive inputs.

theorem Runtime.Autograd.Model.Dual.jet_log {n : ℕ} (directions : Fin n → ℝ) {x : ℝ} (hx : x ≠ 0) : jet directions Real.log x = MathFunctions.log (Nested.seed directions x)

Direct scalar logarithm evaluation on seeded inputs away from zero.

theorem Runtime.Autograd.Model.Dual.jet_one_div {n : ℕ} (directions : Fin n → ℝ) {x : ℝ} (hx : x ≠ 0) : jet directions (fun (y : ℝ) => 1 / y) x = 1 / Nested.seed directions x

Direct reciprocal evaluation on seeded inputs away from zero.

theorem Runtime.Autograd.Model.Dual.jet_sqrt_comp_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (directions : Fin n → E) {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ (↑n) f x) (hzero : f x ≠ 0) : jet directions (fun (y : E) => √(f y)) x = MathFunctions.sqrt (jet directions f x)

The runtime square root preserves mixed derivatives at nonzero inputs. For negative exact-real inputs, both the runtime and mathlib use the locally constant zero branch. No derivative claim at zero or about native floating-point square roots is made.

theorem Runtime.Autograd.Model.Dual.jet_sqrt {n : ℕ} (directions : Fin n → ℝ) {x : ℝ} (hx : x ≠ 0) : jet directions Real.sqrt x = MathFunctions.sqrt (Nested.seed directions x)

Direct square-root evaluation on seeded inputs away from zero.

theorem Runtime.Autograd.Model.Dual.hasDerivAt_pow_const {f : ℝ → ℝ} {df point exponent : ℝ} (hf : HasDerivAt f df point) (h : exponent = 0 ∨ f point ≠ 0 ∨ 1 ≤ exponent) : HasDerivAt (fun (t : ℝ) => f t ^ exponent) ({ re := f point, du := df } ^ { re := exponent, du := 0 }).du point

The actual constant-exponent dual rule agrees with mathlib's real-power derivative.

At zero, the exponent must be zero or at least one. Positive integer powers therefore include zero and negative inputs without passing through a logarithm. This concerns exact-real coefficients; it does not assert an error bound for floating-point powers.

theorem Runtime.Autograd.Model.Dual.hasDerivAt_pow {f g : ℝ → ℝ} {df dg point : ℝ} (hf : HasDerivAt f df point) (hg : HasDerivAt g dg point) (h : 0 < f point) : HasDerivAt (fun (t : ℝ) => f t ^ g t) ({ re := f point, du := df } ^ { re := g point, du := dg }).du point

The actual dual power rule differentiates a positive base and a varying exponent together.

Both input curves may vary. Positivity is the domain of the logarithmic formula; the selected constant-exponent branch agrees with the same derivative when the exponent direction is zero. This is an exact-real statement, not a rounding theorem for a floating-point implementation.

theorem Runtime.Autograd.Model.Dual.hasDerivAt_atan2 {f g : ℝ → ℝ} {df dg point : ℝ} (hf : HasDerivAt f df point) (hg : HasDerivAt g dg point) (h : { re := g point, im := f point } ∈ Complex.slitPlane) : HasDerivAt (fun (t : ℝ) => Atan2.atan2 (f t) (g t)) (Atan2.atan2 { re := f point, du := df } { re := g point, du := dg }).du point

The actual dual angle rule differentiates two real curves away from the branch cut.

The slit-plane hypothesis excludes the origin and negative real axis. This is an exact-real result, not an accuracy theorem for floating-point execution.