BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIBellmanInnovation

Chronological Bellman innovation for a deterministic action table. The sampled action coordinate is deliberately ignored: the table chooses the action from the recursively reconstructed current state. This makes the pathwise recursion canonical on every batch, while its law is still the exact generated deterministic-policy trajectory law.

noncomputable def sampledCumulativeDeterministicGapInnovationFrom (mdp : MDP State Action) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> StepTrace Action State remaining -> Real | 0, _, _, _ => 0 | remaining + 1, hremaining, state, trace => let stage : Fin mdp.horizon := ⟨mdp.horizon - (remaining + 1), by omega⟩ mdp.transitionValue (feature stage) state (table stage state) - feature stage (trace 0).2 + sampledCumulativeDeterministicGapInnovationFrom mdp table feature remaining (by omega) (trace 0).2 (Fin.tail trace) omit [Nonempty State] [Nonempty Action] in theorem measurable_sampledCumulativeDeterministicGapInnovationFrom (mdp : MDP State Action) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (fun p : State × StepTrace Action State remaining => mdp.sampledCumulativeDeterministicGapInnovationFrom table feature remaining hremaining p.1 p.2)

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

theorem measurable_sampledCumulativeDeterministicGapInnovationFrom (mdp : MDP State Action) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (fun p : State × StepTrace Action State remaining => mdp.sampledCumulativeDeterministicGapInnovationFrom table feature remaining hremaining p.1 p.2)

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

theorem actionStateKernel_deterministicGapInnovation_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (table : DeterministicMarkovPolicyTable mdp) (feature : State -> Real) (hfeature : forall nextState, feature nextState ∈ Set.Icc (0 : Real) mdp.horizon) (stage : Fin mdp.horizon) (currentState : State) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun head : Action × State => tilt * (mdp.transitionValue feature currentState (table stage currentState) - feature head.2) - tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (table.toMarkovPolicy.actionStateKernel stage currentState)

Stage-resolved MGF for the canonicalized deterministic trajectory.

