BanditRLProof.Algorithms.ETCRealInfinitePiTail

A finite maximizer of the identity-integral means of a Real reward kernel.

noncomputable def realKernelBestArm {K : Nat} (hK : 0 < K) (nu : ProbabilityTheory.Kernel (Fin K) Real) : Fin K

The selected kernel best arm dominates every arm mean.

theorem realKernelMean_le_realKernelBestArm {K : Nat} (hK : 0 < K) (nu : ProbabilityTheory.Kernel (Fin K) Real) (a : Fin K) : realKernelMean nu a <= realKernelMean nu (ETC.realKernelBestArm hK nu)

The finite supremum of kernel means is attained at `realKernelBestArm`.

theorem ciSup_realKernelMean_eq_realKernelBestArm {K : Nat} (hK : 0 < K) (nu : ProbabilityTheory.Kernel (Fin K) Real) : (⨆ a : Fin K, realKernelMean nu a) = realKernelMean nu (ETC.realKernelBestArm hK nu)

Kernel gap is the selected best mean minus the queried arm mean.

theorem realKernelGap_eq_realKernelBestArm_sub {K : Nat} (hK : 0 < K) (nu : ProbabilityTheory.Kernel (Fin K) Real) (a : Fin K) : realKernelGap nu a = realKernelMean nu (ETC.realKernelBestArm hK nu) - realKernelMean nu a

Native Real centered candidate-minus-best reward difference.

noncomputable def realCenteredPairwiseRewardDiff {Omega : Type u} {K : Nat} (spec : ETC.Spec K) (mean : Fin K -> Real) (best commitArm : Fin K) (reward : Omega -> RewardTrace Real) (a : Fin K) (t : Nat) (omega : Omega) : Real

Native Real threshold of the centered pairwise exploration event.

noncomputable def realCenteredPairwiseGapThreshold {K : Nat} (spec : ETC.Spec K) (mean : Fin K -> Real) (best a : Fin K) : Real

Variance proxy charged at candidate and best-arm exploration coordinates.

noncomputable def realCenteredPairwiseRewardDiffVarianceProxy {K : Nat} (spec : ETC.Spec K) (best commitArm : Fin K) (cReward : Fin K -> Nat -> NNReal) (a : Fin K) (t : Nat) : NNReal

Selected centered Real rewards equal reward sum minus count times mean.

theorem real_selectedSubMean_sum_eq_sumRewards_sub_pullCount_mul {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Real) (a : Action) (n : Nat) (mu : Real) : (Finset.range n).sum (fun t => if action t = a then reward t - mu else 0) = sumRewards action reward a n - (pullCount action a n : Real) * mu

Selected negative centered Real rewards equal count times mean minus sum.

theorem real_meanSubSelected_sum_eq_pullCount_mul_sub_sumRewards {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Real) (a : Action) (n : Nat) (mu : Real) : (Finset.range n).sum (fun t => if action t = a then mu - reward t else 0) = (pullCount action a n : Real) * mu - sumRewards action reward a n

Equal exploration counts turn a raw reward comparison into a centered sum.

theorem real_sumRewards_le_imp_centered_pairwise_sum_ge {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Real) (a b : Action) (n m : Nat) (muA muB : Real) (hcount_a : pullCount action a n = m) (hcount_b : pullCount action b n = m) (hraw : sumRewards action reward b n <= sumRewards action reward a n) : (m : Real) * (muB - muA) <= (Finset.range n).sum (fun t => (if action t = a then reward t - muA else 0) + (if action t = b then muB - reward t else 0))

A native Real commit fiber is contained in its centered pairwise tail event.

theorem realExplorationArgmaxCommit_eq_arm_event_subset_centeredPairwise_sum_event {Omega : Type u} {K : Nat} (spec : ETC.Spec K) (mean : Fin K -> Real) (best baseCommitArm : Fin K) (reward : Omega -> RewardTrace Real) (a : Fin K) (hm : 0 < spec.explorationPulls) : Set.Subset {omega | ETC.realExplorationArgmaxCommit spec baseCommitArm (reward omega) = a} {omega | ETC.realCenteredPairwiseGapThreshold spec mean best a <= (Finset.range (spec.explorationPulls * K)).sum (fun t => ETC.realCenteredPairwiseRewardDiff spec mean best baseCommitArm reward a t omega)}

