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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretInMeasureExplicitSchedule

# Explicit polynomial-prefix absolute consistency in measure This module upgrades the one-sided scheduled certificate to Mathlib `TendstoInMeasure` for the same equal-round-weighted natural realized behavior-regret process. Outside the compiled model-tail/return event, the parent route supplies the upper bound. The exact expected-minus-deviation identity, expected-regret nonnegativity, and the return-event complement supply the missing lower bound. The process differs from the existing mass-weighted `realizedSuccessorAverageRegret` process. The result is only for the explicit fourth-power prefix subsequence; it is not all-prefix, anytime, almost-sure, or L1 convergence.

Module map

Declarations
11
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretUpperTailInProbability

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretL1Consistency

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess Compiled

The equal-round-weighted natural realized-regret process on the explicit schedule.

noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Real
Source line 36 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet Compiled

Fixed-threshold distance-from-zero violation for the scheduled process.

noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (n : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))
Source line 52 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability Compiled

Trajectory probability of the scheduled distance violation.

noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (n : Nat) : ENNReal
Source line 71 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess Compiled

Every scheduled coordinate of the equal-round-weighted process is measurable.

theorem measurable_explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Measurable (explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)
Source line 87 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet Compiled

Every fixed-threshold scheduled distance violation is measurable.

theorem measurableSet_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (n : Nat) : MeasurableSet (explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n)
Source line 104 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess_neg_averageReturnRadius_lt_of_not_mem_event Compiled

Every fixed-threshold scheduled distance violation is measurable. -/ theorem measurableSet_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (n : Nat) : MeasurableSet (explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n) := by unfold explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet exact measurableSet_le measurable_const (Measurable.dist (measurable_explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) measurable_const) /- Outside the scheduled union event, the return deviation is strictly smaller than its confidence radius. Nonnegative behavior expected regret therefore gives the missing lower side after division by the positive scheduled prefix.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess_neg_averageReturnRadius_lt_of_not_mem_event (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) (htrajectory : trajectory ∉ explicitPolynomialPrefixTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) : -explicitPolynomialPrefixAverageReturnRadius mdp varianceProxy baseVisitFloor n < explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n trajectory
Source line 130 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_explicitPolynomialPrefixTailModelReturnBadEvent_le Compiled

Direct projection of the scheduled parent-event probability bound.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_explicitPolynomialPrefixTailModelReturnBadEvent_le (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) (n : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (explicitPolynomialPrefixTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n
Source line 207 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet_subset_event Compiled

Eventually every fixed positive distance violation lies in the parent event.

theorem eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet_subset_event (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) (epsilon : Real) (hepsilon : 0 < epsilon) : ∀ᶠ n in atTop, explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n ⊆ explicitPolynomialPrefixTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n
Source line 239 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_le_failureBudget Compiled

Eventually every fixed distance probability is bounded by the exact budget.

theorem eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_le_failureBudget (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) (epsilon : Real) (hepsilon : 0 < epsilon) : ∀ᶠ n in atTop, explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n
Source line 306 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_tendsto_zero Compiled

The scheduled distance-violation probability vanishes at every positive threshold.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_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) (epsilon : Real) (hepsilon : 0 < epsilon) : Tendsto (explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon) atTop (nhds 0)
Source line 342 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegret_tendstoInMeasure_zero Compiled

The scheduled distance-violation probability vanishes at every positive threshold. -/ theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_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) (epsilon : Real) (hepsilon : 0 < epsilon) : Tendsto (explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon) atTop (nhds 0) := by exact tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (explicitPolynomialPrefixTailModelReturnFailureBudget_tendsto_zero mdp) (Eventually.of_forall fun _ => bot_le) (eventually_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_le_failureBudget mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor epsilon hepsilon) /- Terminal route: the equal-round-weighted natural realized behavior regret on the explicit fourth-power prefixes converges absolutely in measure to zero.

theorem selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegret_tendstoInMeasure_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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let process := explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall n, Measurable (process n)) /\ (forall epsilon, 0 < epsilon -> (forall n, MeasurableSet (explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n)) /\ (∀ᶠ n in atTop, explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n ⊆ explicitPolynomialPrefixTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n /\ explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n) /\ Tendsto (explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon) atTop (nhds 0)) /\ TendstoInMeasure source.trajectoryMeasure process atTop (fun _ => 0)
Source line 375 Chapter context: Finite-horizon RL