Rounded scalar NN ops (ℝ + neural_round)

We collect small building blocks: common scalar functions used in neural networks, defined in the “rounding-on-ℝ” style.

The pattern is always:

1. define the intended real-valued expression (e.g. max x 0 for ReLU),
2. round it back to the target grid using neural_round.

This is the same modeling choice as NF: we treat each primitive as a real computation followed by a rounding step.

If you need an error bound for any of these ops under round-to-nearest, you can usually get it directly from the generic lemma neural_error_bound_ulp applied to the exact real expression.

@[inline]

noncomputable def TorchLean.Floats.NNOps.round1 {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (g : ℝ → ℝ) (x : ℝ) : ℝ

Round the result of a real-valued scalar function.

This is the basic adapter used throughout this file.

@[inline]

noncomputable def TorchLean.Floats.NNOps.round2 {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (g : ℝ → ℝ → ℝ) (x y : ℝ) : ℝ

Round the result of a two-argument real-valued function.

This is handy for “activation-like” helpers that take a parameter (e.g. leaky ReLU slope).

noncomputable def TorchLean.Floats.NNOps.neuralRelu {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : ℝ

ReLU (rounded).

Mathematically, ReLU is relu(x) = max(x, 0). Here we evaluate that in ℝ and then round.

This is close in spirit to what happens in practice: even if a framework fuses ops, the overall effect is still “some real expression, then it gets rounded to the destination format”.

noncomputable def TorchLean.Floats.NNOps.neuralLeakyRelu {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (negative_slope x : ℝ) : ℝ

Leaky ReLU (rounded).

Definition (PyTorch torch.nn.functional.leaky_relu):

• if x > 0 then x
• else negative_slope * x.

noncomputable def TorchLean.Floats.NNOps.neuralSigmoid {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : ℝ

Sigmoid (rounded), with the usual stable piecewise definition.

We define the exact real function as:

• if x ≥ 0, use 1 / (1 + exp(-x))
• else use exp(x) / (1 + exp(x))

The two branches are algebraically equal, but the piecewise form avoids overflow in exp.

noncomputable def TorchLean.Floats.NNOps.neuralTanh {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : ℝ

tanh (rounded).

This is just “evaluate Real.tanh then round”. Any round-to-nearest error bound is inherited from neural_error_bound_ulp applied at Real.tanh x.

noncomputable def TorchLean.Floats.NNOps.neuralSilu {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : ℝ

SiLU / Swish (rounded).

PyTorch analogies: torch.nn.functional.silu / torch.nn.SiLU.

Definition: silu(x) = x * sigmoid(x). We use the same stable sigmoid expression as neural_sigmoid, then round the final result.

noncomputable def TorchLean.Floats.NNOps.neuralSoftplus {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : ℝ

Softplus (rounded), with a stable piecewise definition.

PyTorch analogy: torch.nn.functional.softplus.

Naively, softplus(x) = log(1 + exp(x)). The piecewise form avoids catastrophic overflow in exp(x) when x is large and positive:

• if x > 0, use x + log(1 + exp(-x))
• else use log(1 + exp(x)).