Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonEpisodeBatchStandardBorel

# Standard Borel instances for finite-horizon episode batches `EpisodeStep` uses an explicit product-coordinate `MeasurableSpace.comap`, so the generic product instance is not visible to typeclass search. This module transports a Polish topology through the coordinate equivalence and then installs the corresponding Standard Borel instance. The deterministic and stochastic infinite batch trajectories are countable products of their finite batch spaces. The episode-step instance needs only measurable Standard Borel state and action spaces. The stochastic batch-trajectory wrapper additionally inherits finite state and action spaces from the finite-horizon aliases. These instances close a regularity boundary only. They do not supply any probability law, independence, support, concentration, or regret property.