Lean module · ETC
BanditRLProof.Algorithms.ETCRatArmLawRealKernel
# Rat arm-law transport to the Real ETC kernel regret surface This module pushes the existing `Rat` arm laws forward along the cast to `Real`, identifies the resulting identity-integral kernel means and gaps, and then assembles the canonical exact per-arm ETC pull-count bounds into the LML-shaped finite sum for Real kernel regret. The result is still tied to the canonical generated `Rat` reward history. It does not transport an arbitrary native `Real` `IsAlgEnvSeq` process or identify the local fold argmax with upstream `measurableArgmax` tie semantics.
Module map
Imports
BanditRLProof.Algorithms.ETCExactSubGaussianTail, BanditRLProof.RealKernelRegretPullCount
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.ETC.ratArmLawRealKernel
Compiled
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
theorem
BanditRLProof.ETC.ratArmLawRealKernel_apply
Compiled
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)
theorem
BanditRLProof.ETC.isMarkovKernel_ratArmLawRealKernel
Compiled
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)
theorem
BanditRLProof.ETC.realKernelMean_ratArmLawRealKernel_eq_integral_cast
Compiled
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))
theorem
BanditRLProof.ETC.realKernelMean_ratArmLawRealKernel_eq_modelMean
Compiled
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)
theorem
BanditRLProof.ETC.ciSup_modelMean_cast_eq_bestArm
Compiled
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)
theorem
BanditRLProof.ETC.realKernelGap_ratArmLawRealKernel_eq_modelGap
Compiled
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)
theorem
BanditRLProof.ETC.integral_realKernelRegret_explorationArgmaxAction_le_exact_sum_of_armLaws
Compiled
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