BanditRLProof.Algorithms.ETCRealHistoryScore

Number of occurrences of an arm in an inclusive finite pair history.

noncomputable def realHistoryPullCount {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : Nat

Sum of rewards of an arm in an inclusive finite pair history.

noncomputable def realHistorySumRewards {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : Real

Empirical mean of an arm in an inclusive finite pair history.

noncomputable def realHistoryEmpMean {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : Real

Inclusive history pull counts are exclusive trace pull counts at `n + 1`.

theorem realHistoryPullCount_finitePairHistoryOfTrace {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (n : Nat) (arm : Fin K) : ETC.realHistoryPullCount n (History.finitePairHistoryOfTrace action reward n) arm = pullCount action arm (n + 1)

Inclusive history reward sums are exclusive trace sums at `n + 1`.

theorem realHistorySumRewards_finitePairHistoryOfTrace {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (n : Nat) (arm : Fin K) : ETC.realHistorySumRewards n (History.finitePairHistoryOfTrace action reward n) arm = sumRewards action reward arm (n + 1)

The source-shaped history mean is the trace empirical mean at `n + 1`.

theorem realHistoryEmpMean_finitePairHistoryOfTrace {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (n : Nat) (arm : Fin K) : ETC.realHistoryEmpMean n (History.finitePairHistoryOfTrace action reward n) arm = sumRewards action reward arm (n + 1) / (pullCount action arm (n + 1) : Real)

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

private theorem pullCount_eq_of_eq_on_lt {Action : Type} [DecidableEq Action] (action action' : ActionTrace Action) (arm : Action) (n : Nat) (haction : forall t, t < n -> action t = action' t) : pullCount action arm n = pullCount action' arm n

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

private theorem sumRewards_eq_of_action_eq_on_lt {Action Reward : Type} [DecidableEq Action] [AddCommMonoid Reward] (action action' : ActionTrace Action) (reward : RewardTrace Reward) (arm : Action) (n : Nat) (haction : forall t, t < n -> action t = action' t) : sumRewards action reward arm n = sumRewards action' reward arm n

At the exploration boundary, the pinned-source finite-history score equals the native Real exploration score whenever the observed actions are round robin.

theorem realHistoryEmpMean_exploration_eq_realEmpMeanAtExploration {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (hm : 0 < spec.explorationPulls) (hactionExplore : forall t, t < K * spec.explorationPulls -> action t = ETC.exploreArm spec t) (arm : Fin K) : ETC.realHistoryEmpMean (K * spec.explorationPulls - 1) (History.finitePairHistoryOfTrace action reward (K * spec.explorationPulls - 1)) arm = ETC.realEmpMeanAtExploration spec baseCommitArm reward arm

Exact native Real ETC regret from a source-shaped finite-history commit score. The history score is rewritten locally; callers no longer provide a commit law already phrased with `realEmpMeanAtExploration`.

theorem integral_realKernelRegret_externalAction_le_exact_sum_of_actionDependent_actionRewardHistory_condDistrib_of_historyLeastEncodedCommit_persist {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (spec : ETC.Spec K) (nu : ProbabilityTheory.Kernel (Fin K) Real) [ProbabilityTheory.IsMarkovKernel nu] (sigma2 : NNReal) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) (hm : 0 < spec.explorationPulls) (n : Nat) (hn : K * spec.explorationPulls <= n) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (hactionExplore : forall t, t < K * spec.explorationPulls -> Filter.EventuallyEq (ae mu) (fun omega => action omega t) (fun _omega => ETC.exploreArm spec t)) (hactionCommit : Filter.EventuallyEq (ae mu) (fun omega => action omega (K * spec.explorationPulls)) (fun omega => ETC.realLeastEncodedArgmax spec.hK (fun arm => ETC.realHistoryEmpMean (K * spec.explorationPulls - 1) (History.finitePairHistoryOfTrace (action omega) (reward omega) (K * spec.explorationPulls - 1)) arm))) (hactionPersist : forall t, K * spec.explorationPulls <= t -> Filter.EventuallyEq (ae mu) (fun omega => action omega t) (fun omega => action omega (K * spec.explorationPulls))) (hzero : ProbabilityTheory.condDistrib (fun omega => reward omega 0) (fun omega => action omega 0) mu =ᵐ[mu.map (fun omega => action omega 0)] ProbabilityTheory.Kernel.ofFunOfCountable (fun arm : Fin K => nu arm)) (hcond : forall i, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] (RewardKernel.contextIndependentOfActionLaws (Context