BanditRLProof.Algorithms.ETCRealPrefixLawTransport

The reward coordinates read during ETC exploration.

def realExplorationRewardPrefix {K : Nat} (spec : ETC.Spec K) (trajectory : RewardTrace Real) : Fin (spec.explorationPulls * K) -> Real

Extend a finite exploration prefix by zero outside the exploration phase.

def realRewardTraceOfExplorationPrefix {K : Nat} (spec : ETC.Spec K) (rewardPrefix : Fin (spec.explorationPulls * K) -> Real) : RewardTrace Real

Taking the exploration prefix after extension recovers the original prefix.

@[simp] theorem realExplorationRewardPrefix_realRewardTraceOfExplorationPrefix {K : Nat} (spec : ETC.Spec K) (rewardPrefix : Fin (spec.explorationPulls * K) -> Real) : ETC.realExplorationRewardPrefix spec (ETC.realRewardTraceOfExplorationPrefix spec rewardPrefix) = rewardPrefix

Prefix extraction from a Real reward trace is measurable.

theorem measurable_realExplorationRewardPrefix {K : Nat} (spec : ETC.Spec K) : Measurable (ETC.realExplorationRewardPrefix spec)

Zero extension of a finite Real reward prefix is measurable.

theorem measurable_realRewardTraceOfExplorationPrefix {K : Nat} (spec : ETC.Spec K) : Measurable (ETC.realRewardTraceOfExplorationPrefix spec)

Timewise measurable rewards give a measurable finite exploration prefix.

