BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardTotalReturnConcentration

Pair a kernel output with the input at which the kernel is evaluated.

noncomputable def retainedInputKernel (kernel : ProbabilityTheory.Kernel Input Output) : ProbabilityTheory.Kernel Input (Input × Output)

No declaration docstring is present; use the chapter context and exact statement below.

theorem retainedInputKernel_apply (kernel : ProbabilityTheory.Kernel Input Output) [ProbabilityTheory.IsMarkovKernel kernel] (input : Input) : retainedInputKernel kernel input = (kernel input).map (Prod.mk input)

Recover the conditional law of the retained input/output pair.

theorem condDistrib_pair_ae_eq_retainedInputKernel_of_pair_map_eq_compProd {Sample : Type w} [MeasurableSpace Sample] [StandardBorelSpace (Input × Output)] [Nonempty (Input × Output)] (mu : Measure Sample) [IsFiniteMeasure mu] (condition : Sample → Input) (next : Sample → Output) (kernel : ProbabilityTheory.Kernel Input Output) [ProbabilityTheory.IsMarkovKernel kernel] (hcondition : Measurable condition) (hnext : Measurable next) (hpair : mu.map (fun sample => (condition sample, next sample)) = (mu.map condition).compProd kernel) : ProbabilityTheory.condDistrib (fun sample => (condition sample, next sample)) condition mu =ᵐ[ mu.map condition] retainedInputKernel kernel

Map a statistic which depends jointly on the retained input and output.

theorem condDistrib_dynamic_map_ae_eq_of_pair_map_eq_compProd {Sample : Type w} [MeasurableSpace Sample] [StandardBorelSpace (Input × Output)] [Nonempty (Input × Output)] {Result : Type*} [MeasurableSpace Result] [StandardBorelSpace Result] [Nonempty Result] (mu : Measure Sample) [IsFiniteMeasure mu] (condition : Sample → Input) (next : Sample → Output) (kernel : ProbabilityTheory.Kernel Input Output) [ProbabilityTheory.IsMarkovKernel kernel] (g : Input × Output → Result) (hcondition : Measurable condition) (hnext : Measurable next) (hg : Measurable g) (hpair : mu.map (fun sample => (condition sample, next sample)) = (mu.map condition).compProd kernel) : ProbabilityTheory.condDistrib (fun sample => g (condition sample, next sample)) condition mu =ᵐ[ mu.map condition] (retainedInputKernel kernel).map g

A complete stochastic-reward episode batch.

abbrev StochasticEpisodeBatch (mdp : MDP State Action) (episodes : Nat)

Finite history through stochastic batch coordinate `n`.

abbrev StochasticEpisodeBatchPrefix (mdp : MDP State Action) (episodes n : Nat)

Infinite stochastic episode-batch trajectory.

abbrev StochasticEpisodeBatchTrajectory (mdp : MDP State Action) (episodes : Nat)

An adaptive source of complete stochastic-reward episode batches. The dynamic measurability field is the only additional policy-selection regularity needed by this route. The exact batch-kernel equality supplies the pointwise conditionally iid law selected by each observed prefix.

structure AdaptiveStochasticEpisodeBatchSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) where

The adaptive infinite stochastic batch-trajectory law.

