Higher derivatives of tensor-valued functions

Tensor coordinates are continuous linear functionals, so they commute with every derivative order. This lets the scalar dual-number rules certify tensor computations in the existing Euclidean tensor norm, with no restriction on tensor rank or differentiation directions.

noncomputable def Runtime.Autograd.Model.DualTensor.jet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) (f : E → TorchLean.Tensor ℝ shape) (x : E) : TorchLean.Tensor (Dual.Nested ℝ n) shape

All mixed derivative coefficients of a tensor-valued function along a direction tuple.

@[simp]

theorem Runtime.Autograd.Model.DualTensor.jet_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) (f : E → TorchLean.Tensor ℝ shape) (x : E) (i : shape.Coord) : TorchLean.Tensor.Internal.Rep.get (jet directions f x) i = Dual.jet directions (fun (y : E) => TorchLean.Tensor.Internal.Rep.get (f y) i) x

Each tensor coordinate carries the corresponding scalar jet.

theorem Runtime.Autograd.Model.DualTensor.jet_linear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) (f : E →L[ℝ] TorchLean.Tensor ℝ shape) (x : E) : jet directions (⇑f) x = Dual.Nested.seedTensor (fun (k : Fin n) => f (directions k)) (f x)

A continuous linear tensor map carries each direction through unchanged by higher terms.

theorem Runtime.Autograd.Model.DualTensor.jet_id {shape : Spec.Shape} {n : ℕ} (directions : Fin n → TorchLean.Tensor ℝ shape) (input : TorchLean.Tensor ℝ shape) : jet directions (fun (x : TorchLean.Tensor ℝ shape) => x) input = Dual.Nested.seedTensor directions input

Runtime seeding is the complete jet of the tensor input, including zero mixed coefficients.

theorem Runtime.Autograd.Model.DualTensor.jet_coordinate {shape : Spec.Shape} {n : ℕ} (directions : Fin n → TorchLean.Tensor ℝ shape) (input : TorchLean.Tensor ℝ shape) (i : shape.Coord) : Dual.jet directions (fun (x : TorchLean.Tensor ℝ shape) => TorchLean.Tensor.Internal.Rep.get x i) input = Dual.Nested.seed (fun (k : Fin n) => TorchLean.Tensor.Internal.Rep.get (directions k) i) (TorchLean.Tensor.Internal.Rep.get input i)

A tensor input coordinate has precisely the value and directions supplied to the runtime.

theorem Runtime.Autograd.Model.DualTensor.jet_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) (value : TorchLean.Tensor ℝ shape) (x : E) : jet directions (fun (x : E) => value) x = TorchLean.Tensor.map (Dual.Nested.ofPrimal n) value

A tensor held constant has zero derivative coefficients in every direction.

theorem Runtime.Autograd.Model.DualTensor.jet_mul_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f g : E → TorchLean.Tensor ℝ shape} {x : E} (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g x) : jet directions (fun (y : E) => (f y).mulSpec (g y)) x = (jet directions f x).mulSpec (jet directions g x)

Pointwise multiplication of complete jets follows the scalar product rule at every order.

theorem Runtime.Autograd.Model.DualTensor.jet_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f g : E → TorchLean.Tensor ℝ shape} (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) (x : E) : jet directions (fun (y : E) => (f y).mulSpec (g y)) x = (jet directions f x).mulSpec (jet directions g x)

Pointwise multiplication of complete jets follows the scalar product rule at every order.

theorem Runtime.Autograd.Model.DualTensor.jet_getFlat {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) (f : E → TorchLean.Tensor ℝ shape) (x : E) (i : Fin (TorchLean.Tensor.Internal.Shape.size shape)) : TorchLean.Tensor.Internal.Rep.getFlat (jet directions f x) i = Dual.jet directions (fun (y : E) => TorchLean.Tensor.Internal.Rep.getFlat (f y) i) x

Flat storage indices read the same coefficients as tensor coordinates.

