Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonNaturalCausalBehaviorExpectedRegretLogRate
# Explicit logarithmic natural-causal cumulative behavior regret 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`. The inverse-square budget telescopes after comparison with `1 / ((t + 1) * (t + 2))`, and the high-power budget is bounded by that square budget. Mathlib's `harmonic_le_one_add_log` controls the remaining shifted harmonic sum. The resulting expected cumulative regret is bounded by an explicit coefficient times `1 + log rounds`; dividing by `rounds` gives an explicit average envelope tending to zero through `Real.isLittleO_log_id_atTop`. Regularity: the scalar sum and asymptotic lemmas are unconditional. The same-source regret consumers retain finite nonempty Standard Borel State/Action, a probability initial law, positive horizon/base floor/reward proxy, bounded deterministic 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 both integrated model-confidence shares. This is an explicit expected cumulative and average rate, not realized-return control, an anytime/pathwise theorem, state reachability, a minimax-optimal rate, or complete UCB-VI.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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)