BanditRLProof.RL.FiniteHorizonAdaptiveEpisodeBatchLaw

Finite history through batch coordinate `n`.

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

Infinite batch trajectory used by the adaptive Ionescu--Tulcea law.

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

An adaptive batch source. Coordinate zero is generated by `initialPolicy`. After observing the prefix through coordinate `n`, `successorPolicy n history` selects the policy for coordinate `n + 1`. `batchKernel_eq_iidEpisodeBatchMeasure` is the exact law transport contract: it also certifies that the history-indexed family is a measurable Markov kernel rather than merely a pointwise family of measures.

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

The adaptive infinite batch-trajectory law.

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

Coordinate zero has the batch law of the configured initial policy.

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

Every successor prefix/next-batch marginal is the compProd of the prefix law and the configured adaptive batch kernel.

theorem trajectoryMeasure_prefix_compProd {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource 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 next batch conditioned on the full finite prefix has the configured history-dependent Markov kernel.

theorem trajectoryMeasure_condDistrib {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) : ProbabilityTheory.condDistrib (fun trajectory : EpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) source.trajectoryMeasure =ᶠ[ ae (source.trajectoryMeasure.map (Preorder.frestrictLe n))] source.batchKernel n

The next batch conditioned on the finite prefix is exactly the generated iid batch law of the policy selected from that prefix.

theorem trajectoryMeasure_condDistrib_eq_iidEpisodeBatchMeasure {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) : ProbabilityTheory.condDistrib (fun trajectory : EpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) source.trajectoryMeasure =ᶠ[ ae (source.trajectoryMeasure.map (Preorder.frestrictLe n))] fun history => (source.successorPolicy n history).iidEpisodeBatchMeasure initialState episodes

Pull an initial-coordinate event back to the adaptive trajectory.

def initialBadEvent {mdp : MDP State Action} {episodes : Nat} (bad : Set (EpisodeBatch mdp episodes)) : Set (EpisodeBatchTrajectory mdp episodes)

Pull a prefix-dependent successor event back to the adaptive trajectory.

def successorBadEvent {mdp : MDP State Action} {episodes : Nat} (n : Nat) (bad : Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)) : Set (EpisodeBatchTrajectory mdp episodes)

Round-indexed adapted bad event, with a separate coordinate-zero event.

def roundBadEvent {mdp : MDP State Action} {episodes : Nat} (initialBad : Set (EpisodeBatch mdp episodes)) (successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)) : Nat -> Set (EpisodeBatchTrajectory mdp episodes) | 0 => initialBadEvent initialBad | n + 1 => successorBadEvent n (successorBad n) /-- Union of the first `rounds` adapted bad events. -/ def finiteHorizonBadEvent {mdp : MDP State Action} {episodes : Nat} (rounds : Nat) (initialBad : Set (EpisodeBatch mdp episodes)) (successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)) : Set (EpisodeBatchTrajectory mdp episodes)

Union of the first `rounds` adapted bad events.

def finiteHorizonBadEvent {mdp : MDP State Action} {episodes : Nat} (rounds : Nat) (initialBad : Set (EpisodeBatch mdp episodes)) (successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)) : Set (EpisodeBatchTrajectory mdp episodes)

Measurability of every pulled-back adapted round event.

theorem measurableSet_roundBadEvent {mdp : MDP State Action} {episodes : Nat} {initialBad : Set (EpisodeBatch mdp episodes)} {successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)} (hinitial : MeasurableSet initialBad) (hsuccessor : forall n, MeasurableSet (successorBad n)) (round : Nat) : MeasurableSet (roundBadEvent initialBad successorBad round)

Measurability of the finite adapted bad-event union.

theorem measurableSet_finiteHorizonBadEvent {mdp : MDP State Action} {episodes rounds : Nat} {initialBad : Set (EpisodeBatch mdp episodes)} {successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)} (hinitial : MeasurableSet initialBad) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (successorBad n)) : MeasurableSet (finiteHorizonBadEvent rounds initialBad successorBad)

Exact mass of a pulled-back coordinate-zero event.

theorem trajectoryMeasure_initialBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) {bad : Set (EpisodeBatch mdp episodes)} (hbad : MeasurableSet bad) : source.trajectoryMeasure (initialBadEvent bad) = source.initialPolicy.iidEpisodeBatchMeasure initialState episodes bad

An adapted successor event inherits a uniform bound on every history fiber.

