BanditRLProof.LowerBounds.InstanceDependent

The exact scalar asymptotic quantifier in Definition 16.1: a nonnegative regret sequence is smaller than every positive polynomial order. Regret nonnegativity is kept outside this analytic predicate so callers must expose the model-specific fact explicitly.

def IsConsistentRegret (regret : Nat -> Real) : Prop

Definition 16.1 over an abstract policy/environment regret interface. This preserves the source quantifier order: one policy, every environment in the class, and every positive real exponent.

def IsConsistentPolicyOver {Policy Environment : Type*} (environmentClass : Set Environment) (regret : Policy -> Environment -> Nat -> Real) (policy : Policy) : Prop

The sum of two source-consistent regret sequences is still consistent. This is the closure step used for `R_n(nu) + R_n(nu')` in the proof of Theorem 16.2.

theorem IsConsistentRegret.add {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) : IsConsistentRegret (fun n => first n + second n)

Two consistent regret sequences are eventually at most `n^p` for every positive exponent `p`. This is a stronger eventual form of the source's auxiliary `C_p n^p` bound and avoids introducing an opaque constant.

theorem IsConsistentRegret.eventually_add_le_rpow {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) {p : Real} (hp : 0 < p) : ∀ᶠ n : Nat in atTop, first n + second n <= (n : Real) ^ p

Eventually, the logarithmic growth ratio of a positive sum of two consistent regrets is at most every positive exponent. This is the direction-correct analytic leaf used before the source takes a limsup.

theorem IsConsistentRegret.eventually_log_add_div_log_le {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) (hpositive : ∀ᶠ n : Nat in atTop, 0 < first n + second n) {p : Real} (hp : 0 < p) : ∀ᶠ n : Nat in atTop, Real.log (first n + second n) / Real.log n <= p

The source quantity `d_inf(P, muStar, M) = inf {D(P,P') : P' in M, mean(P') > muStar}`. The value is extended-real, so an empty alternative set has infimum `∞` and support failures remain visible.

def divergenceInfimum {Reward : Type*} [MeasurableSpace Reward] (P : Measure Reward) (muStar : Real) (distributionClass : Set (Measure Reward)) (mean : Measure Reward -> Real) : ENNReal

Any admissible confusing alternative upper-bounds `d_inf`, with KL in the source direction from the original law to the alternative law.

theorem divergenceInfimum_le {Reward : Type*} [MeasurableSpace Reward] {P P' : Measure Reward} {muStar : Real} {distributionClass : Set (Measure Reward)} {mean : Measure Reward -> Real} (hclass : P' ∈ distributionClass) (hbetter : muStar < mean P') : divergenceInfimum P muStar distributionClass mean <= relativeEntropy P P'

Parameterized form of `d_inf`, useful when a distribution class is presented by a family of laws rather than an injective set-level mean map.

def parametricDivergenceInfimum {Reward Parameter : Type*} [MeasurableSpace Reward] (law : Parameter -> Measure Reward) (mean : Parameter -> Real) (parameter : Parameter) (muStar : Real) : ENNReal

Candidate inequality for the parameterized `d_inf` surface.

theorem parametricDivergenceInfimum_le {Reward Parameter : Type*} [MeasurableSpace Reward] {law : Parameter -> Measure Reward} {mean : Parameter -> Real} {parameter alternative : Parameter} {muStar : Real} (hbetter : muStar < mean alternative) : parametricDivergenceInfimum law mean parameter muStar <= relativeEntropy (law parameter) (law alternative)

Unit-variance Gaussian specialization of the source `d_inf`.

abbrev unitGaussianDivergenceInfimum (mu muStar : Real) : ENNReal

A Gaussian alternative with mean `muStar + epsilon` is admissible and has the exact arm-level information cost shown here. Taking `epsilon -> 0` is a separate infimum/limit leaf and is not hidden in this theorem.

theorem unitGaussianDivergenceInfimum_le_perturbed (mu muStar epsilon : Real) (hepsilon : 0 < epsilon) : unitGaussianDivergenceInfimum mu muStar <= ENNReal.ofReal (((muStar - mu) + epsilon) ^ 2 / 2)