Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretExplicitIntegratedRate
# Natural-causal behavior expected-regret explicit integrated rate This module turns the actual exploratory `source.successorPolicyAt` pointwise planning certificate into a finite-coordinate expectation bound on the same genuine heterogeneous dependent causal trajectory measure. A generic event split integrates a local bound off one measurable bad event and a global bound on it. For the natural causal source, the local term is the compiled planning rate, the global term is `2 * horizon`, and the event has the compiled two-share coordinate model-confidence budget. The resulting envelope is explicit: the model-event fallback is `4 * horizon * selfConsistentScheduledLocalDelta mdp t`, and a closed-form theorem expands both this confidence term and the existing planning rate. The envelope tends to zero, yielding a quantitative squeeze proof of expected- absolute behavior-regret convergence without using the realized-return MGF. Regularity: the generic integral lemma needs a probability measure, a measurable bad event, integrability, and pointwise local/global bounds. The causal consumer retains finite nonempty Standard Borel State/Action, probability initial law, positive horizon/base floor/reward proxy, bounded means, uniform mean-compatible selected-reward sub-Gaussianity, and path support. Failure policy preserves the actual exploratory policy, one dependent source, actual samples, `n`-prefix to `n+1` selection, scheduled budgets, initial exclusion, and behavior/recommendation separation. This is a per-coordinate integrated rate, not cumulative/average regret, anytime, reachability, minimax/optimal rate, or complete UCB-VI.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretFinitePrefixCumulativeAverageRate
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.integral_le_add_const_mul_measureReal_of_le_on_compl
Compiled
Integrate a local bound off one bad event and a global bound on it.
theorem integral_le_add_const_mul_measureReal_of_le_on_compl {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (f : Omega -> Real) (bad : Set Omega) (hbad : MeasurableSet bad) (hf : Integrable f mu) (rate envelope : Real) (hrate : 0 <= rate) (hglobal : forall omega, f omega <= envelope) (hgood : forall omega, omega ∉ bad -> f omega <= rate) : integral mu f <= rate + envelope * (mu bad).toReal
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalPlanningRateAt_nonneg
Compiled
The named causal planning envelope is pointwise nonnegative.
theorem selfConsistentScheduledCausalPlanningRateAt_nonneg (mdp : MDP State Action) (t : Nat) : 0 <= selfConsistentScheduledCausalPlanningRateAt mdp t
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalCoordinateModelFailureBudget_toReal_eq
Compiled
The two coordinate model-confidence shares have real mass `2 * delta_t`.
theorem selfConsistentScheduledCausalCoordinateModelFailureBudget_toReal_eq (mdp : MDP State Action) (t : Nat) : (selfConsistentScheduledCausalCoordinateModelFailureBudget mdp t).toReal = 2 * AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp t
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt
Compiled
Planning rate plus the one-event `2H` expectation fallback.
noncomputable def selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt (mdp : MDP State Action) (t : Nat) : Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_eq
Compiled
Closed form of the finite-coordinate integrated behavior envelope.
theorem selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_eq (mdp : MDP State Action) (t : Nat) : selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp t = (mdp.horizon : Real) * (2 * (1 / (AdaptiveEpisodeBatchSource.decayingExplorationScale t : Real) ^ 2 + (12 * (Fintype.card State : Real) * (mdp.horizon : Real)) / (AdaptiveEpisodeBatchSource.decayingExplorationScale t : Real) ^ 2)) + exploratoryBehaviorRegretCharge mdp (AdaptiveEpisodeBatchSource.decayingExplorationRate (t + 1)) 1 + (4 * (mdp.horizon : Real)) / (((t + 2 : Nat) : Real) ^ (mdp.horizon + 5))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_nonneg
Compiled
The explicit integrated behavior envelope is nonnegative.
theorem selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_nonneg (mdp : MDP State Action) (t : Nat) : 0 <= selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp t
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret_le_rateAt
Compiled
Expected absolute behavior regret obeys the explicit finite-coordinate rate.
theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret_le_rateAt (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) (t : Nat) : selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t <= selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp t
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_tendsto_zero
Compiled
The explicit integrated behavior envelope vanishes.
theorem selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp) atTop (nhds 0)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret_tendsto_zero_of_explicit_rate
Compiled
Quantitative squeeze proof of expected-absolute convergence.
theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret_tendsto_zero_of_explicit_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) : Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_behaviorExpectedRegret_explicitIntegratedRate
Compiled
The finite-coordinate rate, its limit, and the induced expectation limit.
theorem selfConsistentScheduledCausalSource_behaviorExpectedRegret_explicitIntegratedRate (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) : (forall t, selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t <= selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp t) /\ Tendsto (selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp) atTop (nhds 0) /\ Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)