BanditRLProof.LowerBounds.BasicIdeas

Worst-case expected regret of one policy over an explicit environment class. The `ENNReal` codomain supplies the source-level supremum without a hidden boundedness hypothesis. If `environmentClass` is empty, this retains the standard complete-lattice value `bot`; meaningful bandit consumers should prove their intended class is nonempty.

noncomputable def worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (environmentClass : Set Environment) (policy : Policy) : ENNReal

Minimax expected regret over explicit policy and environment classes. The definition mirrors `inf_pi sup_nu R_n(pi,nu)`. Nonemptiness of the classes is intentionally a consumer-side semantic contract rather than a hidden assumption of the definition.

noncomputable def minimaxExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) : ENNReal

A policy is minimax optimal for an explicit policy class, environment class, and fixed-horizon regret functional when it is admissible and its worst-case regret attains the minimax value. The horizon is carried by `regret`; keeping the two classes explicit records the source warning that minimax optimality is not a property of a policy alone.

def IsMinimaxOptimal {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (policy : Policy) : Prop

A minimax-optimal policy belongs to the policy class over which the infimum is taken.

theorem IsMinimaxOptimal.mem_policyClass {Policy : Type u} {Environment : Type v} {regret : Policy -> Environment -> ENNReal} {policyClass : Set Policy} {environmentClass : Set Environment} {policy : Policy} (hpolicy : IsMinimaxOptimal regret policyClass environmentClass policy) : policy ∈ policyClass

A minimax-optimal policy attains the fixed-class minimax value.

theorem IsMinimaxOptimal.eq_minimaxExpectedRegret {Policy : Type u} {Environment : Type v} {regret : Policy -> Environment -> ENNReal} {policyClass : Set Policy} {environmentClass : Set Environment} {policy : Policy} (hpolicy : IsMinimaxOptimal regret policyClass environmentClass policy) : worstCaseExpectedRegret regret environmentClass policy = minimaxExpectedRegret regret policyClass environmentClass

One environment's regret is below the worst case over any class containing it.

theorem expectedRegret_le_worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (environmentClass : Set Environment) (policy : Policy) (environment : Environment) (henvironment : environment ∈ environmentClass) : regret policy environment ≤ worstCaseExpectedRegret regret environmentClass policy

The minimax value is below the worst-case value of each admissible policy.

theorem minimaxExpectedRegret_le_worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (policy : Policy) (hpolicy : policy ∈ policyClass) : minimaxExpectedRegret regret policyClass environmentClass ≤ worstCaseExpectedRegret regret environmentClass policy

A uniform lower bound on every admissible policy is a minimax lower bound.

theorem le_minimaxExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (lower : ENNReal) (hlower : ∀ policy : policyClass, lower ≤ worstCaseExpectedRegret regret environmentClass policy.1) : lower ≤ minimaxExpectedRegret regret policyClass environmentClass

Finite averaging: among a nonempty family whose sum is at most `budget`, one coordinate is at most `budget / m`. This is a Mathlib-composed deterministic leaf. It contains no bandit law, expectation, measurability, or concentration assumption.

theorem exists_alternative_le_average {m : Nat} (hm : 0 < m) (alternativeExpectedPulls : Fin m -> Real) (budget : Real) (hbudget : ∑ i : Fin m, alternativeExpectedPulls i ≤ budget) : ∃ i : Fin m, alternativeExpectedPulls i ≤ budget / (m : Real)

Removing the distinguished arm zero from an exact nonnegative pull budget leaves at most the full budget on the `Fin.succ` alternative arms.

theorem alternativeExpectedPullBudget_le {m : Nat} (expectedPulls : Fin (m + 1) -> Real) (budget : Real) (hnonneg : ∀ arm, 0 ≤ expectedPulls arm) (htotal : ∑ arm : Fin (m + 1), expectedPulls arm = budget) : (∑ i : Fin m, expectedPulls i.succ) ≤ budget

Chapter 13's least-explored alternative arm. There are `m + 1` arms: arm zero is the base arm and `i.succ`, for `i : Fin m`, are the alternatives. The hypotheses are precisely the expected pull-count nonnegativity and total-budget identity needed by the averaging argument.

theorem exists_leastExploredAlternative {m : Nat} (hm : 0 < m) (expectedPulls : Fin (m + 1) -> Real) (horizon : Nat) (hnonneg : ∀ arm, 0 ≤ expectedPulls arm) (htotal : ∑ arm : Fin (m + 1), expectedPulls arm = (horizon : Real)) : ∃ i : Fin m, expectedPulls i.succ ≤ (horizon : Real) / (m : Real)

The exact deterministic expression in the base-environment identity (13.2).

def baseEnvironmentRegret (horizon : Nat) (gap baseFirstExpectedPulls : Real) : Real

The changed-environment regret lower expression on the right of (13.3).

def changedEnvironmentRegretLowerBound (gap changedFirstExpectedPulls : Real) : Real

Quantitative algebraic core of the two-environment heuristic. The premise bounds the cross-environment discrepancy in the expected number of base-arm pulls. Chapter 13 writes these expectations as approximately equal; later information-theoretic chapters must supply an actual value of `error`. This theorem neither derives that premise nor proves Theorem 13.1.

theorem max_base_changed_regretLowerBound_ge_half_sub_error (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls error : Real) (hgap : 0 ≤ gap) (hpullDifference : baseFirstExpectedPulls - changedFirstExpectedPulls ≤ error) : gap * ((horizon : Real) - error) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)

Zero-error corollary of the quantitative two-environment algebra. The premise `baseFirstExpectedPulls ≤ changedFirstExpectedPulls` specializes the pull discrepancy to at most zero. The quantitative predecessor is the intended interface for later information theorems; neither declaration is the Gaussian minimax lower bound.

theorem max_base_changed_regretLowerBound_ge_half (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls : Real) (hgap : 0 ≤ gap) (htransport : baseFirstExpectedPulls ≤ changedFirstExpectedPulls) : gap * (horizon : Real) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)