Lean module · Probability layer
BanditRLProof.ConditionalRewardFoundation
This module closes the canonical COND-EXPECT-REWARD route for reward-only trajMeasure processes. A centered reward-kernel law and deterministic historywise proxy ceilings yield, on the generated history filtration:
Module map
Imports
BanditRLProof.ConditionalRewardLawSource
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_centeredReward_succ_condExp_eq_zero_trajMeasure_of_condSubgaussian
Compiled
Canonical successor conditional mean-zero with no caller integrability premise. The canonical conditional MGF theorem supplies exponential integrability, and `HasCondSubgaussianMGF.integrable` lowers it to the ordinary integrability needed by `condExp`.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_centeredReward_succ_condExp_eq_zero_trajMeasure_of_condSubgaussianReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem historyStepKernelFamily_centeredReward_succ_condExp_eq_zero_trajMeasure_of_condSubgaussian {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (defaultAction : Action) (i : Nat) (c : NNReal) (hvariance : forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= c) : let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) mu0 stepKernel let reward : RewardTrace Rat -> RewardTrace Rat := fun trajectory => trajectory let hreward : forall t : Nat, Measurable (fun trajectory : RewardTrace Rat => reward trajectory t)
theorem
BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_conditionalRewardFoundation_trajMeasure
Compiled
The canonical conditional reward foundation as one theorem-facing endpoint. For every successor time it exposes both conditional mean zero and the conditional MGF witness. The same assumptions also yield the finite-sum Azuma-Hoeffding upper tail for the zero-initialized centered process. Thus `Finset.range n` contains the deterministic slot `Y 0 = 0` and successor rewards `Y 1, ..., Y (n - 1)`. When the cumulative proxy is zero, Lean's totalized division makes the displayed exponential bound equal to `1`; this endpoint does not claim a sharper degenerate-variance bound.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_conditionalRewardFoundation_trajMeasureReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem historyStepKernelFamily_conditionalRewardFoundation_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (defaultAction : Action) (varianceCeiling : Nat -> NNReal) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= varianceCeiling i) : let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) mu0 stepKernel let reward : RewardTrace Rat -> RewardTrace Rat := fun trajectory => trajectory let hreward : forall t : Nat, Measurable (fun trajectory : RewardTrace Rat => reward trajectory t)