BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeExplicitExpectedAverageRealizedBehaviorRegret

The cumulative behavior expected-regret process belongs to `L2` under its deterministic finite-prefix envelope.

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

Every deterministic-prefix average realized behavior-regret coordinate is in `L2`: the behavior component is bounded and the centered return component is sub-Gaussian.

theorem memLp_two_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess (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 (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 2 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure

Mathlib bounded-stopping transport gives `L2` for the exact stopped average realized behavior regret.

theorem memLp_two_selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret (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) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (htau : IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) tau) (maxRounds : Nat) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) : MemLp (selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau) 2 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure

Every deterministic logarithmic average-rate coordinate is nonnegative.

theorem selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (returnDelta : Real) : 0 <= selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate mdp varianceProxy baseVisitFloor rounds returnDelta

Deterministic finite sum which dominates the logarithmic rate selected by any positive stopping time bounded by `maxRounds`.

noncomputable def selfConsistentScheduledNaturalCausalBoundedStoppingExplicitExpectedRateBudget (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (maxRounds : Nat) : Real

The finite expected-rate budget is nonnegative.

theorem selfConsistentScheduledNaturalCausalBoundedStoppingExplicitExpectedRateBudget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (maxRounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalBoundedStoppingExplicitExpectedRateBudget mdp varianceProxy baseVisitFloor maxRounds

The stopped logarithmic rate is charged to the finite positive-prefix rate budget without assuming endpoint monotonicity.

theorem selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate_le_explicitExpectedRateBudget (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (maxRounds : Nat) (htau_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (fun _ => selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds (1 / 8 : Real)) tau trajectory <= selfConsistentScheduledNaturalCausalBoundedStoppingExplicitExpectedRateBudget mdp varianceProxy baseVisitFloor maxRounds

Exact stopped second moment on the generated causal trajectory measure.

noncomputable def selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) : Real

The exact stopped second moment is nonnegative.

theorem selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) : 0 <= selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau

The exact stopped second moment is nonnegative. -/ theorem selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) : 0 <= selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau := by unfold selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment exact integral_nonneg fun _ => sq_nonneg _ /- Terminal expected-regret route. The bad-event contribution is charged through the exact stopped second moment; no optional-stopping theorem is used.

theorem selfConsistentScheduledCausalSource_boundedStoppingTimeExplicitExpectedAverageRealizedBehaviorRegret (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) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (htau : IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) tau) (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) (htau_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let returnDeltaAt := fun _ : Nat => selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds (1 / 8 : Real) let event := selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds (1 / 8 : Real) let goodEvent := event.compl let stoppedRegret := selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau let stoppedRate := selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau let rateBudget := selfConsistentScheduledNaturalCausalBoundedStoppingExplicitExpectedRateBudget mdp varianceProxy baseVisitFloor maxRounds let secondMoment := selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau MemLp stoppedRegret 2 source.trajectoryMeasure /\ MeasurableSet event /\ source.trajectoryMeasure event <= ENNReal.ofReal (1 / 4 : Real) /\ (3 / 4 : Real) <= source.trajectoryMeasure.real goodEvent /\ 0 <= rateBudget /\ 0 <= secondMoment /\ integral source.trajectoryMeasure (event.indicator (fun trajectory => |stoppedRegret trajectory|)) <= (1 / 2 : Real) * Real.sqrt secondMoment /\ integral source.trajectoryMeasure stoppedRegret <= rateBudget + (1 / 2 : Real) * Real.sqrt secondMoment /\ forall trajectory, trajectory ∈ goodEvent -> stoppedRegret trajectory <= stoppedRate trajectory