BanditRLProof.RewardTraceLaw

The zeroth coordinate of an Ionescu-Tulcea trajectory has the supplied initial law. This is a project-level wrapper over `trajMeasure`, `traj_map_frestrictLe`, and `partialTraj_self`. It is general enough to be tracked as a Mathlib candidate.

theorem trajMeasure_map_eval_zero {X : Nat -> Type*} [forall n, MeasurableSpace (X n)] (mu0 : Measure (X 0)) [IsProbabilityMeasure mu0] (kernel : (n : Nat) -> ProbabilityTheory.Kernel ((i : Finset.Iic n) -> X i) (X (n + 1))) [forall n, ProbabilityTheory.IsMarkovKernel (kernel n)] : Measure.map (fun trajectory : ((n : Nat) -> X n) => trajectory 0) (ProbabilityTheory.Kernel.trajMeasure mu0 kernel) = mu0

Finite reward-prefix law uniqueness from the initial marginal and successor conditional distributions. Only the conditional laws before `n` are required. The proof turns each conditional-distribution identity into a joint prefix/next-reward law with `condDistrib_ae_eq_iff_measure_eq_compProd`, then matches the corresponding Ionescu-Tulcea recurrence.

theorem rewardTrace_prefix_map_eq_trajMeasure_of_condDistrib {Omega Reward : Type*} [MeasurableSpace Omega] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (mu0 : Measure Reward) [IsProbabilityMeasure mu0] (reward : Omega -> RewardTrace Reward) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (kernel : (n : Nat) -> ProbabilityTheory.Kernel ((i : Finset.Iic n) -> Reward) Reward) [forall n, ProbabilityTheory.IsMarkovKernel (kernel n)] (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = mu0) (n : Nat) (hcond : forall i : Nat, i < n -> ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i) mu =ᵐ[ mu.map (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)] kernel i) : Measure.map (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) n) mu = Measure.map (fun trajectory : RewardTrace Reward => History.finiteRewardHistoryOfTrace trajectory n) (ProbabilityTheory.Kernel.trajMeasure (X

The complete trace law is uniquely determined by its initial marginal and all successor conditional distributions. The finite-prefix theorem above handles every `Finset.Iic n`. Any finite set of time coordinates embeds measurably into one such prefix, so the external law and the Ionescu-Tulcea law have the same finite-dimensional marginals. Mathlib's projective-limit uniqueness then identifies the full measures.

theorem rewardTrace_map_eq_trajMeasure_of_condDistrib {Omega Reward : Type*} [MeasurableSpace Omega] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (mu0 : Measure Reward) [IsProbabilityMeasure mu0] (reward : Omega -> RewardTrace Reward) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (kernel : (n : Nat) -> ProbabilityTheory.Kernel ((i : Finset.Iic n) -> Reward) Reward) [forall n, ProbabilityTheory.IsMarkovKernel (kernel n)] (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = mu0) (hcond : forall i : Nat, ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i) mu =ᵐ[mu.map (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)] kernel i) : Measure.map reward mu = ProbabilityTheory.Kernel.trajMeasure (X

Two complete traces are identically distributed when they share an initial marginal and the same successor conditional-distribution kernels.

theorem identDistrib_rewardTrace_of_common_condDistrib {Omega Xi Reward : Type*} [MeasurableSpace Omega] [MeasurableSpace Xi] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (mu' : Measure Xi) [IsFiniteMeasure mu'] (mu0 : Measure Reward) [IsProbabilityMeasure mu0] (reward : Omega -> RewardTrace Reward) (reward' : Xi -> RewardTrace Reward) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hreward' : forall t : Nat, Measurable (fun xi : Xi => reward' xi t)) (kernel : (n : Nat) -> ProbabilityTheory.Kernel ((i : Finset.Iic n) -> Reward) Reward) [forall n, ProbabilityTheory.IsMarkovKernel (kernel n)] (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = mu0) (hzero' : Measure.map (fun xi : Xi => reward' xi 0) mu' = mu0) (hcond : forall i : Nat, ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i) mu =ᵐ[mu.map (fun omega : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)] kernel i) (hcond' : forall i : Nat, ProbabilityTheory.condDistrib (fun xi : Xi => reward' xi (i + 1)) (fun xi : Xi => History.finiteRewardHistoryOfTrace (reward' xi) i) mu' =ᵐ[mu'.map (fun xi : Xi => History.finiteRewardHistoryOfTrace (reward' xi) i)] kernel i) : ProbabilityTheory.IdentDistrib reward reward' mu mu'