Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonNaturalCausalBehaviorExpectedRegretLogRate
This module closes the symbolic finite-prefix envelope for the actual source.successorPolicyAt behavior on the one genuine heterogeneous dependent causal trajectory measure. The expanded coordinate rate has an inverse-square term, the scheduled exploration harmonic term, and a confidence term with exponent mdp.horizon + 5.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalBehaviorExpectedRegretHighProbabilityLogRate
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.sum_range_one_div_natCast_add_two_sq_le_one
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.sum_range_one_div_natCast_add_two_sq_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_range_one_div_natCast_add_two_sq_le_one (rounds : Nat) : (Finset.range rounds).sum (fun t => 1 / (((t + 2 : Nat) : Real) ^ 2)) <= 1
theorem
BanditRLProof.sum_range_one_div_natCast_add_two_pow_le_one
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.sum_range_one_div_natCast_add_two_pow_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_range_one_div_natCast_add_two_pow_le_one (rounds exponent : Nat) (hexponent : 2 <= exponent) : (Finset.range rounds).sum (fun t => 1 / (((t + 2 : Nat) : Real) ^ exponent)) <= 1
theorem
BanditRLProof.sum_range_one_div_natCast_add_three_le_one_add_log
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.sum_range_one_div_natCast_add_three_le_one_add_logReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_range_one_div_natCast_add_three_le_one_add_log (rounds : Nat) : (Finset.range rounds).sum (fun t => 1 / (((t + 3 : Nat) : Real))) <= 1 + Real.log (rounds : Real)
theorem
BanditRLProof.one_le_one_add_log_natCast
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.one_le_one_add_log_natCastReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem one_le_one_add_log_natCast (rounds : Nat) : (1 : Real) <= 1 + Real.log (rounds : Real)
theorem
BanditRLProof.tendsto_one_add_log_natCast_div_natCast_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.tendsto_one_add_log_natCast_div_natCast_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem tendsto_one_add_log_natCast_div_natCast_zero : Filter.Tendsto (fun rounds : Nat => (1 + Real.log (rounds : Real)) / (rounds : Real)) Filter.atTop (nhds 0)
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSquareRateCoefficient
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSquareRateCoefficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfConsistentScheduledNaturalCausalInverseSquareRateCoefficient (mdp : MDP State Action) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficient
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficient (mdp : MDP State Action) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalHighPowerRateCoefficient
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalHighPowerRateCoefficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfConsistentScheduledNaturalCausalHighPowerRateCoefficient (mdp : MDP State Action) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicRateCoefficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient (mdp : MDP State Action) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate (mdp : MDP State Action) (rounds : Nat) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate (mdp : MDP State Action) (rounds : Nat) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate (mdp : MDP State Action) (rounds : Nat) : Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_eq_threeTerm
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_eq_threeTermReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt_eq_threeTerm (mdp : MDP State Action) (t : Nat) : selfConsistentScheduledNaturalCausalIntegratedBehaviorExpectedRegretRateAt mdp t = selfConsistentScheduledNaturalCausalInverseSquareRateCoefficient mdp * (1 / (((t + 2 : Nat) : Real) ^ 2)) + selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficient mdp * (1 / (((t + 3 : Nat) : Real))) + selfConsistentScheduledNaturalCausalHighPowerRateCoefficient mdp * (1 / (((t + 2 : Nat) : Real) ^ (mdp.horizon + 5)))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSquareRateCoefficient_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSquareRateCoefficient_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalInverseSquareRateCoefficient_nonneg (mdp : MDP State Action) : 0 <= selfConsistentScheduledNaturalCausalInverseSquareRateCoefficient mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficient_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficient_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficient_nonneg (mdp : MDP State Action) : 0 <= selfConsistentScheduledNaturalCausalExplorationHarmonicRateCoefficient mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalHighPowerRateCoefficient_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalHighPowerRateCoefficient_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalHighPowerRateCoefficient_nonneg (mdp : MDP State Action) : 0 <= selfConsistentScheduledNaturalCausalHighPowerRateCoefficient mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient_nonneg (mdp : MDP State Action) : 0 <= selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_le_refined
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_le_refinedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_le_refined (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds <= selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate_le_logarithmic
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate_le_logarithmicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate_le_logarithmic (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_le_logarithmic
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_le_logarithmicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate_le_logarithmic (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate_nonneg (mdp : MDP State Action) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_nonneg (mdp : MDP State Action) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate mdp rounds
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_tendsto_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_tendsto_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate mdp) atTop (nhds 0)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate_isBigO
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate_isBigOReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate_isBigO (mdp : MDP State Action) : (selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp) =O[atTop] (fun rounds : Nat => 1 + Real.log (rounds : Real))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_le_logarithmic
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_le_logarithmicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_le_logarithmic (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 <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_isBigO_one_add_log
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_isBigO_one_add_logReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret_isBigO_one_add_log (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) : (selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) =O[atTop] (fun rounds : Nat => 1 + Real.log (rounds : Real))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_le_logarithmic
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_le_logarithmicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_le_logarithmic (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 <= selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate mdp rounds
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_isBigO_log_div_natCast
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_isBigO_log_div_natCastReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_isBigO_log_div_natCast (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) : (selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) =O[atTop] (fun rounds : Nat => (1 + Real.log (rounds : Real)) / (rounds : Real))
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_tendsto_zero_of_logarithmicRate
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_tendsto_zero_of_logarithmicRateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret_tendsto_zero_of_logarithmicRate (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)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_cumulative_and_averageBehaviorExpectedRegret_explicitLogarithmicRate
Compiled
Same-source explicit logarithmic cumulative and `log(n) / n` average route.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_cumulative_and_averageBehaviorExpectedRegret_explicitLogarithmicRateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledCausalSource_cumulative_and_averageBehaviorExpectedRegret_explicitLogarithmicRate (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 rounds, selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds <= selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds /\ selfConsistentScheduledNaturalCausalRefinedCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds) /\ (forall rounds, selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds) /\ (forall rounds, selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate mdp rounds) /\ (selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp) =O[atTop] (fun rounds : Nat => 1 + Real.log (rounds : Real)) /\ (selfConsistentScheduledNaturalCausalExpectedCumulativeBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) =O[atTop] (fun rounds : Nat => 1 + Real.log (rounds : Real)) /\ (selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) =O[atTop] (fun rounds : Nat => (1 + Real.log (rounds : Real)) / (rounds : Real)) /\ Tendsto (selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate mdp) atTop (nhds 0) /\ Tendsto (selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)