Lean module · ETC
BanditRLProof.Algorithms.ETCRealSourceAdapter
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.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.integral_realKernelRegret_externalAction_le_exact_sum_of_actionDependent_actionRewardHistory_condDistribReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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 := History.FinitePairHistory (Fin K) Real i) (fun arm : Fin K => nu arm) (fun _arm => inferInstance)).kernel) (hactionETC : Filter.Eventually (fun omega => forall t, t < n -> action omega t = ETC.realExplorationArgmaxAction spec (ETC.realKernelBestArm spec.hK nu) (reward omega) t) (ae mu)) : integral mu (fun omega => realKernelRegret nu (action omega) 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)))))