Tensor Initialization

Deterministic tensor initialization helpers (Xavier/Kaiming, etc.) that return TorchLean TorchLean.Tensors with shape tracked in the type.

Tensor Initialization Helpers

This module exposes Runtime.Autograd.Torch.Init through TorchLean TorchLean.Tensors with shapes tracked in the type.

All initializers are deterministic given an explicit seed : Nat, which is convenient for:

• reproducible examples
• stable tests
• proofs that want to fix concrete initial values

PyTorch Mapping

The names mirror common PyTorch initializers:

• Xavier/Glorot: torch.nn.init.xavier_uniform_, torch.nn.init.xavier_normal_
• Kaiming/He: torch.nn.init.kaiming_uniform_, torch.nn.init.kaiming_normal_

See the PyTorch init docs: https://pytorch.org/docs/stable/nn.init.html

def TorchLean.Init.tensor {α : Type} [Storage α] [Runtime.FromFloat α] {shape : Shape} (scheme : Scheme) (seed : ℕ := 0) : Tensor α shape

Initialize a tensor under any executable arithmetic.

The element type and dimensions are normally inferred from the expected tensor type. Initialization is generated once in Float, then converted through the element type's canonical Runtime.FromFloat instance.

def TorchLean.Init.xavierUniform {α : Type} [Storage α] [Runtime.FromFloat α] {outputWidth inputWidth : ℕ} (seed : ℕ := 0) : Tensor α [outputWidth, inputWidth]

Xavier/Glorot uniform initialization for a linear weight matrix.

Both widths are inferred from the expected Tensor α [outputWidth, inputWidth] type.

def TorchLean.Init.kaimingUniform {α : Type} [Storage α] [Runtime.FromFloat α] {outputWidth inputWidth : ℕ} (seed : ℕ := 0) : Tensor α [outputWidth, inputWidth]

Kaiming/He uniform initialization for a linear weight matrix used before a ReLU.

Both widths are inferred from the expected Tensor α [outputWidth, inputWidth] type.