BanditRLProof.Algorithms.UCBArmStreamExpectedPullCount

During initialization the recursive process follows round robin exactly.

theorem armStreamAction_eq_initializationArm_of_lt {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (t : Nat) (ht : t < K) : armStreamAction hK c stream t = initializationArm hK t

Every arm is pulled exactly once in the first full initialization cycle.

theorem pullCount_armStreamAction_K_eq_one {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (arm : Fin K) : pullCount (armStreamAction hK c stream) arm K = 1

After initialization every arm has positive prior pull count.

theorem pullCount_armStreamAction_pos_of_K_le {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (arm : Fin K) (t : Nat) (ht : K <= t) : 0 < pullCount (armStreamAction hK c stream) arm t

A second pull cannot occur before the round-robin cycle is complete.

theorem K_lt_of_one_lt_pullCount_armStreamAction {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (arm : Fin K) (t : Nat) (hcount : 1 < pullCount (armStreamAction hK c stream) arm t) : K < t

After initialization the recursive action is the native trace UCB argmax.

theorem armStreamAction_eq_realIndexAction_of_K_le {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (t : Nat) (ht : K <= t) : armStreamAction hK c stream t = realIndexAction hK (armStreamAction hK c stream) (armStreamReward hK c stream) c t

The selected recursive action maximizes the actual random-width index.

theorem realIndex_le_realIndex_armStreamAction_of_K_le {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (t : Nat) (ht : K <= t) (arm : Fin K) : realIndex (armStreamAction hK c stream) (armStreamReward hK c stream) c arm t <= realIndex (armStreamAction hK c stream) (armStreamReward hK c stream) c (armStreamAction hK c stream t) t

Good confidence inequalities force the selected arm gap below twice its width.

theorem meanGap_le_two_realWidth_of_selected {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (t : Nat) (ht : K <= t) (trueMean : Fin K -> Real) (best chosen : Fin K) (hselected : armStreamAction hK c stream t = chosen) (hbest : trueMean best <= realEmpiricalMean (armStreamAction hK c stream) (armStreamReward hK c stream) best t + realWidth (armStreamAction hK c stream) c best t) (hchosen : realEmpiricalMean (armStreamAction hK c stream) (armStreamReward hK c stream) chosen t - realWidth (armStreamAction hK c stream) c chosen t <= trueMean chosen) : meanGap trueMean best chosen <= 2 * realWidth (armStreamAction hK c stream) c chosen t

Squaring the good-event gap inequality gives the standard UCB count bound.

theorem pullCount_le_eight_scale_log_div_gap_sq {K : Nat} (action : ActionTrace (Fin K)) (arm : Fin K) (scale gap : Real) (t : Nat) (hscale : 0 <= scale) (hgap : 0 < gap) (hcount : 0 < pullCount action arm t) (hgap_le : gap <= 2 * realWidth action scale arm t) : (pullCount action arm t : Real) <= 8 * scale * Real.log ((t + 1 : Nat) : Real) / gap ^ 2

Real threshold used for the horizon-wide pull-count split.

noncomputable def realPullThreshold (c : Real) (sigma2 : NNReal) (gap : Real) (n : Nat) : Real

Integer split point: one more than the ceiling of the real threshold.

noncomputable def pullThreshold (c : Real) (sigma2 : NNReal) (gap : Real) (n : Nat) : Nat

The one-sided inverse-power tail budget at time `t`.

noncomputable def indexTail (c : Real) (t : Nat) : ENNReal

Finite-horizon sum of the source-faithful one-sided index tails.

noncomputable def constSum (c : Real) (n : Nat) : ENNReal

A selected arm whose prior count has crossed the horizon threshold.

noncomputable def selectedLargePullCountEvent {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (gap : Real) (arm : Fin K) (n t : Nat) : Set (ArmRewardStream K)

Lower-index failure for a fixed arm of the recursive process.

noncomputable def lowerIndexFailure {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (arm : Fin K) (mean : Real) (t : Nat) : Set (ArmRewardStream K)

Upper-index failure for a fixed arm of the recursive process.

noncomputable def upperIndexFailure {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (arm : Fin K) (mean : Real) (t : Nat) : Set (ArmRewardStream K)

Crossing the horizon count threshold while selecting a positive-gap arm forces one of the two one-sided index failures used by the arm-stream tail module.

theorem selectedLargePullCountEvent_subset_lower_union_upper {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) (arm : Fin K) (n t : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hgap : 0 < realKernelGap nu arm) (ht : t < n) : selectedLargePullCountEvent hK c sigma2 (realKernelGap nu arm) arm n t ⊆ lowerIndexFailure hK c sigma2 (ETC.realKernelBestArm hK nu) (realKernelMean nu (ETC.realKernelBestArm hK nu)) t ∪ upperIndexFailure hK c sigma2 arm (realKernelMean nu arm) t

The selected-large event has twice the one-sided inverse-power budget.

theorem measure_selectedLargePullCountEvent_le_two_mul_indexTail {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (n t : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hgap : 0 < realKernelGap nu arm) (ht : t < n) (hsubGBest : HasSubgaussianMGF (fun reward => reward - realKernelMean nu (ETC.realKernelBestArm hK nu)) sigma2 (nu (ETC.realKernelBestArm hK nu))) (hsubGArm : HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : armStreamMeasure nu (selectedLargePullCountEvent hK c sigma2 (realKernelGap nu arm) arm n t) <= 2 * indexTail c t

Finite-time selected-large indicators integrate to twice `constSum`.

theorem lintegral_selectedLargePullCount_indicator_sum_le_two_mul_constSum {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hgap : 0 < realKernelGap nu arm) (hsubGBest : HasSubgaussianMGF (fun reward => reward - realKernelMean nu (ETC.realKernelBestArm hK nu)) sigma2 (nu (ETC.realKernelBestArm hK nu))) (hsubGArm : HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : ∫⁻ stream : ArmRewardStream K, (Finset.range n).sum (fun t : Nat => if armStreamAction hK (c * (sigma2 : Real)) stream t = arm ∧ pullThreshold c sigma2 (realKernelGap nu arm) n <= pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm t then (1 : ENNReal) else 0) ∂armStreamMeasure nu <= 2 * constSum c n

ENNReal expected pull-count bound for one positive-gap arm of the concrete recursive UCB process.

theorem lintegral_natCast_pullCount_armStreamAction_le_threshold_add_two_mul_constSum {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hgap : 0 < realKernelGap nu arm) (hsubGBest : HasSubgaussianMGF (fun reward => reward - realKernelMean nu (ETC.realKernelBestArm hK nu)) sigma2 (nu (ETC.realKernelBestArm hK nu))) (hsubGArm : HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : ∫⁻ stream : ArmRewardStream K, (pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n : ENNReal) ∂armStreamMeasure nu <= (pullThreshold c sigma2 (realKernelGap nu arm) n : ENNReal) + 2 * constSum c n

Every finite inverse-power tail budget is finite.

theorem indexTail_ne_top (c : Real) (t : Nat) : indexTail c t ≠ ∞

The finite-horizon inverse-power tail sum is finite.

theorem constSum_ne_top (c : Real) (n : Nat) : constSum c n ≠ ∞

Real pull counts of the measurable recursive process are integrable.

theorem integrable_real_pullCount_armStreamAction {K : Nat} (hK : 0 < K) (c : Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (n : Nat) : Integrable (fun stream : ArmRewardStream K => (pullCount (armStreamAction hK c stream) arm n : Real)) (armStreamMeasure nu)

Real Bochner expected pull-count bound obtained from the ENNReal endpoint.

theorem integral_real_pullCount_armStreamAction_le_threshold_add_two_mul_constSum {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hgap : 0 < realKernelGap nu arm) (hsubGBest : HasSubgaussianMGF (fun reward => reward - realKernelMean nu (ETC.realKernelBestArm hK nu)) sigma2 (nu (ETC.realKernelBestArm hK nu))) (hsubGArm : HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : ∫ stream : ArmRewardStream K, (pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n : Real) ∂armStreamMeasure nu <= (pullThreshold c sigma2 (realKernelGap nu arm) n : Real) + 2 * (constSum c n).toReal

The ceiling threshold is bounded by the exact LML real threshold plus two.

theorem pullThreshold_cast_le_realPullThreshold_add_two (c : Real) (sigma2 : NNReal) (gap : Real) (n : Nat) (hthreshold : 0 <= realPullThreshold c sigma2 gap n) : (pullThreshold c sigma2 gap n : Real) <= realPullThreshold c sigma2 gap n + 2

LML-shaped Real expected pull-count bound without a ceiling term.

theorem integral_real_pullCount_armStreamAction_le_realThreshold_add_two_add_two_mul_constSum {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hgap : 0 < realKernelGap nu arm) (hsubGBest : HasSubgaussianMGF (fun reward => reward - realKernelMean nu (ETC.realKernelBestArm hK nu)) sigma2 (nu (ETC.realKernelBestArm hK nu))) (hsubGArm : HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : ∫ stream : ArmRewardStream K, (pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n : Real) ∂armStreamMeasure nu <= realPullThreshold c sigma2 (realKernelGap nu arm) n + 2 + 2 * (constSum c n).toReal

Finite-arm expected regret bound for the concrete recursive arm-stream UCB process, in the same gap-weighted shape as the pinned LML route.

theorem integral_realKernelRegret_armStreamAction_le_sum_gap_mul_realThreshold_add_two_add_two_mul_constSum {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : ∫ stream : ArmRewardStream K, realKernelRegret nu (armStreamAction hK (c * (sigma2 : Real)) stream) n ∂armStreamMeasure nu <= (Finset.univ : Finset (Fin K)).sum (fun arm => realKernelGap nu arm * (realPullThreshold c sigma2 (realKernelGap nu arm) n + 2 + 2 * (constSum c n).toReal))

Canonical arm-stream specialization of the pinned LML UCB regret theorem, with exactly the upstream gap-weighted finite-sum right-hand side.

theorem integral_realKernelRegret_armStreamAction_le_lml_sum {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : ∫ stream : ArmRewardStream K, realKernelRegret nu (armStreamAction hK (c * (sigma2 : Real)) stream) n ∂armStreamMeasure nu <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))

The complete recursive arm-stream action trace is measurable.

theorem measurable_armStreamActionTrace {K : Nat} (hK : 0 < K) (c : Real) : Measurable (armStreamAction hK c : ArmRewardStream K -> ActionTrace (Fin K))

Kernel regret is a measurable functional of a finite-arm action trace.

theorem measurable_realKernelRegret_actionTrace {K : Nat} (nu : Kernel (Fin K) Real) (n : Nat) : Measurable (fun action : ActionTrace (Fin K) => realKernelRegret nu action n)

Any external action process with the same complete action-trace law as the canonical arm-stream UCB process inherits its exact LML-shaped regret bound.

theorem integral_realKernelRegret_externalAction_le_lml_sum_of_identDistrib_armStreamAction {Omega : Type*} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (hident : IdentDistrib action (armStreamAction hK (c * (sigma2 : Real))) mu (armStreamMeasure nu)) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))

An external action generated almost surely by the recursive UCB map inherits the canonical action-trace law from an identically distributed latent arm stream.

theorem identDistrib_action_armStreamAction_of_identDistrib_armStream {Omega : Type*} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (c : Real) (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (armStream : Omega -> ArmRewardStream K) (action : Omega -> ActionTrace (Fin K)) (hstreamLaw : IdentDistrib armStream (id : ArmRewardStream K -> ArmRewardStream K) mu (armStreamMeasure nu)) (haction : ∀ᵐ omega ∂mu, action omega = armStreamAction hK c (armStream omega)) : IdentDistrib action (armStreamAction hK c) mu (armStreamMeasure nu)

Exact LML-shaped regret for an external action generated from a latent arm stream with the canonical complete stream law.

theorem integral_realKernelRegret_externalAction_le_lml_sum_of_identDistrib_armStream {Omega : Type*} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (armStream : Omega -> ArmRewardStream K) (action : Omega -> ActionTrace (Fin K)) (hstreamLaw : IdentDistrib armStream (id : ArmRewardStream K -> ArmRewardStream K) mu (armStreamMeasure nu)) (haction : ∀ᵐ omega ∂mu, action omega = armStreamAction hK (c * (sigma2 : Real)) (armStream omega)) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))

Identical laws of complete action/reward trajectories imply identical laws of their action traces. This is the projection used by LML's `IsAlgEnvSeq.identDistrib_trajectory` route.

theorem identDistrib_action_of_identDistrib_actionRewardTrace {Omega Xi : Type*} [MeasurableSpace Omega] [MeasurableSpace Xi] {K : Nat} (mu : Measure Omega) (mu' : Measure Xi) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (action' : Xi -> ActionTrace (Fin K)) (reward' : Xi -> RewardTrace Real) (htrajectory : IdentDistrib (fun omega t => (action omega t, reward omega t)) (fun xi t => (action' xi t, reward' xi t)) mu mu') : IdentDistrib action action' mu mu'

Exact LML-shaped regret transported from an observable action/reward trajectory law matching the canonical recursive arm-stream UCB trajectory.

theorem integral_realKernelRegret_externalAction_le_lml_sum_of_identDistrib_actionRewardTrace {Omega : Type*} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (htrajectory : IdentDistrib (fun omega t => (action omega t, reward omega t)) (fun stream t => (armStreamAction hK (c * (sigma2 : Real)) stream t, armStreamReward hK (c * (sigma2 : Real)) stream t)) mu (armStreamMeasure nu)) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun x => x - realKernelMean nu arm) sigma2 (nu arm)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))

Exact LML-shaped regret from upstream-style initial and successor action/reward conditional laws. The external process and the canonical arm-stream UCB process need only share the same initial pair marginal and the same history-indexed successor pair kernels; full trajectory `IdentDistrib` is then supplied by Ionescu-Tulcea/projective-limit uniqueness.

theorem integral_realKernelRegret_externalAction_le_lml_sum_of_common_actionReward_condDistrib {Omega : Type*} [MeasurableSpace Omega] {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) [IsFiniteMeasure mu] (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (mu0 : Measure (Fin K × Real)) [IsProbabilityMeasure mu0] (pairKernel : (i : Nat) -> Kernel (History.FinitePairHistory (Fin K) Real i) (Fin K × Real)) [forall i, IsMarkovKernel (pairKernel i)] (hzero : Measure.map (fun omega : Omega => (action omega 0, reward omega 0)) mu = mu0) (hzeroCanonical : Measure.map (fun stream : ArmRewardStream K => (armStreamAction hK (c * (sigma2 : Real)) stream 0, armStreamReward hK (c * (sigma2 : Real)) stream 0)) (armStreamMeasure nu) = mu0) (hcond : forall i : Nat, condDistrib (fun omega : Omega => (action omega (i + 1), reward omega (i + 1))) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu =ᵐ[mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)] pairKernel i) (hcondCanonical : forall i : Nat, condDistrib (fun stream : ArmRewardStream K => (armStreamAction hK (c * (sigma2 : Real)) stream (i + 1), armStreamReward hK (c * (sigma2 : Real)) stream (i + 1))) (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i) (armStreamMeasure nu) =ᵐ[(armStreamMeasure nu).map (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i)] pairKernel i) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun x => x - realKernelMean nu arm) sigma2 (nu arm)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))

An external action/reward process has the same complete observable trajectory law as canonical arm-stream UCB when its initial pair marginal and every successor pair conditional distribution agree with the corresponding canonical ones. The canonical initial measure and kernel family are chosen internally.

theorem identDistrib_actionRewardTrace_of_condDistrib_eq_armStream {Omega : Type*} [MeasurableSpace Omega] {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) [IsFiniteMeasure mu] (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hzero : Measure.map (fun omega : Omega => (action omega 0, reward omega 0)) mu = Measure.map (fun stream : ArmRewardStream K => (armStreamAction hK (c * (sigma2 : Real)) stream 0, armStreamReward hK (c * (sigma2 : Real)) stream 0)) (armStreamMeasure nu)) (hcond : forall i : Nat, condDistrib (fun omega : Omega => (action omega (i + 1), reward omega (i + 1))) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu =ᵐ[mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)] condDistrib (fun stream : ArmRewardStream K => (armStreamAction hK (c * (sigma2 : Real)) stream (i + 1), armStreamReward hK (c * (sigma2 : Real)) stream (i + 1))) (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i) (armStreamMeasure nu)) : IdentDistrib (fun omega t => (action omega t, reward omega t)) (fun stream t => (armStreamAction hK (c * (sigma2 : Real)) stream t, armStreamReward hK (c * (sigma2 : Real)) stream t)) mu (armStreamMeasure nu)

An external process has the canonical observable UCB trajectory law from the four split law surfaces used by LML's `IsAlgEnvSeq`: the initial action law, the initial feedback law given that action, the successor action law given finite pair history, and the successor feedback law given history and the next action. The canonical split kernels and their `compProd` pair kernels are chosen internally.

theorem identDistrib_actionRewardTrace_of_split_condDistrib_eq_armStream {Omega : Type*} [MeasurableSpace Omega] {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) [IsFiniteMeasure mu] (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hzeroAction : Measure.map (fun omega : Omega => action omega 0) mu = Measure.map (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream 0) (armStreamMeasure nu)) (hzeroFeedback : condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] condDistrib (fun stream : ArmRewardStream K => armStreamReward hK (c * (sigma2 : Real)) stream 0) (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream 0) (armStreamMeasure nu)) (hcondAction : forall i : Nat, condDistrib (fun omega : Omega => action omega (i + 1)) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu =ᵐ[ mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)] condDistrib (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream (i + 1)) (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i) (armStreamMeasure nu)) (hcondFeedback : forall i : Nat, condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1))) mu =ᵐ[ mu.map (fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)))] condDistrib (fun stream : ArmRewardStream K => armStreamReward hK (c * (sigma2 : Real)) stream (i + 1)) (fun stream : ArmRewardStream K => (History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i, armStreamAction hK (c * (sigma2 : Real)) stream (i + 1))) (armStreamMeasure nu)) : IdentDistrib (fun omega t => (action omega t, reward omega t)) (fun stream t => (armStreamAction hK (c * (sigma2 : Real)) stream t, armStreamReward hK (c * (sigma2 : Real)) stream t)) mu (armStreamMeasure nu)

