BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Probability layer

BanditRLProof.ConditionalRewardFoundation

# Canonical conditional reward foundation 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: conditional expectation zero for every successor centered reward; a conditional sub-Gaussian MGF witness at the selected proxy ceiling; the finite-sum Azuma-Hoeffding upper tail.

Module map

Declarations
2
Placeholders
0

Imports

BanditRLProof.ConditionalRewardLawSource

Imported by

BanditRLProof

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`.

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
Source line 28 Chapter context: Probability layer
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.

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
Source line 139 Chapter context: Probability layer