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 IEEE32Exec), we provide a small parametric complex scalar:

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

The provided Context instance is designed to be:

• good enough for TorchLean’s tensor/model surface (arithmetic + common transcendental functions),
• runtime-friendly when α is runtime-friendly, and
• conservative for the few operations that are fundamentally about angles/branches (log, sqrt): we pick a simple real-part-based approximation that is exact on real inputs (imag part 0).

This is not meant to be a full replacement for complex analysis; for deep analytic theorems, use mathlib’s ℂ directly.

structure TorchLean.Complex (α : Type) : Type

Parametric complex numbers a + i·b over a scalar type α.

• re : α

  Real part.

• im : α

  Imaginary part.

@[implicit_reducible]

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

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

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

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

@[simp]

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

@[simp]

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

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

Imaginary unit i.

@[simp]

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

@[simp]

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

Basic algebraic structure

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

Complex multiplication.

Division uses the standard formula (a+bi)/(c+di) = ((ac+bd) + i(bc-ad)) / (c^2 + d^2).

@[implicit_reducible]

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

@[implicit_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 keeps the instance lightweight and avoids polluting mathlib’s ℂ with ad-hoc orderings.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

Numeric literals and constants

@[implicit_reducible]

instance TorchLean.Complex.instCoeNatOfContext {α : Type} [Context α] : Coe ℕ (Complex α)

@[implicit_reducible]

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

Transcendentals

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

Squared magnitude re^2 + im^2 (helper for abs/log).

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

Real magnitude sqrt(normSq z).

@[implicit_reducible]

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

max/min and Context

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

Lift a scalar Context to TorchLean complex scalars.