Higher derivatives on local domains

Division, 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 proof follows the runtime implementation, including its floating-point safeguards. Over exact reals, the checks for non-finite intermediate values are always false; no floating-point execution is identified with exact-real arithmetic here.

theorem Runtime.Autograd.Model.Dual.jet_beq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (ds : Fin n → E) (f : E → ℝ) (x : E) : (jet ds f x == 0) = (f x == 0)

Runtime comparisons inspect the primal value, not its derivative coefficients.

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

The runtime quotient rule preserves every derivative coefficient away from a zero denominator. Both functions need be smooth only near the evaluation point.

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_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (ds : Fin n → E) (f : E → ℝ) (x : E) : 0 < jet ds f x ↔ 0 < f x

The square-root branch depends only on the primal input.

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.