TorchLean API

NN.Proofs.Autograd.FDeriv.TensorCoordinates

Coordinate derivatives on real tensors #

The tensor representation already carries its Euclidean norm. Reading its coordinates is a continuous linear equivalence with a finite function space, so coordinatewise derivative proofs give Fréchet derivatives on the tensor itself. In particular, a matrix proof can keep its row and column indices instead of introducing a second flattened layout.

The coordinate function space is only used to assemble the derivative. The result has the native tensor type and the Euclidean topology used by the tensor inner-product and adjoint theorems.

The native coordinate view, with continuity supplied by finite dimensionality.

Instances For
    @[simp]

    Reading the coordinate view performs the same lookup as the tensor representation.

    @[simp]

    Rebuilding a tensor preserves each supplied coordinate.

    A single tensor coordinate is a continuous linear functional.

    Instances For
      @[simp]

      The coordinate functional uses the native lookup.

      Local smoothness of a tensor is equivalent to local smoothness of every coordinate.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_coordinate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {f : ETorchLean.Tensor shape} {x : E} (hf : ContDiffAt n f x) (i : shape.Coord) :
      ContDiffAt n (fun (y : E) => TorchLean.Tensor.Internal.Rep.get (f y) i) x

      Reading a fixed coordinate preserves local smoothness.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {g : } {f : ETorchLean.Tensor shape} {x : E} (hg : ∀ (i : TorchLean.Tensor.Internal.Coord shape), ContDiffAt n g (TorchLean.Tensor.Internal.Rep.get (f x) i)) (hf : ContDiffAt n f x) :
      ContDiffAt n (fun (y : E) => TorchLean.Tensor.map g (f y)) x

      An elementwise map needs smoothness only at the current coordinate values.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_ofFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {f : Eshape.Coord} {x : E} (hf : ∀ (i : shape.Coord), ContDiffAt n (fun (y : E) => f y i) x) :

      Locally smooth coordinate families assemble into a locally smooth native tensor.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_map2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {op : } {f g : ETorchLean.Tensor shape} {x : E} (hop : ∀ (i : TorchLean.Tensor.Internal.Coord shape), ContDiffAt n (fun (p : × ) => op p.1 p.2) (TorchLean.Tensor.Internal.Rep.get (f x) i, TorchLean.Tensor.Internal.Rep.get (g x) i)) (hf : ContDiffAt n f x) (hg : ContDiffAt n g x) :
      ContDiffAt n (fun (y : E) => TorchLean.Tensor.map2Spec op (f y) (g y)) x

      A binary elementwise map needs smoothness only at each current pair of coordinates.

      Tensor smoothness is equivalent to smoothness of its finitely many coordinates.

      Reading a fixed tensor coordinate preserves the differentiability order.

      theorem Proofs.Autograd.TensorCoordinates.contDiff_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {g : } {f : ETorchLean.Tensor shape} (hg : ContDiff n g) (hf : ContDiff n f) :
      ContDiff n fun (x : E) => TorchLean.Tensor.map g (f x)

      Mapping a smooth scalar function over a smooth tensor preserves its differentiability order.

      theorem Proofs.Autograd.TensorCoordinates.contDiff_ofFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {f : Eshape.Coord} (hf : ∀ (i : shape.Coord), ContDiff n fun (x : E) => f x i) :

      Smooth coordinate families assemble into a smooth native tensor.

      Reading a packed storage index preserves local smoothness.

      Packed row-major lookups are the same continuous coordinate functionals.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_sumSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {f : ETorchLean.Tensor shape} {x : E} (hf : ContDiffAt n f x) :
      ContDiffAt n (fun (y : E) => (f y).sumSpec) x

      Summation preserves local smoothness, including for empty tensors.

      theorem Proofs.Autograd.TensorCoordinates.contDiff_sumSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {f : ETorchLean.Tensor shape} (hf : ContDiff n f) :
      ContDiff n fun (x : E) => (f x).sumSpec

      Summing the packed tensor preserves smoothness, including when it has no entries.

      theorem Proofs.Autograd.TensorCoordinates.contDiff_map2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {op : } {f g : ETorchLean.Tensor shape} (hop : ContDiff n fun (p : × ) => op p.1 p.2) (hf : ContDiff n f) (hg : ContDiff n g) :
      ContDiff n fun (x : E) => TorchLean.Tensor.map2Spec op (f x) (g x)

      Applying a smooth binary scalar function to two tensors preserves their smoothness.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_dotSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {f g : ETorchLean.Tensor shape} {x : E} (hf : ContDiffAt n f x) (hg : ContDiffAt n g x) :
      ContDiffAt n (fun (y : E) => (f y).dotSpec (g y)) x

      Dot products preserve local smoothness in both tensor arguments.

      theorem Proofs.Autograd.TensorCoordinates.contDiff_dotSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} {n : WithTop ℕ∞} {f g : ETorchLean.Tensor shape} (hf : ContDiff n f) (hg : ContDiff n g) :
      ContDiff n fun (x : E) => (f x).dotSpec (g x)

      Dot products of two smooth tensor families are smooth.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_matMulSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {n : WithTop ℕ∞} {rows inner cols : } {f : ETorchLean.Tensor [rows, inner]} {g : ETorchLean.Tensor [inner, cols]} {x : E} (hf : ContDiffAt n f x) (hg : ContDiffAt n g x) :
      ContDiffAt n (fun (y : E) => Spec.matMulSpec (f y) (g y)) x

      Matrix multiplication needs smoothness of its inputs only near the evaluation point.

      theorem Proofs.Autograd.TensorCoordinates.contDiff_matMulSpec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {n : WithTop ℕ∞} {rows inner cols : } {f : ETorchLean.Tensor [rows, inner]} {g : ETorchLean.Tensor [inner, cols]} (hf : ContDiff n f) (hg : ContDiff n g) :
      ContDiff n fun (x : E) => Spec.matMulSpec (f x) (g x)

      Matrix multiplication preserves smoothness when both operands vary.

      theorem Proofs.Autograd.TensorCoordinates.contDiffAt_pull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {source target : Spec.Shape} {n : WithTop ℕ∞} (index : target.Coordsource.Coord) {f : ETorchLean.Tensor source} {x : E} (hf : ContDiffAt n f x) :
      ContDiffAt n (fun (y : E) => TorchLean.Tensor.Internal.Rep.pull index (f y)) x

      Fixed coordinate reads preserve local smoothness, including repeated reads and empty outputs.

      theorem Proofs.Autograd.TensorCoordinates.contDiff_pull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {source target : Spec.Shape} {n : WithTop ℕ∞} (index : target.Coordsource.Coord) {f : ETorchLean.Tensor source} (hf : ContDiff n f) :
      ContDiff n fun (x : E) => TorchLean.Tensor.Internal.Rep.pull index (f x)

      Fixed coordinate reads preserve smoothness, including repeated reads and empty outputs.

      noncomputable def Proofs.Autograd.TensorCoordinates.assemble {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} (derivatives : shape.CoordE →L[] ) :

      Assemble one scalar derivative for each output coordinate into a tensor derivative.

      Instances For
        @[simp]
        theorem Proofs.Autograd.TensorCoordinates.assemble_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} (derivatives : shape.CoordE →L[] ) (dx : E) (i : shape.Coord) :
        TorchLean.Tensor.Internal.Rep.get ((assemble derivatives) dx) i = (derivatives i) dx

        Each coordinate of the assembled tangent is given by its supplied scalar derivative.

        theorem Proofs.Autograd.TensorCoordinates.hasFDerivAt_of_coordinates {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {shape : Spec.Shape} (f : ETorchLean.Tensor shape) (derivatives : shape.CoordE →L[] ) (x : E) (h : ∀ (i : TorchLean.Tensor.Internal.Coord shape), HasFDerivAt (fun (y : E) => TorchLean.Tensor.Internal.Rep.get (f y) i) (derivatives i) x) :
        HasFDerivAt f (assemble derivatives) x

        Scalar coordinate derivatives determine the full tensor Fréchet derivative.

        Finiteness of the shape matters here: assembling the coordinates is a continuous linear map. The hypotheses therefore imply a Fréchet derivative in the tensor norm, not just separate directional derivatives of its entries.