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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretFinitePrefixCumulativeAverageRate

# Natural-causal finite-prefix cumulative and average behavior regret This module sums the actual `source.successorPolicyAt` expected-regret process over `Finset.range rounds` on the one genuine heterogeneous dependent causal trajectory measure. `ExpectationBochnerSums.integral_finset_sum` identifies the integral of that pathwise finite sum with the sum of coordinate expectations; coordinate nonnegativity then identifies those terms with the compiled expected absolute regrets. Summing the explicit integrated coordinate bounds gives a finite-prefix cumulative rate, and division by `rounds` gives its Cesaro rate. The existing `tendsto_natWeightedAverage_zero` theorem at unit natural weights proves that this deterministic average rate tends to zero, so a nonnegative squeeze yields average behavior expected-regret consistency. Regularity for the finite-sum identity is only the probability initial law and the deterministic reward bound needed by coordinate integrability. The rate consumer retains finite nonempty Standard Borel State/Action, a probability initial law, positive horizon/base floor/reward proxy, bounded means, uniform mean-compatible selected-reward sub-Gaussianity, and exploratory path support. Failure policy: preserve the actual exploratory behavior rather than the recommended policy, the same dependent source and sampled batches, natural coordinate `t` selecting successor batch `t + 1`, scheduled budgets, initial batch exclusion, and the two model-confidence shares already integrated by the parent. This route proves a finite-prefix cumulative bound and a vanishing Cesaro average. It does not provide a closed sublinear cumulative rate, realized-return control, every-trajectory or anytime guarantees, reachability, minimax/optimal rates, or complete UCB-VI.

Module map

Declarations
17
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretExplicitIntegratedRate, BanditRLProof.ExpectationBochnerSums

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalBehaviorExpectedRegretLogRate

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess Compiled

Natural-prefix cumulative expected regret of the actual successor behavior.

noncomputable def selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat)
Source line 51 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret Compiled

Expectation of the natural-prefix cumulative behavior regret.

noncomputable def selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real
Source line 65 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate Compiled

Finite-prefix sum of the explicit integrated coordinate rates.

noncomputable def selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate (mdp : MDP State Action) (rounds : Nat) : Real
Source line 80 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret Compiled

Natural-prefix average behavior expected regret.

noncomputable def selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real
Source line 87 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate Compiled

Cesaro average of the explicit integrated coordinate rates.

noncomputable def selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate (mdp : MDP State Action) (rounds : Nat) : Real
Source line 100 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_nonneg Compiled

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

theorem selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (trajectory) : 0 <= selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory
Source line 106 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess Compiled

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

theorem integrable_selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (rounds : Nat) : Integrable (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 123 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_eq_sum_expectedAbsolute Compiled

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

theorem selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_eq_sum_expectedAbsolute (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (rounds : Nat) : selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds = (Finset.range rounds).sum fun t => selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t
Source line 144 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_nonneg Compiled

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

theorem selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds
Source line 178 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_nonneg Compiled

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

theorem selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_nonneg (mdp : MDP State Action) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds
Source line 197 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_le_rate Compiled

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

theorem selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_le_rate (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (rounds : Nat) : selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds
Source line 206 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_le_rate Compiled

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

theorem selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_le_rate (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (rounds : Nat) : selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate mdp rounds
Source line 236 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate_eq_natWeightedAverage Compiled

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

theorem selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate_eq_natWeightedAverage (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate mdp rounds = natWeightedAverage (fun _ => 1) (selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp) rounds
Source line 268 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate_tendsto_zero Compiled

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

theorem selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate mdp) atTop (nhds 0)
Source line 282 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_nonneg Compiled

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

theorem selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds
Source line 300 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_tendsto_zero Compiled

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

theorem selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 317 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_cumulative_and_averageBehaviorExpectedRegret_explicitRate Compiled

Same-source finite-prefix cumulative and Cesaro-average behavior-regret route.

theorem selfConsistentScheduledCausalSource_cumulative_and_averageBehaviorExpectedRegret_explicitRate (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, Integrable (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) source.trajectoryMeasure) /\ (forall rounds, selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds = (Finset.range rounds).sum fun t => selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) /\ (forall rounds, selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds) /\ (forall rounds, selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate mdp rounds) /\ Tendsto (selfConsistentScheduledNaturalCausalAverageIntegratedBehaviorExpectedRegretRate mdp) atTop (nhds 0) /\ Tendsto (selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 350 Chapter context: Finite-horizon RL