BanditRLProof.RL.FiniteHorizonStochasticRewardBellmanInnovationConcentration

A symmetric interval with NNReal radius has variance proxy equal to its square.

theorem intervalVarianceProxy_neg_coe (bound : NNReal) : intervalVarianceProxy (-(bound : Real)) (bound : Real) = bound ^ 2

Hoeffding proxy for the mean Bellman return with `remaining` decisions.

noncomputable def meanBellmanInnovationStepVarianceProxy (rewardBound : NNReal) (remaining : Nat) : NNReal

Sum of the stage-dependent mean Bellman innovation proxies.

noncomputable def meanBellmanInnovationVarianceProxy (rewardBound : NNReal) (remaining : Nat) : NNReal

No declaration docstring is present; use the chapter context and exact statement below.

theorem meanBellmanInnovationVarianceProxy_zero (rewardBound : NNReal) : meanBellmanInnovationVarianceProxy rewardBound 0 = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem meanBellmanInnovationVarianceProxy_succ (rewardBound : NNReal) (remaining : Nat) : meanBellmanInnovationVarianceProxy rewardBound (remaining + 1) = meanBellmanInnovationStepVarianceProxy rewardBound (remaining + 1) + meanBellmanInnovationVarianceProxy rewardBound remaining

No declaration docstring is present; use the chapter context and exact statement below.

theorem meanBellmanInnovationVarianceProxy_pos {rewardBound : NNReal} {remaining : Nat} (hrewardBound : 0 < rewardBound) (hremaining : 0 < remaining) : 0 < meanBellmanInnovationVarianceProxy rewardBound remaining

Every bounded-mean-reward policy value lies in its remaining reward envelope.

theorem valueRemaining_abs_le_of_rewardBound {mdp : MDP State Action} (policy : MarkovPolicy mdp) (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (remaining : Nat) (hremaining : remaining ≤ mdp.horizon) (state : State) : |policy.valueRemaining remaining hremaining state| ≤ (remaining : Real) * (rewardBound : Real)

Sum of policy-action and transition innovations in the mean Bellman return.

noncomputable def sampledCumulativeMeanBellmanInnovationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) : (remaining : Nat) → remaining ≤ mdp.horizon → State → RewardStepTrace Action State remaining → Real | 0, _, _, _ => 0 | remaining + 1, hremaining, state, trace => (mdp.reward state (trace 0).1 + policy.valueRemaining remaining (by omega) (trace 0).2.2 - policy.valueRemaining (remaining + 1) hremaining state) + sampledCumulativeMeanBellmanInnovationFrom mdp policy remaining (by omega) (trace 0).2.2 (Fin.tail trace) /-- The recursive mean Bellman innovation is jointly measurable in start state and trace. -/ theorem measurable_sampledCumulativeMeanBellmanInnovationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining ≤ mdp.horizon) : Measurable (fun p : State × RewardStepTrace Action State remaining => mdp.sampledCumulativeMeanBellmanInnovationFrom policy remaining hremaining p.1 p.2)

The recursive mean Bellman innovation is jointly measurable in start state and trace.

theorem measurable_sampledCumulativeMeanBellmanInnovationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining ≤ mdp.horizon) : Measurable (fun p : State × RewardStepTrace Action State remaining => mdp.sampledCumulativeMeanBellmanInnovationFrom policy remaining hremaining p.1 p.2)

Dropping the sampled reward recovers the ordinary action/next-state kernel.

theorem actionRewardStateKernel_map_dropReward (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : (source.actionRewardStateKernel policy stage).map (fun head : Action × (Real × State) => (head.1, head.2.2)) = policy.actionStateKernel stage

The one-step mean Bellman return integrates to the recursive policy value.

theorem integral_meanBellmanReturn_actionStateKernel_eq_valueRemaining (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 ≤ mdp.horizon) (state : State) : ∫ head : Action × State, (mdp.reward state head.1 + policy.valueRemaining remaining (by omega) head.2) ∂ policy.actionStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ state = policy.valueRemaining (remaining + 1) hremaining state

A one-step mean Bellman innovation is sub-Gaussian at its stage envelope.

theorem actionStateKernel_meanBellmanInnovation_hasSubgaussianMGF (policy : MarkovPolicy mdp) (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (remaining : Nat) (hremaining : remaining + 1 ≤ mdp.horizon) (state : State) : ProbabilityTheory.HasSubgaussianMGF (fun head : Action × State => mdp.reward state head.1 + policy.valueRemaining remaining (by omega) head.2 - policy.valueRemaining (remaining + 1) hremaining state) (meanBellmanInnovationStepVarianceProxy rewardBound (remaining + 1)) (policy.actionStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ state)

The reward-bearing head has the same mean Bellman innovation MGF.

theorem actionRewardStateKernel_meanBellmanInnovation_hasSubgaussianMGF (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (remaining : Nat) (hremaining : remaining + 1 ≤ mdp.horizon) (state : State) : ProbabilityTheory.HasSubgaussianMGF (fun head : Action × (Real × State) => mdp.reward state head.1 + policy.valueRemaining remaining (by omega) head.2.2 - policy.valueRemaining (remaining + 1) hremaining state) (meanBellmanInnovationStepVarianceProxy rewardBound (remaining + 1)) (source.actionRewardStateKernel policy ⟨mdp.horizon - (remaining + 1), by omega⟩ state)

The cumulative mean Bellman innovation has the sum of its stage proxies.

theorem stochasticTrajectoryKernelRemaining_sampledCumulativeMeanBellmanInnovationFrom_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (remaining : Nat) (hremaining : remaining ≤ mdp.horizon) (state : State) : ProbabilityTheory.HasSubgaussianMGF (mdp.sampledCumulativeMeanBellmanInnovationFrom policy remaining hremaining state) (meanBellmanInnovationVarianceProxy rewardBound remaining) (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state)

Fixed-horizon two-sided tail for the cumulative mean Bellman innovation.

theorem stochasticTrajectoryKernelRemaining_sampledCumulativeMeanBellmanInnovationFrom_abs_tail_le [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (remaining : Nat) (hremaining : remaining ≤ mdp.horizon) (state : State) (htotal : 0 < ((meanBellmanInnovationVarianceProxy rewardBound remaining : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) : (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state) {trace | Concentration.subGaussianSumConfidenceRadius (meanBellmanInnovationVarianceProxy rewardBound remaining) delta ≤ |mdp.sampledCumulativeMeanBellmanInnovationFrom policy remaining hremaining state trace|} ≤ ENNReal.ofReal delta