BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalExplicitRate

A finite average with positive natural-number weights.

noncomputable def natWeightedAverage (weight : Nat -> Nat) (value : Nat -> Real) (rounds : Nat) : Real

Positive natural weights preserve a zero limit under finite weighted averaging.

theorem tendsto_natWeightedAverage_zero (weight : Nat -> Nat) (hweight : forall t, 0 < weight t) (value : Nat -> Real) (hvalue : Tendsto value atTop (nhds 0)) : Tendsto (natWeightedAverage weight value) atTop (nhds 0)

The successor episode mass is the corresponding range sum.

theorem successorEpisodeMass_eq_sum_range (episodes : Nat -> Nat) (rounds : Nat) : successorEpisodeMass episodes rounds = (Finset.range rounds).sum (fun t => (episodes (t + 1) : Real))

Positive coordinate batch sizes make successor mass diverge.

theorem successorEpisodeMass_tendsto_atTop (episodes : Nat -> Nat) (hepisodes : forall t, 0 < episodes t) : Tendsto (successorEpisodeMass episodes) atTop atTop

The heterogeneous global return proxy is exactly linear in successor mass.

theorem cumulativeSuccessorGlobalReturnVarianceProxy_coe (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : ((cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real) = successorEpisodeMass episodes rounds * (mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy : Real)

Globally centered successor-return radius divided by actual successor mass.

noncomputable def normalizedSuccessorGlobalReturnConfidenceRadius (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) : Real

Exact square-root formula for the heterogeneous normalized return radius.

theorem normalizedSuccessorGlobalReturnConfidenceRadius_eq (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) (hmass : 0 < successorEpisodeMass episodes rounds) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes rounds rewardBound rewardVarianceProxy delta = Real.sqrt (2 * (mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy : Real) * Real.log (2 / delta) / successorEpisodeMass episodes rounds)

Fixed-half return envelope on the actual heterogeneous successor mass.

noncomputable def fixedHalfSuccessorGlobalReturnRateEnvelope (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : Real

At confidence share one half, the normalized radius is the fixed-half envelope.

theorem normalizedSuccessorGlobalReturnConfidenceRadius_half_eq (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hmass : 0 < successorEpisodeMass episodes rounds) : normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes rounds rewardBound rewardVarianceProxy (1 / 2) = fixedHalfSuccessorGlobalReturnRateEnvelope mdp episodes rounds rewardBound rewardVarianceProxy

The fixed-half heterogeneous return envelope vanishes with prefix length.

theorem fixedHalfSuccessorGlobalReturnRateEnvelope_tendsto_zero (mdp : MDP State Action) (episodes : Nat -> Nat) (hepisodes : forall t, 0 < episodes t) (rewardBound rewardVarianceProxy : NNReal) : Tendsto (fun rounds => fixedHalfSuccessorGlobalReturnRateEnvelope mdp episodes rounds rewardBound rewardVarianceProxy) atTop (nhds 0)

Coordinatewise planning rate for the genuinely causal successor batch.

noncomputable def selfConsistentScheduledCausalPlanningRateAt (mdp : MDP State Action) (t : Nat) : Real

The causal coordinatewise planning rate vanishes.

theorem selfConsistentScheduledCausalPlanningRateAt_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledCausalPlanningRateAt mdp) atTop (nhds 0)

Positive scheduled successor weights applied to the coordinatewise rate.

noncomputable def selfConsistentScheduledCausalWeightedPlanningRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real

The exact causal planning average is controlled by the weighted rate envelope.

theorem selfConsistentScheduledCausalSuccessorPlanningAverageBound_le_rateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (rounds : Nat) : selfConsistentScheduledCausalSuccessorPlanningAverageBound mdp varianceProxy baseVisitFloor rounds <= selfConsistentScheduledCausalWeightedPlanningRateEnvelope mdp varianceProxy baseVisitFloor rounds

The scheduled weighted causal planning envelope tends to zero.

theorem selfConsistentScheduledCausalWeightedPlanningRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledCausalWeightedPlanningRateEnvelope mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Fixed-half global return envelope for the scheduled causal source.

noncomputable def selfConsistentScheduledCausalReturnRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real

The scheduled causal return envelope tends to zero.

theorem selfConsistentScheduledCausalReturnRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledCausalReturnRateEnvelope mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Full deterministic realized-regret envelope on the causal successor prefix.

noncomputable def selfConsistentScheduledCausalRealizedSuccessorAverageRegretRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real

The complete deterministic causal realized-regret envelope tends to zero.

theorem selfConsistentScheduledCausalRealizedSuccessorAverageRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledCausalRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy baseVisitFloor) atTop (nhds 0)

The complete deterministic causal realized-regret envelope tends to zero. -/ theorem selfConsistentScheduledCausalRealizedSuccessorAverageRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledCausalRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy baseVisitFloor) atTop (nhds 0) := by unfold selfConsistentScheduledCausalRealizedSuccessorAverageRegretRateEnvelope simpa using (selfConsistentScheduledCausalWeightedPlanningRateEnvelope_tendsto_zero mdp varianceProxy baseVisitFloor).add (selfConsistentScheduledCausalReturnRateEnvelope_tendsto_zero mdp varianceProxy baseVisitFloor) /- The deterministic regret envelope vanishes, but the exact finite-prefix model failure budget below accumulates the early coordinate events. This theorem therefore deliberately stops at a finite-prefix certificate.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_optimism_and_realizedSuccessorAverageRegret_le_explicitRateEnvelope (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) (hrounds : 0 < rounds) : let episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t let rewardBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor t let transitionBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor t let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds (1 / 2) MeasurableSet event /\ source.trajectoryMeasure event <= selfConsistentScheduledCausalModelReturnFailureBudget mdp rounds (1 / 2) /\ forall trajectory, trajectory ∉ event -> (forall round : Fin rounds, let t := (round : Nat) let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t) forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) /\ source.realizedSuccessorAverageRegret trajectory rounds <= selfConsistentScheduledCausalRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy baseVisitFloor rounds