theorem measurable_realExplorationRewardPrefix_comp {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (spec : ETC.Spec K) (reward : Omega -> RewardTrace Real) (hreward : forall t, Measurable (fun omega => reward omega t)) : Measurable (fun omega => ETC.realExplorationRewardPrefix spec (reward omega))

Reward sums agree when the reward traces agree before the horizon.

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

Native Real exploration means depend only on the exploration reward prefix.

theorem realEmpMeanAtExploration_eq_of_eq_on_exploration {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward reward' : RewardTrace Real) (hreward : forall t, t < spec.explorationPulls * K -> reward t = reward' t) (a : Fin K) : ETC.realEmpMeanAtExploration spec baseCommitArm reward a = ETC.realEmpMeanAtExploration spec baseCommitArm reward' a

Native Real empirical argmax commit depends only on exploration rewards.

theorem realExplorationArgmaxCommit_eq_of_eq_on_exploration {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward reward' : RewardTrace Real) (hreward : forall t, t < spec.explorationPulls * K -> reward t = reward' t) : ETC.realExplorationArgmaxCommit spec baseCommitArm reward = ETC.realExplorationArgmaxCommit spec baseCommitArm reward'

Extending the extracted prefix does not change the ETC commit arm.

theorem realExplorationArgmaxCommit_realRewardTraceOf_prefix_eq {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (trajectory : RewardTrace Real) : ETC.realExplorationArgmaxCommit spec baseCommitArm trajectory = ETC.realExplorationArgmaxCommit spec baseCommitArm (ETC.realRewardTraceOfExplorationPrefix spec (ETC.realExplorationRewardPrefix spec trajectory))

Extending the extracted prefix does not change the native Real ETC action.

theorem realExplorationArgmaxAction_realRewardTraceOf_prefix_eq {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (trajectory : RewardTrace Real) : ETC.realExplorationArgmaxAction spec baseCommitArm trajectory = ETC.realExplorationArgmaxAction spec baseCommitArm (ETC.realRewardTraceOfExplorationPrefix spec (ETC.realExplorationRewardPrefix spec trajectory))

Kernel regret is measurable from a timewise measurable finite-arm action.

theorem measurable_realKernelRegret_of_forall_measurable_action {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (nu : ProbabilityTheory.Kernel (Fin K) Real) (action : Omega -> ActionTrace (Fin K)) (haction : forall t, Measurable (fun omega => action omega t)) (n : Nat) : Measurable (fun omega => realKernelRegret nu (action omega) n)

The finite-prefix functional whose value is native Real ETC kernel regret.

noncomputable def realKernelRegretOfExplorationPrefix {K : Nat} (spec : ETC.Spec K) (nu : ProbabilityTheory.Kernel (Fin K) Real) (baseCommitArm : Fin K) (n : Nat) (rewardPrefix : Fin (spec.explorationPulls * K) -> Real) : Real

The finite-prefix kernel-regret functional is measurable.

theorem measurable_realKernelRegretOfExplorationPrefix {K : Nat} (spec : ETC.Spec K) (nu : ProbabilityTheory.Kernel (Fin K) Real) (baseCommitArm : Fin K) (n : Nat) : Measurable (ETC.realKernelRegretOfExplorationPrefix spec nu baseCommitArm n)

Native Real ETC kernel regret factors through the exploration prefix.

theorem realKernelRegret_realExplorationArgmaxAction_eq_prefixFunctional {K : Nat} (spec : ETC.Spec K) (nu : ProbabilityTheory.Kernel (Fin K) Real) (baseCommitArm : Fin K) (trajectory : RewardTrace Real) (n : Nat) : realKernelRegret nu (ETC.realExplorationArgmaxAction spec baseCommitArm trajectory) n = ETC.realKernelRegretOfExplorationPrefix spec nu baseCommitArm n (ETC.realExplorationRewardPrefix spec trajectory)

Kernel regret agrees when two action traces agree before the horizon.

theorem realKernelRegret_eq_of_action_eq_on_lt {K : Nat} (nu : ProbabilityTheory.Kernel (Fin K) Real) (action action' : ActionTrace (Fin K)) (n : Nat) (haction : forall t, t < n -> action t = action' t) : realKernelRegret nu action n = realKernelRegret nu action' n

A constant-kernel Ionescu-Tulcea trajectory is the infinite product law.

theorem real_trajMeasure_const_eq_infinitePi (coordLaw : Nat -> Measure Real) [forall t, IsProbabilityMeasure (coordLaw t)] : ProbabilityTheory.Kernel.trajMeasure (coordLaw 0) (fun i => ProbabilityTheory.Kernel.const ((j : Finset.Iic i) -> Real) (coordLaw (i + 1))) = Measure.infinitePi coordLaw

Convert the inclusive history through `horizon - 1` to a `Fin horizon` prefix.

def realExplorationPrefixOfFiniteRewardHistory {K : Nat} (spec : ETC.Spec K) (history : History.FiniteRewardHistory Real (spec.explorationPulls * K - 1)) : Fin (spec.explorationPulls * K) -> Real

The inclusive-history to `Fin` exploration-prefix conversion is measurable.

theorem measurable_realExplorationPrefixOfFiniteRewardHistory {K : Nat} (spec : ETC.Spec K) : Measurable (ETC.realExplorationPrefixOfFiniteRewardHistory spec)

Conversion of a trace's inclusive history is its `Fin` exploration prefix.

theorem realExplorationPrefixOfFiniteRewardHistory_of_trace {K : Nat} (spec : ETC.Spec K) (trajectory : RewardTrace Real) : ETC.realExplorationPrefixOfFiniteRewardHistory spec (History.finiteRewardHistoryOfTrace trajectory (spec.explorationPulls * K - 1)) = ETC.realExplorationRewardPrefix spec trajectory

Equality of finite exploration-prefix laws transports the canonical native Real ETC exact regret bound to an arbitrary reward process.

theorem integral_realKernelRegret_realExplorationArgmaxAction_le_exact_sum_of_prefixLaw_eq_infinitePi {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) (reward : Omega -> RewardTrace Real) (hreward : forall t, Measurable (fun omega => reward omega t)) (hprefixLaw : Measure.map (fun omega => ETC.realExplorationRewardPrefix spec (reward omega)) mu = Measure.map (ETC.realExplorationRewardPrefix spec) (Measure.infinitePi (fun t : Nat => nu (ETC.exploreArm spec t)))) : let best := ETC.realKernelBestArm spec.hK nu integral mu (fun omega => realKernelRegret nu (ETC.realExplorationArgmaxAction spec best (reward omega)) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => realKernelGap nu arm * ((spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * Real.exp (-(spec.explorationPulls : Real) * (realKernelGap nu arm) ^ 2 / (4 * (sigma2 : Real)))))

External-action version of the finite-prefix law transport theorem. The two remaining upstream obligations are explicit: finite-prefix reward law equality and almost-sure equality with the local native Real ETC action.

theorem integral_realKernelRegret_externalAction_le_exact_sum_of_prefixLaw_eq_infinitePi {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) (hreward : forall t, Measurable (fun omega => reward omega t)) (hprefixLaw : Measure.map (fun omega => ETC.realExplorationRewardPrefix spec (reward omega)) mu = Measure.map (ETC.realExplorationRewardPrefix spec) (Measure.infinitePi (fun t : Nat => nu (ETC.exploreArm spec t)))) (haction : Filter.Eventually (fun omega => forall t, t < n -> action omega t = ETC.realExplorationArgmaxAction spec (ETC.realKernelBestArm spec.hK nu) (reward omega) t) (ae mu)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => realKernelGap nu arm * ((spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * Real.exp (-(spec.explorationPulls : Real) * (realKernelGap nu arm) ^ 2 / (4 * (sigma2 : Real)))))

External native Real exact ETC regret from the scheduled exploration-arm initial marginal and successor conditional reward laws. This is the direct law surface needed before mapping an upstream `IsAlgEnvSeq` witness.

theorem integral_realKernelRegret_externalAction_le_exact_sum_of_initial_map_eq_condDistrib {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) (hreward : forall t, Measurable (fun omega => reward omega t)) (hzero : Measure.map (fun omega => reward omega 0) mu = nu (ETC.exploreArm spec 0)) (hcond : forall i, i < spec.explorationPulls * K - 1 -> ProbabilityTheory.condDistrib (fun omega => reward omega (i + 1)) (fun omega => History.finiteRewardHistoryOfTrace (reward omega) i) mu =ᵐ[mu.map (fun omega => History.finiteRewardHistoryOfTrace (reward omega) i)] ProbabilityTheory.Kernel.const (History.FiniteRewardHistory Real i) (nu (ETC.exploreArm spec (i + 1)))) (haction : Filter.Eventually (fun omega => forall t, t < n -> action omega t = ETC.realExplorationArgmaxAction spec (ETC.realKernelBestArm spec.hK nu) (reward omega) t) (ae mu)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => realKernelGap nu arm * ((spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * Real.exp (-(spec.explorationPulls : Real) * (realKernelGap nu arm) ^ 2 / (4 * (sigma2 : Real)))))