BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationCommonSpaceL1Consistency

Mean-reward expected regret has the deterministic `2H` envelope.

theorem expectedRegret_le_two_mul_horizon_of_rewardBound {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (hrewardBound : forall state action, |mdp.reward state action| <= 1) : policy.expectedRegret initialState <= 2 * (mdp.horizon : Real)

Every selected-policy expected successor average is at most `2H`.

theorem successorExpectedAverageRegret_le_two_mul_horizon {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hrounds : 0 < rounds) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : source.successorExpectedAverageRegret trajectory rounds <= 2 * (mdp.horizon : Real)

The cumulative globally centered successor deviation inherits one global sub-Gaussian MGF from the strongly adapted conditional increments.

theorem trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_hasSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource 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) : ProbabilityTheory.HasSubgaussianMGF (source.cumulativeSuccessorGlobalReturnDeviation rounds) (cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy) source.trajectoryMeasure

Finite-window stochastic realized successor-average regret is integrable.

theorem integrable_realizedSuccessorAverageRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (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 (fun trajectory => source.realizedSuccessorAverageRegret trajectory rounds) source.trajectoryMeasure

The scaled-MGF first-moment contribution after episode/round normalization.

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

The scaled-MGF contribution is nonnegative.

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

Whenever `log (2/delta) >= 1/2`, the scaled-MGF first-moment term is at most `2 * exp(1/2)` times the compiled normalized confidence radius.

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

The scheduled confidence logarithm is uniformly at least one half.

theorem one_half_le_log_two_div_vanishingAverageConfidenceDelta (n : Nat) : (1 / 2 : Real) <= Real.log (2 / AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n)

The scheduled scaled-MGF contribution tends to zero.

theorem decayingExplorationNormalizedSuccessorGlobalReturnMGFFirstMomentBound_tendsto_zero (mdp : MDP State Action) (baseVisitFloor : Real) (rewardBound rewardVarianceProxy : NNReal) : Tendsto (fun n => normalizedSuccessorGlobalReturnMGFFirstMomentBound mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n) (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) rewardBound rewardVarianceProxy) atTop (nhds 0)

Scheduled cumulative sampled-return deviation on the stochastic common space.

noncomputable def decayingExplorationStochasticCumulativeReturnDeviationProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : DecayingExplorationStochasticWindowSpace mdp baseVisitFloor -> Real

Every common-space cumulative deviation coordinate has its exact MGF.

theorem decayingExplorationStochasticCumulativeReturnDeviationProcess_hasSubgaussianMGF (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : ProbabilityTheory.HasSubgaussianMGF (decayingExplorationStochasticCumulativeReturnDeviationProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) (AdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n) 1 rewardVarianceProxy) (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)

Every scheduled common-space realized-regret coordinate is integrable.

theorem integrable_decayingExplorationStochasticRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : Integrable (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)

Pull only the projected-count failure event to the stochastic common space.

noncomputable def decayingExplorationStochasticCommonCountBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Set (DecayingExplorationStochasticWindowSpace mdp baseVisitFloor)

The pulled-back projected-count event is measurable.

theorem measurableSet_decayingExplorationStochasticCommonCountBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : MeasurableSet (decayingExplorationStochasticCommonCountBadEvent mdp initialState initialTable defaultState baseVisitFloor n)

The common-space projected-count event consumes one confidence share.

theorem decayingExplorationStochasticCommonMeasure_countBadEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor (decayingExplorationStochasticCommonCountBadEvent mdp initialState initialTable defaultState baseVisitFloor n) <= ENNReal.ofReal (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n)

Expected absolute scheduled stochastic realized-behavior regret.

noncomputable def decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Real

Planner radius, count-failure contribution, and normalized stochastic MGF first-moment contribution.

noncomputable def decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegretBound (mdp : MDP State Action) (baseVisitFloor : Real) (rewardVarianceProxy : NNReal) (n : Nat) : Real

Expected absolute stochastic realized regret is nonnegative.

theorem decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : 0 <= decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState baseVisitFloor n

The explicit stochastic expected-absolute bound is nonnegative.

theorem decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegretBound_nonneg (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) (rewardVarianceProxy : NNReal) (n : Nat) : 0 <= decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n

The common-space expected absolute stochastic realized regret is bounded by the planner radius, one count-failure contribution, and the directly integrated normalized sub-Gaussian deviation.

theorem decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret_le_bound (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState baseVisitFloor n <= decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n

The explicit stochastic expected-absolute envelope tends to zero.

theorem decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegretBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) (rewardVarianceProxy : NNReal) : Tendsto (decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy) atTop (nhds 0)

Terminal expected-consistency theorem for unbounded sampled rewards: every coordinate is integrable, obeys the explicit three-term bound, and its expected absolute realized regret tends to zero.

theorem exploratorySource_decayingExplorationStochasticCommonMeasure_integrable_expectedAbsoluteRealizedBehaviorRegret_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (forall n, Integrable (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)) /\ (forall n, decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState baseVisitFloor n <= decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n) /\ Tendsto (decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState baseVisitFloor) atTop (nhds 0)

Every scheduled stochastic common-space coordinate belongs to `L1`.

theorem memLp_one_decayingExplorationStochasticRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : MemLp (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) 1 (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)

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

theorem eLpNorm_one_decayingExplorationStochasticRealizedBehaviorRegretProcess_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : eLpNorm (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) 1 (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor) = ENNReal.ofReal (decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState baseVisitFloor n)

The exponent-one extended norm of the stochastic process tends to zero.

theorem eLpNorm_one_decayingExplorationStochasticRealizedBehaviorRegretProcess_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => eLpNorm (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) 1 (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)) atTop (nhds 0)

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

theorem eLpNorm_one_decayingExplorationStochasticRealizedBehaviorRegretProcess_sub_zero_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => eLpNorm (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n - (fun _ => 0)) 1 (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)) atTop (nhds 0)

The stochastic scheduled realized-regret process as an `Lp Real 1` value.

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

The named stochastic `Lp` coordinate represents the original process a.e.

theorem decayingExplorationStochasticRealizedBehaviorRegretLp_coeFn_ae_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : (decayingExplorationStochasticRealizedBehaviorRegretLp mdp initialState rewardSource rewardVarianceProxy law initialTable defaultState baseVisitFloor hrewardBound n : DecayingExplorationStochasticWindowSpace mdp baseVisitFloor -> Real) =ᵐ[ decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor] decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n

The named stochastic `Lp Real 1` process converges to zero.

theorem decayingExplorationStochasticRealizedBehaviorRegretLp_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (decayingExplorationStochasticRealizedBehaviorRegretLp mdp initialState rewardSource rewardVarianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0)

Terminal stochastic `L1` theorem: coordinate membership, exact exponent-one norms, `Lp` convergence, and induced convergence in measure hold on the same independent product of complete scheduled experiments.

theorem exploratorySource_decayingExplorationStochasticCommonMeasure_memLp_eLpNorm_L1_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (forall n, MemLp (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) 1 (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)) /\ (forall n, eLpNorm (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n) 1 (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor) = ENNReal.ofReal (decayingExplorationStochasticExpectedAbsoluteRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState baseVisitFloor n)) /\ Tendsto (fun n => eLpNorm (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n - (fun _ => 0)) 1 (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor)) atTop (nhds 0) /\ Tendsto (decayingExplorationStochasticRealizedBehaviorRegretLp mdp initialState rewardSource rewardVarianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0) /\ TendstoInMeasure (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor) (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor) atTop (fun _ => 0)