Lean module · Probability layer
BanditRLProof.KernelTrajectoryPrefix
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.Algorithms.StochasticGradientBanditTheoremTwoNativeTrajectory, 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`.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.KernelTrajectoryPrefix.partialTraj_zero_congrReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.KernelTrajectoryPrefix.trajMeasure_map_frestrictLe_congrReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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)