Lean module · ETC
BanditRLProof.Algorithms.ETCRealLMLCompat
# Native Real ETC LML field compatibility surface The pinned LML source currently uses a newer Lean/mathlib toolchain, so ABRL cannot import its `IsAlgEnvSeq` declaration directly. This module packages the exact measurable-action, measurable-feedback, action-behavior, and stationary feedback-law consequences consumed by the local ETC theorem. It is a local compatibility structure, not an imported LML proof.
Module map
Imports
BanditRLProof.Algorithms.ETCRealHistoryScore
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.ETC.RealStationaryETCSequence
Compiled
The exact consequences of a stationary Real ETC algorithm-environment sequence used by the local regret route. The fields correspond to the pinned source's `IsAlgEnvSeq` measurability and feedback fields together with `ETC.arm_of_lt`, `ETC.arm_mul`, and `ETC.arm_of_ge`. Conditional laws are stated as `condDistrib` equalities, which is the Mathlib-facing form consumed by ABRL.
structure RealStationaryETCSequence {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (spec : ETC.Spec K) (nu : ProbabilityTheory.Kernel (Fin K) Real) [ProbabilityTheory.IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) : Prop where
theorem
BanditRLProof.ETC.regret_le_of_realStationaryETCSequence
Compiled
Exact native Real ETC regret from the bundled stationary sequence fields. This is the local theorem corresponding to the mathematical statement of the pinned LML `Bandits.ETC.regret_le`. A direct theorem about the imported LML `IsAlgEnvSeq` symbol still requires a common Lean/mathlib toolchain.
theorem regret_le_of_realStationaryETCSequence {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] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (h : ETC.RealStationaryETCSequence mu spec nu action reward) (sigma2 : NNReal) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun x => x - realKernelMean nu arm) sigma2 (nu arm)) (hm : 0 < spec.explorationPulls) (n : Nat) (hn : K * spec.explorationPulls <= n) : 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)))))