Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonEpisodeBatchStandardBorel
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.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveEpisodeBatchLaw, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardTotalReturnConcentration
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationRegularityClosedConsistency, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentSchedule
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.EpisodeStep.toProdEquiv
Compiled
Product coordinates underlying the measurable structure on `EpisodeStep`.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.EpisodeStep.toProdEquivReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def toProdEquiv : EpisodeStep State Action ≃ State × Action × Real × State where