theorem trajectoryMeasure_successorBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) {bad : Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)} (hbad : MeasurableSet bad) (budget : ENNReal) (hfiber : forall history, source.batchKernel n history (Prod.mk history ⁻¹' bad) <= budget) : source.trajectoryMeasure (successorBadEvent n bad) <= budget

Every adapted round event inherits the supplied local budget.

theorem trajectoryMeasure_roundBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) {initialBad : Set (EpisodeBatch mdp episodes)} {successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)} (rounds : Nat) (hinitial : MeasurableSet initialBad) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (successorBad n)) (budget : ENNReal) (hinitial_le : source.initialPolicy.iidEpisodeBatchMeasure initialState episodes initialBad <= budget) (hsuccessor_le : forall n, n + 1 < rounds -> forall history, source.batchKernel n history (Prod.mk history ⁻¹' successorBad n) <= budget) (round : Fin rounds) : source.trajectoryMeasure (roundBadEvent initialBad successorBad round) <= budget

Finite-horizon adaptive union bound with equal confidence shares `delta / rounds`. Independence between batches is not assumed.

theorem trajectoryMeasure_finiteHorizonBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (delta : Real) {initialBad : Set (EpisodeBatch mdp episodes)} {successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)} (hinitial : MeasurableSet initialBad) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (successorBad n)) (hinitial_le : source.initialPolicy.iidEpisodeBatchMeasure initialState episodes initialBad <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)) (hsuccessor_le : forall n, n + 1 < rounds -> forall history, source.batchKernel n history (Prod.mk history ⁻¹' successorBad n) <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)) : source.trajectoryMeasure (finiteHorizonBadEvent rounds initialBad successorBad) <= ENNReal.ofReal delta

Terminal adaptive law-and-budget package: every successor conditional law is the generated iid batch law of the history-selected policy, and arbitrary measurable adapted local events obey one global finite-horizon delta budget.

theorem trajectoryMeasure_conditionalLaw_and_finiteHorizonBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (delta : Real) {initialBad : Set (EpisodeBatch mdp episodes)} {successorBad : (n : Nat) -> Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)} (hinitial : MeasurableSet initialBad) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (successorBad n)) (hinitial_le : source.initialPolicy.iidEpisodeBatchMeasure initialState episodes initialBad <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)) (hsuccessor_le : forall n, n + 1 < rounds -> forall history, source.batchKernel n history (Prod.mk history ⁻¹' successorBad n) <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)) : (forall n, ProbabilityTheory.condDistrib (fun trajectory : EpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) source.trajectoryMeasure =ᶠ[ ae (source.trajectoryMeasure.map (Preorder.frestrictLe n))] fun history => (source.successorPolicy n history).iidEpisodeBatchMeasure initialState episodes) ∧ MeasurableSet (finiteHorizonBadEvent rounds initialBad successorBad) ∧ source.trajectoryMeasure (finiteHorizonBadEvent rounds initialBad successorBad) <= ENNReal.ofReal delta

Count-confidence event for the initial policy's coordinate-zero batch.

def initialSimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) : Set (EpisodeBatch mdp episodes)

Prefix/next-batch count event for the policy selected from that prefix.

def successorSimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) (n : Nat) : Set (EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes)

The finite-horizon union of initial and history-selected simultaneous count events on the adaptive batch trajectory.

def adaptiveSimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) : Set (EpisodeBatchTrajectory mdp episodes)

Policy used at a batch coordinate of one adaptive trajectory.

def policyAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) : Nat -> MarkovPolicy mdp | 0 => source.initialPolicy | n + 1 => source.successorPolicy n (Preorder.frestrictLe n trajectory) omit [Nonempty State] [Nonempty Action] in /-- The initial count event receives the common local confidence share. -/ theorem initialSimultaneousCountBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.initialPolicy.iidEpisodeBatchMeasure initialState episodes (source.initialSimultaneousCountBadEvent rounds delta) <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)

The initial count event receives the common local confidence share.

theorem initialSimultaneousCountBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.initialPolicy.iidEpisodeBatchMeasure initialState episodes (source.initialSimultaneousCountBadEvent rounds delta) <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)

Every history fiber of the selected-policy successor count event receives the same local confidence share.

theorem successorSimultaneousCountBadEvent_fiber_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (n : Nat) (history : EpisodeBatchPrefix mdp episodes n) : source.batchKernel n history (Prod.mk history ⁻¹' source.successorSimultaneousCountBadEvent rounds delta n) <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)

Measurability of the adaptive simultaneous-count union.

theorem measurableSet_adaptiveSimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (source.successorSimultaneousCountBadEvent rounds delta n)) : MeasurableSet (source.adaptiveSimultaneousCountBadEvent rounds delta)

Adaptive global-delta simultaneous count confidence. Outside one measurable finite-horizon event, every realized batch satisfies the strict count deviation bound relative to the policy selected from its preceding history.

theorem trajectoryMeasure_adaptiveSimultaneousCountConfidence {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (source.successorSimultaneousCountBadEvent rounds delta n)) : MeasurableSet (source.adaptiveSimultaneousCountBadEvent rounds delta) ∧ source.trajectoryMeasure (source.adaptiveSimultaneousCountBadEvent rounds delta) <= ENNReal.ofReal delta ∧ forall trajectory, trajectory ∉ source.adaptiveSimultaneousCountBadEvent rounds delta -> forall round : Fin rounds, forall coordinate : CountCoordinate mdp, |coordinate.deviation (source.policyAt trajectory round) initialState (trajectory round)| < simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta)