Lean module · EXP3
BanditRLProof.Exp3Potential
# EXP3 potential finite-sum wrappers This module records the deterministic finite-action potential surface used by exponential-weights/EXP3 routes. It deliberately stops before importance weighted estimators, logarithmic inequalities, learning-rate optimization, or a regret theorem.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.Exp3HedgeRegret, BanditRLProof.TsallisConjugatePotentialFiniteHorizon, BanditRLProof.TsallisTimeVaryingPenalty
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3Potential.potential
Compiled
Finite-action exponential-weights potential.
noncomputable def potential {Action : Type u} (arms : Finset Action) (w : Action -> Real) : Real
def
BanditRLProof.Exp3Potential.updatedWeight
Compiled
Multiplicative exponential-weights update for one action.
noncomputable def updatedWeight {Action : Type u} (eta : Real) (w loss : Action -> Real) (a : Action) : Real
def
BanditRLProof.Exp3Potential.updatedPotential
Compiled
Potential after applying the exponential-weights update on each action.
noncomputable def updatedPotential {Action : Type u} (arms : Finset Action) (eta : Real) (w loss : Action -> Real) : Real
theorem
BanditRLProof.Exp3Potential.updatedPotential_eq_sum
Compiled
Unfold the updated potential as an explicit finite sum.
theorem updatedPotential_eq_sum {Action : Type u} (arms : Finset Action) (eta : Real) (w loss : Action -> Real) : updatedPotential arms eta w loss = arms.sum (fun a => w a * Real.exp (-eta * loss a))
theorem
BanditRLProof.Exp3Potential.updatedWeight_nonneg_of_nonneg
Compiled
Exponential updating preserves nonnegative weights.
theorem updatedWeight_nonneg_of_nonneg {Action : Type u} (eta : Real) (w loss : Action -> Real) (a : Action) (hw : 0 <= w a) : 0 <= updatedWeight eta w loss a
theorem
BanditRLProof.Exp3Potential.updatedPotential_nonneg_of_nonneg
Compiled
The updated potential is nonnegative when all current finite weights are.
theorem updatedPotential_nonneg_of_nonneg {Action : Type u} (arms : Finset Action) (eta : Real) (w loss : Action -> Real) (hw : forall a, a ∈ arms -> 0 <= w a) : 0 <= updatedPotential arms eta w loss
theorem
BanditRLProof.Exp3Potential.updatedPotential_sub_potential_eq_sum_weight_mul_exp_sub_one
Compiled
One-step potential increment identity. This is the algebraic finite-sum surface used before applying any EXP/log inequality such as `exp x <= 1 + x + x^2`.
theorem updatedPotential_sub_potential_eq_sum_weight_mul_exp_sub_one {Action : Type u} (arms : Finset Action) (eta : Real) (w loss : Action -> Real) : updatedPotential arms eta w loss - potential arms w = arms.sum (fun a => w a * (Real.exp (-eta * loss a) - 1))
theorem
BanditRLProof.Exp3Potential.sum_range_forward_difference
Compiled
Finite-horizon telescoping for a real-valued potential process.
theorem sum_range_forward_difference (Phi : Nat -> Real) (T : Nat) : (Finset.range T).sum (fun t => Phi (t + 1) - Phi t) = Phi T - Phi 0
def
BanditRLProof.Exp3Potential.potentialProcess
Compiled
Potential process induced by a time-indexed finite-action weight family.
noncomputable def potentialProcess {Action : Type u} (arms : Finset Action) (w : Nat -> Action -> Real) (t : Nat) : Real
theorem
BanditRLProof.Exp3Potential.potentialProcess_telescope_sum_range
Compiled
Finite-horizon telescope specialized to exponential-weights potentials. This is the compiled local replacement for treating "the potential telescopes" as only a proof weapon.
theorem potentialProcess_telescope_sum_range {Action : Type u} (arms : Finset Action) (w : Nat -> Action -> Real) (T : Nat) : (Finset.range T).sum (fun t => potentialProcess arms w (t + 1) - potentialProcess arms w t) = potentialProcess arms w T - potentialProcess arms w 0