BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeExplicitThreeQuarterGoodEventAverageRealizedBehaviorRegret

A shifted inverse-power prefix with exponent at least six is at most one sixteenth. This refines the existing inverse-square comparison.

theorem sum_range_one_div_natCast_add_two_pow_le_one_div_sixteen (rounds exponent : Nat) (hexponent : 6 <= exponent) : (Finset.range rounds).sum (fun t => 1 / (((t + 2 : Nat) : Real) ^ exponent)) <= 1 / 16

The finite scheduled model budget is the ENNReal image of twice the real sum of its local confidence schedule.

theorem selfConsistentScheduledCausalModelFailureBudget_eq_ofReal_two_mul_sum (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledCausalModelFailureBudget mdp rounds = ENNReal.ofReal (2 * (Finset.range rounds).sum fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp t)

Every finite prefix of the existing self-consistent model schedule spends at most one eighth of probability mass across both model-confidence shares.

theorem selfConsistentScheduledCausalModelFailureBudget_le_one_eighth (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (rounds : Nat) : selfConsistentScheduledCausalModelFailureBudget mdp rounds <= ENNReal.ofReal (1 / 8 : Real)

With return budget one eighth, the joint horizon-level model event and all positive-prefix return events have probability at most one quarter. Its measurable complement has real probability at least three quarters.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_boundedStoppingSingleModelReturnBadEvent_le_one_quarter (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) (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds (1 / 8 : Real) MeasurableSet event /\ source.trajectoryMeasure event <= ENNReal.ofReal (1 / 4 : Real) /\ (3 / 4 : Real) <= source.trajectoryMeasure.real event.compl

With return budget one eighth, the joint horizon-level model event and all positive-prefix return events have probability at most one quarter. Its measurable complement has real probability at least three quarters. -/ theorem selfConsistentScheduledCausalSource_trajectoryMeasure_boundedStoppingSingleModelReturnBadEvent_le_one_quarter (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) (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds (1 / 8 : Real) MeasurableSet event /\ source.trajectoryMeasure event <= ENNReal.ofReal (1 / 4 : Real) /\ (3 / 4 : Real) <= source.trajectoryMeasure.real event.compl := by dsimp only let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds (1 / 8 : Real) have hparent := selfConsistentScheduledCausalSource_trajectoryMeasure_boundedStoppingSingleModelReturnBadEvent_le mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor maxRounds hmaxRounds (1 / 8 : Real) (by norm_num) (by norm_num) have heventMeasurable : MeasurableSet event := by simpa [event] using hparent.1 have hmodel : selfConsistentScheduledCausalModelFailureBudget mdp maxRounds <= ENNReal.ofReal (1 / 8 : Real) := selfConsistentScheduledCausalModelFailureBudget_le_one_eighth mdp hhorizon maxRounds have hbudget : selfConsistentScheduledCausalModelFailureBudget mdp maxRounds + ENNReal.ofReal (1 / 8 : Real) <= ENNReal.ofReal (1 / 4 : Real) := by calc selfConsistentScheduledCausalModelFailureBudget mdp maxRounds + ENNReal.ofReal (1 / 8 : Real) <= ENNReal.ofReal (1 / 8 : Real) + ENNReal.ofReal (1 / 8 : Real) := add_le_add hmodel (le_refl _) _ = ENNReal.ofReal ((1 / 8 : Real) + (1 / 8 : Real)) := by rw [ENNReal.ofReal_add (by norm_num) (by norm_num)] _ = ENNReal.ofReal (1 / 4 : Real) := by norm_num have heventTail : source.trajectoryMeasure event <= ENNReal.ofReal (1 / 4 : Real) := by have hraw : source.trajectoryMeasure event <= selfConsistentScheduledCausalModelFailureBudget mdp maxRounds + ENNReal.ofReal (1 / 8 : Real) := by simpa [source, event] using hparent.2 exact hraw.trans hbudget have heventTailReal : source.trajectoryMeasure.real event <= 1 / 4 := by apply ENNReal.toReal_le_of_le_ofReal (by norm_num) exact heventTail have hgoodMass : (3 / 4 : Real) <= source.trajectoryMeasure.real event.compl := by change (3 / 4 : Real) <= source.trajectoryMeasure.real (eventᶜ) rw [MeasureTheory.probReal_compl_eq_one_sub heventMeasurable] linarith exact ⟨heventMeasurable, heventTail, hgoodMass⟩ /- Terminal explicit-confidence route. The good event is the complement of the same single-model/return event used by the compiled bounded-stopping parent.

theorem selfConsistentScheduledCausalSource_boundedStoppingTimeExplicitThreeQuarterGoodEventAverageRealizedBehaviorRegret (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 stoppedViolation := selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau let event := selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds (1 / 8 : Real) let goodEvent := event.compl MeasurableSet[ selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds] stoppedViolation /\ MeasurableSet event /\ MeasurableSet goodEvent /\ stoppedViolation ⊆ event /\ selfConsistentScheduledCausalModelFailureBudget mdp maxRounds <= ENNReal.ofReal (1 / 8 : Real) /\ source.trajectoryMeasure event <= ENNReal.ofReal (1 / 4 : Real) /\ source.trajectoryMeasure stoppedViolation <= ENNReal.ofReal (1 / 4 : Real) /\ (3 / 4 : Real) <= source.trajectoryMeasure.real goodEvent /\ forall trajectory, trajectory ∈ goodEvent -> selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau trajectory <= selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau trajectory