BanditRLProof.Algorithms.ETCRatArmLawRealKernel

Push each countable `Rat` arm law forward to a Real-valued arm kernel.

noncomputable def ratArmLawRealKernel {K : Nat} (armLaw : Fin K -> Measure Rat) : ProbabilityTheory.Kernel (Fin K) Real

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

theorem ratArmLawRealKernel_apply {K : Nat} (armLaw : Fin K -> Measure Rat) (arm : Fin K) : ratArmLawRealKernel armLaw arm = Measure.map (fun reward : Rat => ((reward : Rat) : Real)) (armLaw arm)

Probability arm laws give a Markov Real pushforward kernel.

theorem isMarkovKernel_ratArmLawRealKernel {K : Nat} (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) : ProbabilityTheory.IsMarkovKernel (ratArmLawRealKernel armLaw)

The pushforward kernel identity integral is the original casted mean.

theorem realKernelMean_ratArmLawRealKernel_eq_integral_cast {K : Nat} (armLaw : Fin K -> Measure Rat) (arm : Fin K) : realKernelMean (ratArmLawRealKernel armLaw) arm = integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real))

Exact arm means identify the pushforward Real kernel mean with the model mean.

theorem realKernelMean_ratArmLawRealKernel_eq_modelMean {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (arm : Fin K) : realKernelMean (ratArmLawRealKernel armLaw) arm = ((model.mean arm : Rat) : Real)

The supremum of the cast model means is attained at the local best arm.

theorem ciSup_modelMean_cast_eq_bestArm {K : Nat} (model : FiniteBanditModel K) : (⨆ arm : Fin K, ((model.mean arm : Rat) : Real)) = ((model.mean model.bestArm : Rat) : Real)

The pushforward Real kernel gap is exactly the cast local model gap.

theorem realKernelGap_ratArmLawRealKernel_eq_modelGap {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (arm : Fin K) : realKernelGap (ratArmLawRealKernel armLaw) arm = ((model.gap arm : Rat) : Real)

Canonical exact ETC expected regret against the Real pushforward arm kernel. This is the finite-arm assembly of the exact per-arm expected pull-count leaf: the best-arm summand vanishes, while each non-best summand uses the exact `exp (-m * gap^2 / (4 * sigma2))` count bound.

theorem integral_realKernelRegret_explorationArgmaxAction_le_exact_sum_of_armLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - ((model.mean arm : Rat) : Real)) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (n : Nat) (hn : K * spec.explorationPulls <= n) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context := Context) armLaw hprob let policy := fun t => ETC.explorationArgmaxHistoryPolicy spec model t let state := fun t history => ETC.explorationArgmaxHistoryState t history let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext (fun t => ETC.measurable_explorationArgmaxHistoryState t) let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) (armLaw defaultAction) stepKernel integral trajMeasure (fun trajectory : RewardTrace Rat => realKernelRegret (ratArmLawRealKernel armLaw) (ETC.explorationArgmaxAction spec model trajectory) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => ((model.gap arm : Rat) : Real) * ((spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * Real.exp (-(spec.explorationPulls : Real) * ((model.gap arm : Rat) : Real) ^ 2 / (4 * (sigma2 : Real)))))