BanditRLProof.RL.FiniteHorizonExploratoryPathSupportExplicitCalibration

Uniform transition-coordinate radius obtained from one common expected-count floor. The denominator is useful when the count radius is strictly smaller than `episodes * visitFloor`.

noncomputable def uniformFloorTransitionCoordinateRadius (mdp : MDP State Action) (episodes : Nat) (delta visitFloor : Real) : Real

A positive common denominator makes the uniform coordinate radius nonnegative.

theorem uniformFloorTransitionCoordinateRadius_nonneg {mdp : MDP State Action} {episodes : Nat} {delta visitFloor : Real} (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < (episodes : Real) * visitFloor) : 0 <= uniformFloorTransitionCoordinateRadius mdp episodes delta visitFloor

A common expected-count floor bounds every deterministic transition-coordinate radius by the corresponding uniform-denominator radius.

theorem expectedCountTransitionCoordinateRadius_le_uniformFloor {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta visitFloor : Real) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < (episodes : Real) * visitFloor) (hcountFloor : forall coordinate : VisitCoordinate mdp, (episodes : Real) * visitFloor <= coordinate.expectedCount policy initialState episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.expectedCountTransitionCoordinateRadius initialState episodes delta stage state action nextState <= uniformFloorTransitionCoordinateRadius mdp episodes delta visitFloor

One state-action floor shared by every stage and target state on the path certificate.

def ExploratoryPathUniformVisitFloor {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (visitFloor : Real) : Prop

A strict scalar count inequality discharges the full exploratory margin.

theorem ExploratoryPathUniformVisitFloor.exploratoryStateCountMargin {mdp : MDP State Action} {initialState : Measure State} {episodes : Nat} {delta : Real} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < (episodes : Real) * visitFloor) : ExploratoryStateCountMargin mdp episodes delta explorationRate (exploratoryPathStateLower support explorationRate)

Every exploratory table inherits the common expected-count floor.

theorem uniformVisitFloor_expectedCount_le {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (coordinate : VisitCoordinate mdp) : (episodes : Real) * visitFloor <= coordinate.expectedCount (table.exploratoryPolicy explorationRate hexplorationRate) initialState episodes

If the uniform transition coefficient is at most one half, `rewardBound` covers every transition-radius/value-envelope sum when it is used as the transition bonus.

theorem transitionBonusCover_rewardBound_of_uniformExpectedCountFloor {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta visitFloor rewardBound : Real) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < (episodes : Real) * visitFloor) (hcountFloor : forall coordinate : VisitCoordinate mdp, (episodes : Real) * visitFloor <= coordinate.expectedCount policy initialState episodes) (hrewardBound_nonneg : 0 <= rewardBound) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes delta visitFloor * (mdp.horizon : Real) <= 1 / 2) : policy.TransitionBonusCover initialState episodes delta rewardBound rewardBound

The scalar path-support conditions construct the source-wide bonus cover.

theorem exploratorySource_sourceTransitionBonusCover_of_pathSupport_explicitCalibration {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound delta : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < (episodes : Real) * visitFloor) (hrewardBound_nonneg : 0 <= rewardBound) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes (multiBatchLocalDelta rounds delta) visitFloor * (mdp.horizon : Real) <= 1 / 2) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState rewardBound explorationRate hexplorationRate SourceTransitionBonusCover behaviorSource rounds (multiBatchLocalDelta rounds delta) rewardBound rewardBound

Explicit path support and scalar rate conditions construct `SourceCalibration`.

theorem exploratorySource_sourceCalibration_of_pathSupport_explicitCalibration {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound delta : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < (episodes : Real) * visitFloor) (hrewardBound_nonneg : 0 <= rewardBound) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes (multiBatchLocalDelta rounds delta) visitFloor * (mdp.horizon : Real) <= 1 / 2) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState rewardBound explorationRate hexplorationRate SourceCalibration behaviorSource rounds delta rewardBound rewardBound

Route endpoint: path support plus explicit scalar count and half-contraction conditions yield the adaptive global confidence, optimism, and recommended expected-regret theorem with `transitionBonus = rewardBound`.

theorem exploratorySource_trajectoryMeasure_allCoordinateConfidence_optimism_and_recommendedExpectedRegret_of_pathSupport_explicitCalibration {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < (episodes : Real) * visitFloor) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes (multiBatchLocalDelta rounds delta) visitFloor * (mdp.horizon : Real) <= 1 / 2) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState rewardBound explorationRate hexplorationRate let bad := behaviorSource.adaptiveSimultaneousCountBadEvent rounds delta MeasurableSet bad /\ behaviorSource.trajectoryMeasure bad <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ bad -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveEmpiricalOptimisticPlanAt (mdp