Complex scalar (TorchLean.Complex α)

TorchLean is scalar-polymorphic, and some model components (e.g. FFT/FNO-style blocks) want a complex-valued scalar type.

Mathlib’s ℂ is specialized to ℝ and intentionally has no order instance; TorchLean’s generic Context includes order-like operations (LT/LE, max/min) for ReLU/argmax-style code paths.

To avoid changing mathlib’s global behavior (and to support runtime-friendly backends like ExecFloat.Binary 8 23), we provide a small parametric complex scalar:

TorchLean.Complex α := α × α with fields re and im.

Complex square roots use the principal branch. Complex logarithms retain the polar angle through Atan2 α; a backend must supply that real-coordinate operation to obtain the complex Context. Arithmetic operations inherit the rounding and exceptional-value behavior of the component type.

The Context instance supports explicit complex programs. For real-valued losses, the application API autograd.complex.grad differentiates both real coordinates by forward-mode seeding; its gradients work with nn.sgdStep, and Checkpoint.State preserves both components. The ordinary supervised trainer still has a real-valued data and result boundary. Complex-linear reverse rules must not be substituted for real-coordinate differentiation of a nonholomorphic loss.

structure TorchLean.Complex (α : Type) : Type

Parametric complex numbers $a+ib$ over a scalar type α.

• re : α

  Real part.

• im : α

  Imaginary part.

def TorchLean.instReprComplex.repr {α✝ : Type} [Repr α✝] : Complex α✝ → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.instReprComplex {α✝ : Type} [Repr α✝] : Repr (Complex α✝)

def TorchLean.Complex.ofReal {α : Type} [Zero α] (a : α) : Complex α

Embed a real scalar as a complex scalar with zero imaginary part.

def TorchLean.Complex.conj {α : Type} [Neg α] (z : Complex α) : Complex α

Complex conjugation keeps the real coordinate and negates the imaginary coordinate.

def TorchLean.Complex.normSq {α : Type} [Mul α] [Add α] (z : Complex α) : α

Squared magnitude, returned in the real component type.

@[simp]

theorem TorchLean.Complex.re_ofReal {α : Type} [Zero α] (a : α) : (ofReal a).re = a

The real part of a real embedded as a complex number is itself.

@[simp]

theorem TorchLean.Complex.im_ofReal {α : Type} [Zero α] (a : α) : (ofReal a).im = 0

A real embedded as a complex number has zero imaginary part.

def TorchLean.Complex.I {α : Type} [Zero α] [One α] : Complex α

Imaginary unit i.

@[simp]

theorem TorchLean.Complex.re_I {α : Type} [Zero α] [One α] : I.re = 0

i has zero real part.

@[simp]

theorem TorchLean.Complex.im_I {α : Type} [Zero α] [One α] : I.im = 1

i has imaginary part one.

Basic algebraic structure

@[instance_reducible]

instance TorchLean.Complex.instInhabitedOfZero {α : Type} [Inhabited α] [Zero α] : Inhabited (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instZero {α : Type} [Zero α] : Zero (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instOneOfZero {α : Type} [One α] [Zero α] : One (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instNeg {α : Type} [Neg α] : Neg (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instAdd {α : Type} [Add α] : Add (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instSub {α : Type} [Sub α] : Sub (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instMulOfAddOfSub {α : Type} [Mul α] [Add α] [Sub α] : Mul (Complex α)

Complex multiplication using the usual real/imaginary component formula.

Division uses the standard formula $$ \frac{a+bi}{c+di}=\frac{(ac+bd)+i(bc-ad)}{c^2+d^2}. $$

@[instance_reducible]

instance TorchLean.Complex.instDivOfMulOfAddOfSub {α : Type} [Mul α] [Add α] [Sub α] [Div α] : Div (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instBEq {α : Type} [BEq α] : BEq (Complex α)

Order is only used in TorchLean for branchy ops like ReLU/max/min. Complex numbers do not have a canonical order, so we pick a simple real-part order: compare re and ignore im.

This instance is local to TorchLean’s branchy tensor operations and does not change mathlib’s ℂ.

@[instance_reducible]

instance TorchLean.Complex.instLT {α : Type} [LT α] : LT (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instLE {α : Type} [LE α] : LE (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instToString {α : Type} [ToString α] : ToString (Complex α)

Numeric literals and constants

@[instance_reducible]

instance TorchLean.Complex.instNatCastOfContext {α : Type} [Context α] : NatCast (Complex α)

Transcendentals

def TorchLean.Complex.Internal.absReal {α : Type} [Context α] (z : Complex α) : α

Real magnitude evaluated with scaling to avoid unnecessary overflow from squaring.

This is mathematically sqrt(re² + im²) for real coordinates; floating-point evaluation can differ in the last bits from the unscaled expression. No IEEE complex special-value contract is asserted.

@[instance_reducible]

instance TorchLean.Complex.instMathFunctionsOfContextOfAtan2 {α : Type} [Context α] [Atan2 α] : MathFunctions (Complex α)

max/min and Context

@[instance_reducible]

instance TorchLean.Complex.instMaxOfContext {α : Type} [Context α] : Max (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instMinOfContext {α : Type} [Context α] : Min (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instPowOfContextOfAtan2 {α : Type} [Context α] [Atan2 α] : Pow (Complex α) (Complex α)

@[instance_reducible]

instance TorchLean.Complex.instContextOfAtan2 {α : Type} [Context α] [Atan2 α] : Context (Complex α)

Lift a scalar Context to TorchLean complex scalars.