theorem Runtime.Autograd.Model.DualTensor.jet_sumSpec_comp_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f : E → TorchLean.Tensor ℝ shape} {x : E} (hf : ContDiffAt ℝ (↑n) f x) : Dual.jet directions (fun (y : E) => (f y).sumSpec) x = (jet directions f x).sumSpec

The runtime sum preserves every derivative coefficient, including for an empty tensor.

theorem Runtime.Autograd.Model.DualTensor.jet_sumSpec_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f : E → TorchLean.Tensor ℝ shape} (hf : ContDiff ℝ (↑n) f) (x : E) : Dual.jet directions (fun (y : E) => (f y).sumSpec) x = (jet directions f x).sumSpec

The runtime sum preserves every derivative coefficient, including for an empty tensor.

theorem Runtime.Autograd.Model.DualTensor.jet_sumSpec {shape : Spec.Shape} {n : ℕ} (directions : Fin n → TorchLean.Tensor ℝ shape) (x : TorchLean.Tensor ℝ shape) : Dual.jet directions (fun (y : TorchLean.Tensor ℝ shape) => y.sumSpec) x = (Dual.Nested.seedTensor directions x).sumSpec

Summing a seeded tensor computes the complete jet of the sum function.

theorem Runtime.Autograd.Model.DualTensor.jet_dotSpec_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f g : E → TorchLean.Tensor ℝ shape} {x : E} (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g x) : Dual.jet directions (fun (y : E) => (f y).dotSpec (g y)) x = (jet directions f x).dotSpec (jet directions g x)

Dot products preserve jets when both operands depend on the input.

theorem Runtime.Autograd.Model.DualTensor.jet_dotSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f g : E → TorchLean.Tensor ℝ shape} (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) (x : E) : Dual.jet directions (fun (y : E) => (f y).dotSpec (g y)) x = (jet directions f x).dotSpec (jet directions g x)

Dot products preserve jets when both operands depend on the input.

theorem Runtime.Autograd.Model.DualTensor.jet_matMulSpec_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n rows inner cols : ℕ} (directions : Fin n → E) {f : E → TorchLean.Tensor ℝ [rows, inner]} {g : E → TorchLean.Tensor ℝ [inner, cols]} {x : E} (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g x) : jet directions (fun (y : E) => Spec.matMulSpec (f y) (g y)) x = Spec.matMulSpec (jet directions f x) (jet directions g x)

Matrix contraction propagates all mixed derivatives of both operands. The shared dimension can be empty; no positivity or nonzero-entry assumptions are needed.

theorem Runtime.Autograd.Model.DualTensor.jet_matMulSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n rows inner cols : ℕ} (directions : Fin n → E) {f : E → TorchLean.Tensor ℝ [rows, inner]} {g : E → TorchLean.Tensor ℝ [inner, cols]} (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) (x : E) : jet directions (fun (y : E) => Spec.matMulSpec (f y) (g y)) x = Spec.matMulSpec (jet directions f x) (jet directions g x)

Matrix contraction propagates all mixed derivatives of both operands. The shared dimension can be empty; no positivity or nonzero-entry assumptions are needed.

theorem Runtime.Autograd.Model.DualTensor.tangent_jet_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f : E → TorchLean.Tensor ℝ shape} {x : E} (hf : ContDiffAt ℝ (↑n) f x) : Dual.Nested.tangentTensor (jet directions f x) = (iteratedFDeriv ℝ n f x) directions

Local smoothness suffices to identify the extracted tensor with its iterated derivative.

theorem Runtime.Autograd.Model.DualTensor.tangent_jet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → E) {f : E → TorchLean.Tensor ℝ shape} (hf : ContDiff ℝ (↑n) f) (x : E) : Dual.Nested.tangentTensor (jet directions f x) = (iteratedFDeriv ℝ n f x) directions

Extracting every tangent gives the tensor's iterated Fréchet derivative, not merely separate coordinate derivatives.