BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceL1Consistency

Every heterogeneous weighted selected-policy average is at most `2H`.

theorem successorWeightedExpectedAverageRegret_le_two_mul_horizon {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hmass : 0 < successorEpisodeMass episodes rounds) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : source.successorWeightedExpectedAverageRegret trajectory rounds <= 2 * (mdp.horizon : Real)

The heterogeneous successor deviation has one global sub-Gaussian MGF.

theorem trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_hasSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : HasSubgaussianMGF (source.cumulativeSuccessorGlobalReturnDeviation rounds) (cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy) source.trajectoryMeasure

Finite-prefix heterogeneous realized successor-average regret is integrable.

theorem integrable_realizedSuccessorAverageRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : forall t, 0 < episodes t) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (hrewardBoundOne : forall state action, |mdp.reward state action| <= 1) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : Integrable (source.realizedSuccessorAverageRegret (rounds := rounds)) source.trajectoryMeasure

Direct first-moment envelope for the normalized heterogeneous deviation.

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

The normalized heterogeneous MGF first-moment envelope is nonnegative.

theorem normalizedSuccessorGlobalReturnMGFFirstMomentBound_nonneg (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : 0 <= normalizedSuccessorGlobalReturnMGFFirstMomentBound mdp episodes rounds rewardBound rewardVarianceProxy

A sufficiently wide normalized confidence radius dominates the MGF mean.

theorem normalizedSuccessorGlobalReturnMGFFirstMomentBound_le_confidenceRadius (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) (hmass : 0 < successorEpisodeMass episodes rounds) (hlog : (1 / 2 : Real) <= Real.log (2 / delta)) : normalizedSuccessorGlobalReturnMGFFirstMomentBound mdp episodes rounds rewardBound rewardVarianceProxy <= 2 * Real.exp (1 / 2 : Real) * normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes rounds rewardBound rewardVarianceProxy delta

Every post-burn-in model budget is finite.

theorem selfConsistentScheduledCausalTailModelFailureBudget_ne_top (mdp : MDP State Action) (burnin : Nat) : selfConsistentScheduledCausalTailModelFailureBudget mdp burnin ≠ ⊤

The real-valued post-burn-in model tail also tends to zero.

theorem selfConsistentScheduledCausalTailModelFailureBudget_toReal_tendsto_zero (mdp : MDP State Action) : Tendsto (fun burnin => (selfConsistentScheduledCausalTailModelFailureBudget mdp burnin).toReal) atTop (nhds 0)

Scheduled direct-MGF contribution under actual successor mass.

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

The scheduled direct-MGF contribution is nonnegative.

theorem selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound mdp varianceProxy baseVisitFloor rounds

The scheduled direct-MGF first-moment contribution tends to zero.

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

The fixed-burn-in expected-regret envelope is nonnegative.

theorem selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : 0 <= selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope mdp varianceProxy baseVisitFloor burnin rounds

Expected absolute regret of one natural causal prefix.

noncomputable def selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real

Two-parameter direct `L1` envelope after a fixed model burn-in.

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

The direct natural-causal `L1` envelope is nonnegative.

theorem selfConsistentScheduledCausalBurninExpectedAbsoluteRegretL1Envelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : 0 <= selfConsistentScheduledCausalBurninExpectedAbsoluteRegretL1Envelope mdp varianceProxy baseVisitFloor burnin rounds

Every coordinate of the natural causal realized-regret process is integrable.

theorem integrable_selfConsistentScheduledNaturalCausalRealizedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (rounds : Nat) : Integrable (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure

Expected absolute natural-causal regret is nonnegative.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds

The expected absolute natural-causal regret is controlled by the good-event planning envelope, the bounded model-tail overflow, and the directly integrated global-return MGF contribution.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_le_burninL1Envelope (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (hrounds : 0 < rounds) : selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledCausalBurninExpectedAbsoluteRegretL1Envelope mdp varianceProxy baseVisitFloor burnin rounds

Expected absolute regret on the natural causal prefixes tends to zero.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_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) : Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)

Every coordinate of the natural causal process belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (rounds : Nat) : MemLp (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure

At exponent one, `eLpNorm` is the lifted expected absolute regret.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (rounds : Nat) : eLpNorm (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)

The exponent-one extended norm on the causal prefixes tends to zero.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_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) : Tendsto (fun rounds => eLpNorm (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)

Canonical natural-causal `L1` norm-of-the-difference convergence.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_sub_zero_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) : Tendsto (fun rounds => eLpNorm (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds - (fun _ => 0)) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)

The natural causal realized-regret process as an `Lp Real 1` value.

noncomputable def selfConsistentScheduledNaturalCausalRealizedRegretLp (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (rounds : Nat) : Lp Real 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure

The named natural-causal `Lp` coordinate represents the process a.e.

theorem selfConsistentScheduledNaturalCausalRealizedRegretLp_coeFn_ae_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (rounds : Nat) : (selfConsistentScheduledNaturalCausalRealizedRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound rounds : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Real) =ᵐ[ (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure] selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds

The named natural-causal `Lp Real 1` process converges to zero.

theorem selfConsistentScheduledNaturalCausalRealizedRegretLp_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) : Tendsto (selfConsistentScheduledNaturalCausalRealizedRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0)

Terminal natural-causal `L1` theorem on one heterogeneous dependent trajectory measure: exact exponent-one norms, `Lp` convergence, and convergence in measure.

theorem selfConsistentScheduledCausalSource_naturalRealizedRegret_memLp_eLpNorm_L1_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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, MemLp (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 source.trajectoryMeasure) /\ (forall rounds, eLpNorm (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 source.trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) /\ Tendsto (fun rounds => eLpNorm (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds - (fun _ => 0)) 1 source.trajectoryMeasure) atTop (nhds 0) /\ Tendsto (selfConsistentScheduledNaturalCausalRealizedRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0) /\ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)