TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.Tensor.Euclidean

Real tensors as Euclidean space #

A real tensor of shape s is a finite family of reals indexed by s.Coord. This file transports the Euclidean inner-product structure of EuclideanSpace ℝ s.Coord along the coordinate view, so that Tensor ℝ s is a NormedAddCommGroup and an InnerProductSpace ℝ with

All Mathlib facts about inner product spaces (Cauchy-Schwarz, the triangle inequality, norm_smul, LipschitzWith, finite dimensionality) then apply to real tensors directly. The metric topology this induces is the one every analytic statement about real tensors should use; continuous_vectorEquiv shows the rank-one coordinate view is a homeomorphism for it.

The instances are stated on the native representation Internal.Rep ℝ s (with s : List Nat) rather than on Tensor ℝ shape: the public type is a reducible abbreviation whose shape argument unfolds to a dimension list, so only representation-level instances are found for literal shapes such as Tensor ℝ [n].

source
noncomputable def TorchLean.Tensor.toEuclidean (s : Internal.Shape) :
Internal.Rep ℝ s ≃ₗ[ℝ] EuclideanSpace ℝ (Internal.Coord s)

The coordinate view of a real tensor as a point of Euclidean space.

Instances For
    source
    @[simp]
    theorem TorchLean.Tensor.toEuclidean_apply {s : Internal.Shape} (x : Internal.Rep ℝ s) (i : Internal.Coord s) :
    ((toEuclidean s) x).ofLp i = x.get i

    Coordinates of the Euclidean view are the tensor's coordinates.

    source
    @[simp]
    theorem TorchLean.Tensor.toEuclidean_symm_apply {s : Internal.Shape} (v : EuclideanSpace ℝ (Internal.Coord s)) (i : Internal.Coord s) :
    ((toEuclidean s).symm v).get i = v.ofLp i

    Coordinates of a tensor rebuilt from Euclidean space are the point's coordinates.

    source
    @[instance_reducible]
    noncomputable instance TorchLean.Tensor.instNormedAddCommGroupRepReal {s : Internal.Shape} :
    NormedAddCommGroup (Internal.Rep ℝ s)

    The Euclidean norm on real tensors.

    source
    @[instance_reducible]
    noncomputable instance TorchLean.Tensor.instInnerProductSpaceRealRep {s : Internal.Shape} :
    InnerProductSpace ℝ (Internal.Rep ℝ s)

    The Euclidean inner product on real tensors.

    source
    instance TorchLean.Tensor.instFiniteDimensionalRealRep {s : Internal.Shape} :
    FiniteDimensional ℝ (Internal.Rep ℝ s)

    Real tensors of a fixed shape form a finite-dimensional real vector space.

    source
    theorem TorchLean.Tensor.norm_eq_norm_toEuclidean {s : Internal.Shape} (x : Internal.Rep ℝ s) :
    ‖x‖ = ‖(toEuclidean s) x‖

    The tensor norm is the norm of its Euclidean view.

    source
    theorem TorchLean.Tensor.inner_eq_inner_toEuclidean {s : Internal.Shape} (x y : Internal.Rep ℝ s) :
    inner ℝ x y = inner ℝ ((toEuclidean s) x) ((toEuclidean s) y)

    The tensor inner product is the inner product of the Euclidean views.

    source
    theorem TorchLean.Tensor.inner_eq_sum {s : Internal.Shape} (x y : Internal.Rep ℝ s) :
    inner ℝ x y = ∑ i : Internal.Coord s, x.get i * y.get i

    The inner product of two real tensors is the sum of coordinatewise products.

    source
    theorem TorchLean.Tensor.norm_eq_sqrt_sum {s : Internal.Shape} (x : Internal.Rep ℝ s) :
    ‖x‖ = √(∑ i : Internal.Coord s, x.get i ^ 2)

    The norm of a real tensor is the square root of its sum of squares.

    source
    theorem TorchLean.Tensor.norm_sq_eq_sum {s : Internal.Shape} (x : Internal.Rep ℝ s) :
    ‖x‖ ^ 2 = ∑ i : Internal.Coord s, x.get i ^ 2

    The squared norm of a real tensor is its sum of squares.

    source
    theorem TorchLean.Tensor.abs_apply_le_norm {s : Internal.Shape} (x : Internal.Rep ℝ s) (i : Internal.Coord s) :
    |x.get i| ≤ ‖x‖

    Every coordinate of a real tensor is bounded by the Euclidean norm.

    source
    theorem TorchLean.Tensor.dist_eq_sqrt_sum {s : Internal.Shape} (x y : Internal.Rep ℝ s) :
    dist x y = √(∑ i : Internal.Coord s, (x.get i - y.get i) ^ 2)

    The distance between real tensors is the square root of the summed squared differences.

    source
    noncomputable def TorchLean.Tensor.vectorLinearEquiv (n : ℕ) :
    Tensor ℝ [n] ≃ₗ[ℝ] Fin n → ℝ

    The rank-one coordinate view as a real linear equivalence.

    Instances For
      source
      theorem TorchLean.Tensor.continuous_vectorEquiv (n : ℕ) :
      Continuous ⇑(vectorEquiv n)

      The rank-one coordinate view is continuous for the Euclidean topology.

      source
      theorem TorchLean.Tensor.continuous_vectorEquiv_symm (n : ℕ) :
      Continuous ⇑(vectorEquiv n).symm

      Rebuilding a rank-one tensor from its coordinates is continuous.