noncomputable def trajectoryMeasure {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : Measure (StochasticEpisodeBatchTrajectory mdp episodes)

Coordinate zero has the configured initial stochastic batch law.

theorem trajectoryMeasure_map_eval_zero {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : source.trajectoryMeasure.map (Function.eval 0) = source.rewardSource.iidStochasticTrajectoryFamilyMeasure source.initialPolicy initialState episodes

The prefix/next-batch marginal has the configured compProd law.

theorem trajectoryMeasure_prefix_compProd {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : source.trajectoryMeasure.map (Preorder.frestrictLe n) ⊗ₘ source.batchKernel n = source.trajectoryMeasure.map (fun trajectory => (Preorder.frestrictLe n trajectory, trajectory (n + 1)))

The dynamic next-round sampled-return statistic on prefix/batch pairs.

noncomputable def successorSampledReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (pair : StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes) : Real

Conditional kernel of the dynamic next-round deviation.

noncomputable def successorDeviationKernel {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : ProbabilityTheory.Kernel (StochasticEpisodeBatchPrefix mdp episodes n) Real

Each deviation-kernel fiber is the selected policy's iid statistic law.

theorem successorDeviationKernel_apply {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : source.successorDeviationKernel n history = (source.rewardSource.iidStochasticTrajectoryFamilyMeasure (source.successorPolicy n history) initialState episodes).map (mdp.sampledCumulativeReturnDeviationSum (source.successorPolicy n history) episodes)

The trajectory-level dynamic deviation at successor coordinate `n + 1`.

noncomputable def successorSampledReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_successorSampledReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : Measurable (source.successorSampledReturnDeviationAt n)

The conditional law of the dynamic successor deviation.

theorem trajectoryMeasure_condDistrib_successorSampledReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : ProbabilityTheory.condDistrib (source.successorSampledReturnDeviationAt n) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.successorDeviationKernel n

The trimmed conditional-expectation kernel has the same dynamic law.

theorem condExpKernel_map_successorSampledReturnDeviationAt_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : Filter.Eventually (fun trajectory : StochasticEpisodeBatchTrajectory mdp episodes => Measure.map (source.successorSampledReturnDeviationAt n) (ProbabilityTheory.condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (StochasticEpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = source.successorDeviationKernel n (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))

Prefix-level increment, including the genuine initial stochastic batch.

noncomputable def sampledReturnDeviationPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : (round : Nat) → StochasticEpisodeBatchPrefix mdp episodes round → Real | 0, history => mdp.sampledCumulativeReturnDeviationSum source.initialPolicy episodes (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩) | n + 1, history => source.successorSampledReturnDeviation n (Preorder.frestrictLe₂ (π

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_sampledReturnDeviationPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) : Measurable (source.sampledReturnDeviationPrefixIncrement round)

Adapted sampled-return deviation increment on the full trajectory.

noncomputable def sampledReturnDeviationIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_sampledReturnDeviationIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) : Measurable (source.sampledReturnDeviationIncrement round)

No declaration docstring is present; use the chapter context and exact statement below.

theorem sampledReturnDeviationIncrement_stronglyAdapted_piLE {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : StronglyAdapted (Filtration.piLE (X

The initial adaptive coordinate inherits the iid batch MGF.

theorem sampledReturnDeviationIncrement_zero_hasSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : ProbabilityTheory.HasSubgaussianMGF (source.sampledReturnDeviationIncrement 0) (mdp.iidSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy) source.trajectoryMeasure

Every successor adaptive coordinate is conditionally sub-Gaussian.

theorem sampledReturnDeviationIncrement_succ_hasCondSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : ProbabilityTheory.HasCondSubgaussianMGF (Filtration.piLE (X

Sum of per-round proxies over `rounds` adaptive stochastic batches.

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

No declaration docstring is present; use the chapter context and exact statement below.

theorem cumulativeSampledReturnDeviationVarianceProxy_eq (mdp : MDP State Action) (rounds episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) : cumulativeSampledReturnDeviationVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy = (rounds : NNReal) * mdp.iidSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy

Cumulative sampled-return deviation over `rounds` adaptive batches.

noncomputable def cumulativeSampledReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : Real

Fixed-round two-sided tail for adaptive stochastic sampled returns.

theorem trajectoryMeasure_cumulativeSampledReturnDeviation_abs_tail_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSampledReturnDeviationVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) : source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (cumulativeSampledReturnDeviationVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy) delta ≤ |source.cumulativeSampledReturnDeviation rounds trajectory|} ≤ ENNReal.ofReal delta