Coordinate independence survives the native Real pairwise transform.

theorem iIndepFun_realCenteredPairwiseRewardDiff_of_iIndepFun_reward {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (spec : ETC.Spec K) (mean : Fin K -> Real) (best commitArm : Fin K) (reward : Omega -> RewardTrace Real) (h_reward_indep : ProbabilityTheory.iIndepFun (fun t omega => reward omega t) mu) (a : Fin K) : ProbabilityTheory.iIndepFun (fun t omega => ETC.realCenteredPairwiseRewardDiff spec mean best commitArm reward a t omega) mu

Per-coordinate centered sub-Gaussianity transfers to the pairwise summand.

theorem realCenteredPairwiseRewardDiff_hasSubgaussianMGF_of_centeredReward {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsZeroOrProbabilityMeasure mu] (spec : ETC.Spec K) (mean : Fin K -> Real) (best commitArm : Fin K) (reward : Omega -> RewardTrace Real) (cReward : Fin K -> Nat -> NNReal) (a : Fin K) (t : Nat) (hne : a ≠ best) (h_subG : forall b, ETC.actionWithCommit spec commitArm t = b -> ProbabilityTheory.HasSubgaussianMGF (fun omega => reward omega t - mean b) (cReward b t) mu) : ProbabilityTheory.HasSubgaussianMGF (fun omega => ETC.realCenteredPairwiseRewardDiff spec mean best commitArm reward a t omega) (ETC.realCenteredPairwiseRewardDiffVarianceProxy spec best commitArm cReward a t) mu

The constant pairwise proxy sums to exactly `2 * m * sigma2`.

theorem sum_realCenteredPairwiseRewardDiffVarianceProxy_const_eq_two_mul {K : Nat} (spec : ETC.Spec K) (best : Fin K) (sigma2 : NNReal) (a : Fin K) (hne : a ≠ best) : (Finset.range (spec.explorationPulls * K)).sum (fun t => ETC.realCenteredPairwiseRewardDiffVarianceProxy spec best best (fun _ _ => sigma2) a t) = (2 : NNReal) * (spec.explorationPulls : NNReal) * sigma2

Exact native Real single-arm wrong-commit tail under action-matched independent kernel coordinates.

theorem real_measure_realExplorationArgmaxCommit_eq_arm_le_exp_of_infinitePi_kernel {K : Nat} (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) (a : Fin K) (hne : a ≠ ETC.realKernelBestArm spec.hK nu) : let best := ETC.realKernelBestArm spec.hK nu let coordLaw := fun t : Nat => nu (ETC.exploreArm spec t) (Measure.infinitePi coordLaw).real {trajectory : RewardTrace Real | ETC.realExplorationArgmaxCommit spec best trajectory = a} <= Real.exp (-(spec.explorationPulls : Real) * (realKernelGap nu a) ^ 2 / (4 * (sigma2 : Real)))

Exact native Real per-arm expected pull-count bound under `infinitePi`.

theorem integral_real_pullCount_realExplorationArgmaxAction_le_exp_of_infinitePi_kernel {K : Nat} (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) (a : Fin K) (n : Nat) (hn : K * spec.explorationPulls <= n) (hne : a ≠ ETC.realKernelBestArm spec.hK nu) : let best := ETC.realKernelBestArm spec.hK nu let coordLaw := fun t : Nat => nu (ETC.exploreArm spec t) integral (Measure.infinitePi coordLaw) (fun trajectory : RewardTrace Real => (pullCount (ETC.realExplorationArgmaxAction spec best trajectory) a n : Real)) <= (spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * Real.exp (-(spec.explorationPulls : Real) * (realKernelGap nu a) ^ 2 / (4 * (sigma2 : Real)))

Exact LML-shaped finite-sum native Real kernel regret bound under the canonical independent exploration-coordinate law.

theorem integral_realKernelRegret_realExplorationArgmaxAction_le_exact_sum_of_infinitePi_kernel {K : Nat} (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) : let best := ETC.realKernelBestArm spec.hK nu let coordLaw := fun t : Nat => nu (ETC.exploreArm spec t) integral (Measure.infinitePi coordLaw) (fun trajectory : RewardTrace Real => realKernelRegret nu (ETC.realExplorationArgmaxAction spec best trajectory) 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)))))