BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeExplicitDeterministicMomentExpectedAverageRealizedBehaviorRegret

The cumulative behavior expected-regret process has its deterministic finite-prefix envelope.

theorem selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_le_rounds_mul_two_horizon (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) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= (rounds : Real) * (2 * (mdp.horizon : Real))

Deterministic envelope for the second moment at one positive prefix.

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

The deterministic coordinate second-moment envelope is nonnegative.

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

At every positive deterministic prefix, the exact average realized behavior-regret second moment is bounded by the deterministic envelope.

theorem integral_sq_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_secondMomentEnvelope (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) (hrounds : 0 < rounds) : integral (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure (fun trajectory => selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory ^ 2) <= selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretSecondMomentEnvelope mdp varianceProxy baseVisitFloor rounds

A finite deterministic second-moment budget covering every positive prefix up to `maxRounds`.

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

The deterministic finite-prefix second-moment budget is nonnegative.

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

A positive bounded stopping time selects one coordinate from the finite prefix sum, so its exact second moment is bounded by the deterministic budget. No optional-stopping theorem is used.

theorem selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment_le_explicitBudget (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_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) : selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau <= selfConsistentScheduledNaturalCausalBoundedStoppingExplicitSecondMomentBudget mdp varianceProxy baseVisitFloor maxRounds

A positive bounded stopping time selects one coordinate from the finite prefix sum, so its exact second moment is bounded by the deterministic budget. No optional-stopping theorem is used. -/ theorem selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment_le_explicitBudget (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_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) : selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau <= selfConsistentScheduledNaturalCausalBoundedStoppingExplicitSecondMomentBudget mdp varianceProxy baseVisitFloor maxRounds := by let mu := (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure let process := selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppedRegret := selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau have hcoordinateIntegrable : forall rounds, Integrable (fun trajectory => process rounds trajectory ^ 2) mu := by intro rounds exact (memLp_two_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound rounds).integrable_sq have hsumIntegrable : Integrable (fun trajectory => (Finset.Icc 1 maxRounds).sum fun rounds => process rounds trajectory ^ 2) mu := by exact IntegrabilitySums.integrable_finset_sum mu (Finset.Icc 1 maxRounds) (fun rounds trajectory => process rounds trajectory ^ 2) (fun rounds _ => hcoordinateIntegrable rounds) have hstoppedIntegrable : Integrable (fun trajectory => stoppedRegret trajectory ^ 2) mu := by exact (memLp_two_selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound tau htau maxRounds htau_le).integrable_sq have hpoint : forall trajectory, stoppedRegret trajectory ^ 2 <= (Finset.Icc 1 maxRounds).sum fun rounds => process rounds trajectory ^ 2 := by intro trajectory have hrange := one_le_untopA_and_untopA_le_of_withTop_bounds tau maxRounds htau_pos htau_le trajectory change process (tau trajectory).untopA trajectory ^ 2 <= _ exact Finset.single_le_sum (fun rounds _ => sq_nonneg (process rounds trajectory)) (Finset.mem_Icc.mpr hrange) have hintegral : integral mu (fun trajectory => stoppedRegret trajectory ^ 2) <= (Finset.Icc 1 maxRounds).sum fun rounds => integral mu (fun trajectory => process rounds trajectory ^ 2) := by calc integral mu (fun trajectory => stoppedRegret trajectory ^ 2) <= integral mu (fun trajectory => (Finset.Icc 1 maxRounds).sum fun rounds => process rounds trajectory ^ 2) := integral_mono hstoppedIntegrable hsumIntegrable hpoint _ = (Finset.Icc 1 maxRounds).sum fun rounds => integral mu (fun trajectory => process rounds trajectory ^ 2) := by exact ExpectationBochnerSums.integral_finset_sum mu (Finset.Icc 1 maxRounds) (fun rounds trajectory => process rounds trajectory ^ 2) (fun rounds _ => hcoordinateIntegrable rounds) unfold selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegretSecondMoment selfConsistentScheduledNaturalCausalBoundedStoppingExplicitSecondMomentBudget change integral mu (fun trajectory => stoppedRegret trajectory ^ 2) <= _ calc integral mu (fun trajectory => stoppedRegret trajectory ^ 2) <= (Finset.Icc 1 maxRounds).sum fun rounds => integral mu (fun trajectory => process rounds trajectory ^ 2) := hintegral _ <= (Finset.Icc 1 maxRounds).sum fun rounds => selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretSecondMomentEnvelope mdp varianceProxy baseVisitFloor rounds := by exact Finset.sum_le_sum fun rounds hrounds => integral_sq_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_secondMomentEnvelope mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound rounds (Finset.mem_Icc.mp hrounds).1 /- Terminal deterministic-moment expected-regret route. The exact stopped second moment is retained as a local quantity but exposed with a finite deterministic upper budget.

theorem selfConsistentScheduledCausalSource_boundedStoppingTimeExplicitDeterministicMomentExpectedAverageRealizedBehaviorRegret (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 let momentBudget := selfConsistentScheduledNaturalCausalBoundedStoppingExplicitSecondMomentBudget mdp varianceProxy baseVisitFloor maxRounds 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 <= momentBudget /\ secondMoment <= momentBudget /\ integral source.trajectoryMeasure (event.indicator (fun trajectory => |stoppedRegret trajectory|)) <= (1 / 2 : Real) * Real.sqrt momentBudget /\ integral source.trajectoryMeasure stoppedRegret <= rateBudget + (1 / 2 : Real) * Real.sqrt momentBudget /\ forall trajectory, trajectory ∈ goodEvent -> stoppedRegret trajectory <= stoppedRate trajectory