Exact canonical arm-stream UCB regret from the four split action/feedback law fields corresponding to LML's `IsAlgEnvSeq` interface.

theorem integral_realKernelRegret_externalAction_le_lml_sum_of_split_condDistrib_eq_armStream {Omega : Type*} [MeasurableSpace Omega] {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) [IsFiniteMeasure mu] (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hzeroAction : Measure.map (fun omega : Omega => action omega 0) mu = Measure.map (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream 0) (armStreamMeasure nu)) (hzeroFeedback : condDistrib (fun omega : Omega => reward omega 0) (fun omega : Omega => action omega 0) mu =ᵐ[ mu.map (fun omega : Omega => action omega 0)] condDistrib (fun stream : ArmRewardStream K => armStreamReward hK (c * (sigma2 : Real)) stream 0) (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream 0) (armStreamMeasure nu)) (hcondAction : forall i : Nat, condDistrib (fun omega : Omega => action omega (i + 1)) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu =ᵐ[ mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)] condDistrib (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream (i + 1)) (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i) (armStreamMeasure nu)) (hcondFeedback : forall i : Nat, condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1))) mu =ᵐ[ mu.map (fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)))] condDistrib (fun stream : ArmRewardStream K => armStreamReward hK (c * (sigma2 : Real)) stream (i + 1)) (fun stream : ArmRewardStream K => (History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i, armStreamAction hK (c * (sigma2 : Real)) stream (i + 1))) (armStreamMeasure nu)) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun x => x - realKernelMean nu arm) sigma2 (nu arm)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))

Exact LML-shaped regret when the external initial and successor observable pair laws agree directly with canonical arm-stream UCB.

theorem integral_realKernelRegret_externalAction_le_lml_sum_of_condDistrib_eq_armStream {Omega : Type*} [MeasurableSpace Omega] {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (mu : Measure Omega) [IsFiniteMeasure mu] (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hzero : Measure.map (fun omega : Omega => (action omega 0, reward omega 0)) mu = Measure.map (fun stream : ArmRewardStream K => (armStreamAction hK (c * (sigma2 : Real)) stream 0, armStreamReward hK (c * (sigma2 : Real)) stream 0)) (armStreamMeasure nu)) (hcond : forall i : Nat, condDistrib (fun omega : Omega => (action omega (i + 1), reward omega (i + 1))) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu =ᵐ[mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)] condDistrib (fun stream : ArmRewardStream K => (armStreamAction hK (c * (sigma2 : Real)) stream (i + 1), armStreamReward hK (c * (sigma2 : Real)) stream (i + 1))) (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) i) (armStreamMeasure nu)) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun x => x - realKernelMean nu arm) sigma2 (nu arm)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))