Lean module · Probability layer
BanditRLProof.KernelTrajectoryPrefix
# Finite-prefix congruence for Ionescu-Tulcea trajectories The infinite `Kernel.traj` construction has a finite marginal determined only by the initial law and the step kernels used before the marginal endpoint. These wrappers expose that fact in the form needed by environment-prefix factorizations.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalSource, BanditRLProof.TsallisScheduledIIDMeanGap
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.KernelTrajectoryPrefix.partialTraj_zero_congr
Compiled
Two partial trajectories from time zero agree through `n` when their step kernels agree strictly before `n`.
theorem partialTraj_zero_congr {X : Nat -> Type u} [forall n, MeasurableSpace (X n)] (kappa eta : (n : Nat) -> Kernel ((i : Finset.Iic n) -> X i) (X (n + 1))) [forall n, IsMarkovKernel (kappa n)] [forall n, IsMarkovKernel (eta n)] (n : Nat) (hstep : forall k, k < n -> kappa k = eta k) : Kernel.partialTraj kappa 0 n = Kernel.partialTraj eta 0 n
theorem
BanditRLProof.KernelTrajectoryPrefix.trajMeasure_map_frestrictLe_congr
Compiled
The finite marginal of an Ionescu-Tulcea trajectory depends only on its initial measure and the step kernels strictly before the endpoint.
theorem trajMeasure_map_frestrictLe_congr {X : Nat -> Type u} [forall n, MeasurableSpace (X n)] (mu0 nu0 : Measure (X 0)) [IsProbabilityMeasure mu0] [IsProbabilityMeasure nu0] (kappa eta : (n : Nat) -> Kernel ((i : Finset.Iic n) -> X i) (X (n + 1))) [forall n, IsMarkovKernel (kappa n)] [forall n, IsMarkovKernel (eta n)] (n : Nat) (hinitial : mu0 = nu0) (hstep : forall k, k < n -> kappa k = eta k) : (Kernel.trajMeasure mu0 kappa).map (Preorder.frestrictLe n) = (Kernel.trajMeasure nu0 eta).map (Preorder.frestrictLe n)