Lean module · ETC
BanditRLProof.Algorithms.ETCRealSourceAdapter
# Native Real ETC source-law adapter This module converts the action-selected feedback-law fields exposed by an algorithm/environment sequence into the reward-only scheduled laws consumed by the native Real exact ETC regret theorem. It does not import LML: the theorem statement mirrors the relevant `IsAlgEnvSeq` fields so the remaining upstream wrapper is limited to source-name and action/tie alignment.
Module map
Imports
BanditRLProof.Algorithms.ETCRealPrefixLawTransport
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ETC.integral_realKernelRegret_externalAction_le_exact_sum_of_actionDependent_actionRewardHistory_condDistrib
Compiled
External native Real exact ETC regret from action-selected initial and full-history successor feedback laws. The exploration action identities turn each action-selected kernel into the constant law of the scheduled round-robin arm. The complete action/reward history is then projected to the reward-only prefix expected by the compiled finite-prefix uniqueness theorem.
theorem integral_realKernelRegret_externalAction_le_exact_sum_of_actionDependent_actionRewardHistory_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) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (hactionExplore : forall t, t < spec.explorationPulls * K -> (fun omega => action omega t) =ᵐ[mu] fun _omega => ETC.exploreArm spec t) (hzero : ProbabilityTheory.condDistrib (fun omega => reward omega 0) (fun omega => action omega 0) mu =ᵐ[ mu.map (fun omega => action omega 0)] ProbabilityTheory.Kernel.ofFunOfCountable (fun arm : Fin K => nu arm)) (hcond : forall i, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] (RewardKernel.contextIndependentOfActionLaws (Context