DQN Minibatch Helpers

NN.Runtime.RL.Algorithms.ValueLearning contains the scalar DQN/Double-DQN targets. This module adds the missing batch-facing layer used by replay-buffer training loops:

• evaluate one transition with caller-provided online/target Q-functions;
• average DQN or Double-DQN losses as a tensor over a replay minibatch;
• update target-network parameters by a weighted average.

The functions are intentionally higher-order: TorchLean examples can pass typed-graph/eager model closures without this module knowing anything about parameters, optimizers, or autograd sessions.

References:

• Mnih et al., "Human-level control through deep reinforcement learning" (2015): https://doi.org/10.1038/nature14236
• van Hasselt, Guez, and Silver, "Deep Reinforcement Learning with Double Q-learning" (2016): https://arxiv.org/abs/1509.06461
• Polyak and Juditsky, "Acceleration of Stochastic Approximation by Averaging" (1992), background for moving-average target-network updates.

def Runtime.RL.DQN.loss {α : Type} [TorchLean.Storage α] [Context α] {obsShape : Spec.Shape} {nActions : ℕ} {Input : Type} (onlineQ targetQ : TorchLean.Tensor α obsShape → TorchLean.Tensor α [nActions]) (gamma : α) (input : Input) (batch double : Bool := false) (error : α → α → α := Core.squaredError) [TorchLean.Internal.BatchInput (Core.Transition α obsShape nActions) (Array (Core.Transition α obsShape nActions)) batch Input] : α

DQN loss for one transition, or the mean loss of a replay batch (batch := true).

double := true selects actions with the online network and evaluates them with the target network. error defaults to squared error; pass a scalar loss such as Core.huberLoss to change it. Batch reduction uses Tensor.mean, including its empty-batch convention.

def Runtime.RL.DQN.updateTarget {α : Type u_1} [One α] [Add α] [Sub α] [Mul α] (tau online target : α) : α

Weighted target-network update:

target ← τ * online + (1 - τ) * target.

Use this elementwise over parameter tensors for DQN/DDPG/TD3/SAC target synchronization. The mixing weight is used as supplied, without validation. The arithmetic order is retained for floating-point callers; algebraically equivalent rearrangements can round differently.