theorem trajectoryKernelRemaining_deterministicGapInnovation_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) (tilt : Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (currentState : State) : Concentration.HasMGFUpperBoundAt (fun trace => tilt * mdp.sampledCumulativeDeterministicGapInnovationFrom table feature remaining hremaining currentState trace - (remaining : Real) * tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (table.toMarkovPolicy.trajectoryKernelRemaining remaining hremaining currentState)

Integrating the start state preserves the canonical deterministic-table stage-resolved MGF.

theorem trajectoryMeasure_deterministicGapInnovation_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun trajectory => tilt * mdp.sampledCumulativeDeterministicGapInnovationFrom table feature mdp.horizon le_rfl trajectory.1 trajectory.2 - (mdp.horizon : Real) * tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (table.toMarkovPolicy.trajectoryMeasure initialState)

Pathwise envelope for the canonical deterministic-table innovation.

theorem abs_sampledCumulativeDeterministicGapInnovationFrom_le (mdp : MDP State Action) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) : forall remaining (hremaining : remaining <= mdp.horizon) (currentState : State) (trace : StepTrace Action State remaining), |mdp.sampledCumulativeDeterministicGapInnovationFrom table feature remaining hremaining currentState trace| <= (remaining : Real) * mdp.horizon

Sum of chronological transition innovations for a stage-indexed bounded continuation table.

noncomputable def sampledCumulativeTransitionGapInnovationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> StepTrace Action State remaining -> Real | 0, _, _, _ => 0 | remaining + 1, hremaining, state, trace => let stage : Fin mdp.horizon := ⟨mdp.horizon - (remaining + 1), by omega⟩ mdp.transitionValue (feature stage) state (trace 0).1 - feature stage (trace 0).2 + sampledCumulativeTransitionGapInnovationFrom mdp policy feature remaining (by omega) (trace 0).2 (Fin.tail trace) omit [Nonempty State] [Nonempty Action] in theorem measurable_sampledCumulativeTransitionGapInnovationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (fun p : State × StepTrace Action State remaining => mdp.sampledCumulativeTransitionGapInnovationFrom policy feature remaining hremaining p.1 p.2)

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

theorem measurable_sampledCumulativeTransitionGapInnovationFrom (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (fun p : State × StepTrace Action State remaining => mdp.sampledCumulativeTransitionGapInnovationFrom policy feature remaining hremaining p.1 p.2)

Pathwise envelope matching the sum of `remaining` centered `[0,H]` transition probes.

theorem abs_sampledCumulativeTransitionGapInnovationFrom_le (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) : forall remaining (hremaining : remaining <= mdp.horizon) (currentState : State) (trace : StepTrace Action State remaining), |mdp.sampledCumulativeTransitionGapInnovationFrom policy feature remaining hremaining currentState trace| <= (remaining : Real) * mdp.horizon

One policy transition has the Hoeffding compensated MGF with range `H`.

theorem actionStateKernel_transitionGapInnovation_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : State -> Real) (hfeature : forall nextState, feature nextState ∈ Set.Icc (0 : Real) mdp.horizon) (stage : Fin mdp.horizon) (currentState : State) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun head : Action × State => tilt * (mdp.transitionValue feature currentState head.1 - feature head.2) - tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (policy.actionStateKernel stage currentState)

Recursive within-episode MGF. Each of the `remaining` transitions pays exactly one `tilt^2 H^2 / 8` compensation.

theorem trajectoryKernelRemaining_transitionGapInnovation_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) (tilt : Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (currentState : State) : Concentration.HasMGFUpperBoundAt (fun trace => tilt * mdp.sampledCumulativeTransitionGapInnovationFrom policy feature remaining hremaining currentState trace - (remaining : Real) * tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (policy.trajectoryKernelRemaining remaining hremaining currentState)

Integrating the start state preserves the exact stage-resolved MGF.

theorem trajectoryMeasure_transitionGapInnovation_compensated_hasMGFUpperBoundAt (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun trajectory => tilt * mdp.sampledCumulativeTransitionGapInnovationFrom policy feature mdp.horizon le_rfl trajectory.1 trajectory.2 - (mdp.horizon : Real) * tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (policy.trajectoryMeasure initialState)

Initial state reconstructed from the first record of a one-episode batch. The default branch specifies the degenerate zero-horizon input only.

def reconstructedInitialState {mdp : MDP State Action} (defaultState : State) (batch : EpisodeBatch mdp 1) : State

Action/next-state trace reconstructed from the one-episode records.

def reconstructedStepTrace {mdp : MDP State Action} (batch : EpisodeBatch mdp 1) : StepTrace Action State mdp.horizon

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

theorem measurable_reconstructedInitialState {mdp : MDP State Action} (defaultState : State) : Measurable (reconstructedInitialState (mdp

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

theorem measurable_reconstructedStepTrace {mdp : MDP State Action} : Measurable (reconstructedStepTrace (mdp

Canonical deterministic-table Bellman innovation read from one generated batch. Recorded action fields are intentionally not used.

noncomputable def cumulativeDeterministicGapInnovation {mdp : MDP State Action} (defaultState : State) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) (batch : EpisodeBatch mdp 1) : Real

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

theorem measurable_cumulativeDeterministicGapInnovation {mdp : MDP State Action} (defaultState : State) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) : Measurable (fun batch : EpisodeBatch mdp 1 => batch.cumulativeDeterministicGapInnovation defaultState table feature)

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

theorem cumulativeDeterministicGapInnovation_episodeBatchOfTrajectories (mdp : MDP State Action) (defaultState : State) (table : DeterministicMarkovPolicyTable mdp) (feature : Fin mdp.horizon -> State -> Real) (hhorizon : 0 < mdp.horizon) (trajectories : Fin 1 -> State × StepTrace Action State mdp.horizon) : EpisodeBatch.cumulativeDeterministicGapInnovation defaultState table feature (mdp.episodeBatchOfTrajectories 1 trajectories) = mdp.sampledCumulativeDeterministicGapInnovationFrom table feature mdp.horizon le_rfl (trajectories 0).1 (trajectories 0).2

Stage-resolved Bellman innovation read from one generated batch.

noncomputable def cumulativeTransitionGapInnovation {mdp : MDP State Action} (defaultState : State) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) (batch : EpisodeBatch mdp 1) : Real

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

theorem measurable_cumulativeTransitionGapInnovation {mdp : MDP State Action} (defaultState : State) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) : Measurable (fun batch : EpisodeBatch mdp 1 => batch.cumulativeTransitionGapInnovation defaultState policy feature)

Reconstruction is literal on the batch map used by the generated law.

theorem cumulativeTransitionGapInnovation_episodeBatchOfTrajectories (mdp : MDP State Action) (defaultState : State) (policy : MarkovPolicy mdp) (feature : Fin mdp.horizon -> State -> Real) (hhorizon : 0 < mdp.horizon) (trajectories : Fin 1 -> State × StepTrace Action State mdp.horizon) : EpisodeBatch.cumulativeTransitionGapInnovation defaultState policy feature (mdp.episodeBatchOfTrajectories 1 trajectories) = mdp.sampledCumulativeTransitionGapInnovationFrom policy feature mdp.horizon le_rfl (trajectories 0).1 (trajectories 0).2

The exact one-episode batch image retains the canonical deterministic-table stage-resolved MGF.

theorem iidEpisodeBatchMeasure_one_cumulativeDeterministicGapInnovation_compensated_hasMGFUpperBoundAt {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (hhorizon : 0 < mdp.horizon) (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun batch : EpisodeBatch mdp 1 => tilt * batch.cumulativeDeterministicGapInnovation defaultState table feature - (mdp.horizon : Real) * tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (table.toMarkovPolicy.iidEpisodeBatchMeasure initialState 1)

The exact one-episode batch image retains the stage-resolved MGF.

theorem iidEpisodeBatchMeasure_one_cumulativeTransitionGapInnovation_compensated_hasMGFUpperBoundAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (hhorizon : 0 < mdp.horizon) (feature : Fin mdp.horizon -> State -> Real) (hfeature : forall stage nextState, feature stage nextState ∈ Set.Icc (0 : Real) mdp.horizon) (tilt : Real) : Concentration.HasMGFUpperBoundAt (fun batch : EpisodeBatch mdp 1 => tilt * batch.cumulativeTransitionGapInnovation defaultState policy feature - (mdp.horizon : Real) * tilt ^ 2 * (mdp.horizon : Real) ^ 2 / 8) 1 0 (policy.iidEpisodeBatchMeasure initialState 1)