Finite independent Pandora model with positive and zero multiplier index rules
DefinitionPandoraBO_ModelThere are independent integrable real box rewards with positive deterministic opening costs. Measurable randomized policies use ordered histories and an independent uniform seed, must open a first box, never reopen a box, and stop irreversibly. Reward is the maximum observed reward without an outside option. The module defines expected reward and cost, penalized and budget optimality, real value suprema and the nonnegative dual minimum. Positive index policies use finite expected-improvement roots. The new zero index is the infimum of all almost-sure extended-real upper bounds of a box reward, that is, its essential supremum; it can be positive infinity. A generalized policy is either a positive-multiplier Gittins policy or a zero-multiplier essential-supremum policy. Complementary slackness means and does not itself include feasibility. The existing strict-gap predicate remains only for a positivity corollary. No optimality, multiplier existence, or budget matching is built into the definitions.
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Instances
import Mathlib.Data.EReal.Basic
/-!
# A finite, independent Pandora's-box model
There are `n + 1` boxes. Rewards have arbitrary integrable probability laws on
the real line and costs are deterministic and strictly positive. A policy
observes an ordered history, uses an independent uniform seed for randomization,
opens at least one box, and never opens a box twice. Stopping is irrevocable.
The definitions impose no optimality, budget activity, or reservation-index
existence assumptions on an instance or on a policy.
-/
set_option autoImplicit false
noncomputable section
open MeasureTheory
namespace PandoraBO
abbrev Box (n : ℕ) := Fin (n + 1)
/-- An ordered history, padded with inactive slots. The Boolean marks whether
the slot is occupied; the other coordinates are the box and its observed reward.
Padding retains the ordinary finite-product Borel measurable structure. -/
abbrev History (n : ℕ) := Fin (n + 1) → Bool × Box n × ℝ
abbrev Decision (n : ℕ) := Option (Box n)
instance decisionMeasurableSpace (n : ℕ) : MeasurableSpace (Decision n) := ⊤
/-- The full, finite independent-box model. -/
structure Instance (n : ℕ) where
law : Box n → Measure ℝ
law_probability : ∀ i, IsProbabilityMeasure (law i)
reward_integrable : ∀ i, Integrable (fun x : ℝ => x) (law i)
cost : Box n → ℝ
cost_positive : ∀ i, 0 < cost i
/-- A single uniform seed suffices for arbitrary randomized policies with a
finite horizon and standard Borel observations. It is independent of all boxes. -/
def seedLaw : Measure ℝ := volume.restrict (Set.Icc 0 1)
abbrev Outcome (n : ℕ) := (Box n → ℝ) × ℝ
/-- Independent rewards and an independent uniform randomization seed. -/
def jointLaw {n : ℕ} (M : Instance n) : Measure (Outcome n) :=
letI : ∀ i, IsProbabilityMeasure (M.law i) := M.law_probability
(Measure.pi M.law).prod seedLaw
def occupied {n : ℕ} (h : History n) (k : Fin (n + 1)) : Prop :=
(h k).1 = true
def observedBox {n : ℕ} (h : History n) (k : Fin (n + 1)) : Box n :=
(h k).2.1
def observedReward {n : ℕ} (h : History n) (k : Fin (n + 1)) : ℝ :=
(h k).2.2
def wasOpened {n : ℕ} (h : History n) (i : Box n) : Prop :=
∃ k, occupied h k ∧ observedBox h k = i
/-- Histories are nonempty occupied prefixes and contain no repeated box. -/
def validHistory {n : ℕ} (h : History n) : Prop :=
occupied h 0 ∧
(∀ k l, k ≤ l → occupied h l → occupied h k) ∧
(∀ k l, occupied h k → occupied h l →
observedBox h k = observedBox h l → k = l)
/-- Policies choose using only their uniform seed and past observations.
`none` means stop. The first opening is mandatory. -/
structure Policy (n : ℕ) where
first : ℝ → Box n
first_measurable : Measurable first
next : History n × ℝ → Decision n
next_measurable : Measurable next
next_unopened : ∀ h u i, next (h, u) = some i → ¬ wasOpened h i
/-- Initial history after the mandatory first opening. -/
def initialHistory {n : ℕ} (π : Policy n) (ω : Outcome n) : History n :=
fun k => if k = 0 then (true, π.first ω.2, ω.1 (π.first ω.2))
else (false, 0, 0)
/-- The fuel is the number of further opportunities. Stopping immediately
returns the current history, so a stopped policy can never resume. -/
def rolloutAux {n : ℕ} (π : Policy n) (ω : Outcome n) :
ℕ → ℕ → History n → History n
| 0, _, h => h
| fuel + 1, step, h =>
match π.next (h, ω.2) with
| none => h
| some i =>
if hs : step < n + 1 then
rolloutAux π ω fuel (step + 1)
(Function.update h ⟨step, hs⟩ (true, i, ω.1 i))
else h
/-- One mandatory opening followed by at most `n` further openings. -/
def terminalHistory {n : ℕ} (π : Policy n) (ω : Outcome n) : History n :=
rolloutAux π ω n 1 (initialHistory π ω)
/-- Maximum observed reward. The first occupied slot supplies the initial
maximum, so there is no outside option and negative rewards remain negative. -/
def historyReward {n : ℕ} (h : History n) : ℝ := by
classical
exact (List.finRange (n + 1)).foldl
(fun incumbent k => if occupied h k then max incumbent (observedReward h k)
else incumbent)
(observedReward h 0)
def historyCost {n : ℕ} (M : Instance n) (h : History n) : ℝ := by
classical
exact ∑ k : Fin (n + 1), if occupied h k then M.cost (observedBox h k) else 0
def terminalReward {n : ℕ} (π : Policy n) (ω : Outcome n) : ℝ :=
historyReward (terminalHistory π ω)
def terminalCost {n : ℕ} (M : Instance n) (π : Policy n) (ω : Outcome n) : ℝ :=
historyCost M (terminalHistory π ω)
def expectedReward {n : ℕ} (M : Instance n) (π : Policy n) : ℝ :=
∫ ω, terminalReward π ω ∂jointLaw M
def expectedCost {n : ℕ} (M : Instance n) (π : Policy n) : ℝ :=
∫ ω, terminalCost M π ω ∂jointLaw M
/-- Expected terminal maximum minus a multiplier times expected opening cost. -/
def value {n : ℕ} (M : Instance n) (multiplier : ℝ) (π : Policy n) : ℝ :=
expectedReward M π - multiplier * expectedCost M π
def optimal {n : ℕ} (M : Instance n) (multiplier : ℝ) (π : Policy n) : Prop :=
∀ ρ : Policy n, value M multiplier ρ ≤ value M multiplier π
def optimalValue {n : ℕ} (M : Instance n) (multiplier : ℝ) : ℝ :=
sSup {r : ℝ | ∃ π : Policy n, r = value M multiplier π}
def dualValue {n : ℕ} (M : Instance n) (B multiplier : ℝ) : ℝ :=
optimalValue M multiplier + multiplier * B
def dualMinimizer {n : ℕ} (M : Instance n) (B multiplier : ℝ) : Prop :=
0 ≤ multiplier ∧ ∀ t : ℝ, 0 ≤ t → dualValue M B multiplier ≤ dualValue M B t
def budgetFeasible {n : ℕ} (M : Instance n) (B : ℝ) (π : Policy n) : Prop :=
expectedCost M π ≤ B
def budgetOptimal {n : ℕ} (M : Instance n) (B : ℝ) (π : Policy n) : Prop :=
budgetFeasible M B π ∧
∀ ρ : Policy n, budgetFeasible M B ρ → expectedReward M ρ ≤ expectedReward M π
def fullInformationPayoff {n : ℕ} (r : Box n → ℝ) : ℝ :=
(List.finRange (n + 1)).foldl (fun incumbent i => max incumbent (r i)) (r 0)
def fullInformationReward {n : ℕ} (M : Instance n) : ℝ :=
∫ ω, fullInformationPayoff ω.1 ∂jointLaw M
def zeroCostOptimal {n : ℕ} (M : Instance n) (π : Policy n) : Prop :=
optimal M 0 π
def budgetValue {n : ℕ} (M : Instance n) (B : ℝ) : ℝ :=
sSup {r : ℝ | ∃ π : Policy n, budgetFeasible M B π ∧ r = expectedReward M π}
/-- A feasible budget with a strict reward gap below full information.
Used only for the positive-multiplier corollary, not the main theorem. -/
def genuinelyActiveBudget {n : ℕ} (M : Instance n) (B : ℝ) : Prop :=
(∃ π : Policy n, budgetFeasible M B π) ∧
budgetValue M B < fullInformationReward M
/-- A useful alternative activity condition, stated without assuming an
optimal multiplier exists. Its equivalence to a strict value gap needs proof. -/
def belowEveryFullInformationPolicy {n : ℕ} (M : Instance n) (B : ℝ) : Prop :=
∀ π : Policy n, expectedReward M π = fullInformationReward M → B < expectedCost M π
def expectedImprovement {n : ℕ} (M : Instance n) (i : Box n) (z : ℝ) : ℝ :=
∫ y, max (y - z) 0 ∂M.law i
def reservationRoot {n : ℕ} (M : Instance n) (i : Box n) (c z : ℝ) : Prop :=
expectedImprovement M i z = c
def reservationIndices {n : ℕ} (M : Instance n) (multiplier : ℝ) (z : Box n → ℝ) : Prop :=
∀ i, reservationRoot M i (multiplier * M.cost i) (z i)
/-- At a positive cost multiplier, a Pandora/Gittins policy opens a maximum
index first. It subsequently opens only a remaining maximum-index box whose
index is at least the incumbent; it stops only when every remaining index is
at most the incumbent. At equality either stopping or opening is permitted,
and all index ties may be randomized through the seed. -/
def isGittinsPolicy {n : ℕ} (M : Instance n) (multiplier : ℝ) (π : Policy n) : Prop :=
∃ z : Box n → ℝ, reservationIndices M multiplier z ∧
(∀ u i, z i ≤ z (π.first u)) ∧
(∀ h u, validHistory h →
match π.next (h, u) with
| none => ∀ i, ¬ wasOpened h i → z i ≤ historyReward h
| some i => historyReward h ≤ z i ∧
∀ j, ¬ wasOpened h j → z j ≤ z i)
/-- The essential supremum of a box reward, expressed as the infimum of
its almost-sure extended-real upper bounds. The value may be positive infinity;
the probability-law assumptions rule out negative infinity. -/
def zeroReservationIndex {n : ℕ} (M : Instance n) (i : Box n) : EReal :=
sInf {z : EReal | ∀ᵐ (y : ℝ) ∂M.law i, (y : EReal) ≤ z}
/-- The zero-multiplier index rule uses essential suprema rather than finite
solutions of a zero-level expected-improvement equation. Equality permits
stopping or continuing, and index ties can be randomized. A particular choice
of ties need not satisfy a given budget. -/
def isZeroGittinsPolicy {n : ℕ} (M : Instance n) (π : Policy n) : Prop :=
(∀ u i, zeroReservationIndex M i ≤ zeroReservationIndex M (π.first u)) ∧
(∀ h u, validHistory h →
match π.next (h, u) with
| none => ∀ i, ¬ wasOpened h i →
zeroReservationIndex M i ≤ (historyReward h : EReal)
| some i => (historyReward h : EReal) ≤ zeroReservationIndex M i ∧
∀ j, ¬ wasOpened h j → zeroReservationIndex M j ≤ zeroReservationIndex M i)
/-- The extended rule includes exactly the positive finite-index branch and
the zero essential-supremum branch. Negative multipliers satisfy neither. -/
def isGeneralizedGittinsPolicy {n : ℕ} (M : Instance n)
(multiplier : ℝ) (π : Policy n) : Prop :=
(0 < multiplier ∧ isGittinsPolicy M multiplier π) ∨
(multiplier = 0 ∧ isZeroGittinsPolicy M π)
/-- Complementary slackness permits unused expected budget when the
multiplier is zero; feasibility is a separate condition. -/
def complementarySlackness {n : ℕ} (M : Instance n)
(B multiplier : ℝ) (π : Policy n) : Prop :=
multiplier * (B - expectedCost M π) = 0
end PandoraBO
Read-back
What the Lean code literally says, in plain math · GPT-6 (Codex)
Box. For each natural number , the box set is , with exactly elements. In particular, means one box, never an empty box set.
History. For each natural number , a history is any function on the ordered slots whose value is a triple consisting of a Boolean, a box in , and a real number. This type itself imposes no validity, occupancy, uniqueness, or reward-support restrictions; even inactive slots have box and reward coordinates.
Decision. For each natural number , a decision is either no box, written stop, or one specified box in .
decisionMeasurableSpace. For each natural number , the measurable structure on the finite decision set consisting of stop and the individual box choices is the top measurable structure, so every subset of this decision set is measurable.
Instance. For each natural number , an instance assigns to every box a measure on the real line that is a probability measure and for which the identity real-valued function is integrable, together with a deterministic real cost satisfying . These requirements apply to every box, including when ; the structure adds no budget, multiplier, reward-sign, bounded-support, or optimality assumptions.
seedLaw. The seed law is Lebesgue measure restricted to the closed real interval .
Outcome. For each natural number , an outcome is a pair consisting of an arbitrary real reward vector on and an arbitrary real seed . The type itself does not restrict to .
jointLaw. For every natural number and instance with box laws , the law of the outcome is the product of the finite product measure and Lebesgue measure restricted to . Thus the coordinate rewards have their given probability laws independently, and the uniform seed is independent of all rewards.
occupied. For any natural number , history , and slot , the slot is occupied exactly when the Boolean coordinate of is true.
observedBox. For any natural number , history , and slot , the observed-box function returns the box coordinate of , regardless of whether the slot is occupied.
observedReward. For any natural number , history , and slot , the observed-reward function returns the real reward coordinate of , regardless of whether the slot is occupied.
wasOpened. For any natural number , history , and box , box was opened exactly when there exists a slot whose Boolean is true and whose box coordinate equals . A box appearing only in inactive slots does not satisfy this predicate.
validHistory. For any natural number , a history is valid exactly when slot zero is occupied, occupancy is downward closed in slot order (if and is occupied then is occupied), and two occupied slots having the same box must be the same slot. Therefore occupied slots form a nonempty prefix with distinct boxes. Observed rewards may be arbitrary real numbers; inactive-slot coordinates have no constraints.
Policy. For each natural number , a policy consists of a measurable map from real seeds to boxes for the mandatory first choice and a measurable map from pairs of a history and real seed to either stop or a box for subsequent choices. For every history, every real seed, and every box, if the subsequent-choice map returns that box, there is no occupied slot of the supplied history bearing it. This last requirement applies even to invalid histories and seeds outside . No optimality or index condition is part of the structure; the structure alone also does not require consistent responses when a previously stopped history is supplied again.
initialHistory. For any natural number , policy, and outcome , the initial history occupies slot zero with the first-choice box selected using and reward equal to that box’s coordinate of . Every other slot is set to the inactive triple with box zero and reward zero. There is always a first opening, including for .
rolloutAux. For any natural number , policy, outcome , natural fuel, natural insertion step, and history, the rollout returns the supplied history when fuel is zero. With positive fuel it evaluates the next decision on the current history and the same seed : stop returns the history immediately; a box choice updates the slot at the insertion step to that box and its coordinate of and recurses with one less fuel and insertion step increased by one, provided the step is less than ; an out-of-range step returns the current history. These arguments are unrestricted, so an arbitrary call can overwrite an occupied slot; a stop returns without further recursion.
terminalHistory. For any natural number , policy, and outcome, the terminal history is the preceding rollout started from the mandatory first-opening history with insertion step one and fuel . Thus the execution has one mandatory opening followed by at most further opening opportunities, and it never resumes after a stop. When it is simply the initial history.
historyReward. For any natural number and history, the history reward starts from the real coordinate of slot zero and scans all slots in order, replacing the running value by its maximum with each occupied slot’s reward and ignoring inactive slots. For a valid history it is exactly the maximum occupied reward, with no extra outside option such as zero. For an arbitrary invalid history the slot-zero reward contributes even if slot zero is inactive.
historyCost. For any natural number , instance with costs , and history, the history cost is the sum over its slots of for an occupied slot bearing box and zero for an inactive slot. It counts slots, so repeated boxes in an invalid history contribute repeatedly.
terminalReward. For any natural number , policy, and outcome, the terminal reward is the history-reward fold applied to the policy’s terminal history obtained from its mandatory first opening and at most further rollout steps.
terminalCost. For any natural number , instance, policy, and outcome, the terminal cost is the sum of the costs of the occupied slots in the terminal history generated by the mandatory first opening and at most further rollout steps.
expectedReward. For any natural number , instance, and policy, expected reward is the real-valued Bochner integral of its terminal reward under the product law of all independent box rewards and the independent uniform seed. The definition has no separate integrability hypothesis on this terminal function; the integral is the library’s total integral operation, which returns zero on a nonintegrable function.
expectedCost. For any natural number , instance, and policy, expected cost is the real-valued Bochner integral of its terminal cost under the product law of all independent box rewards and the independent uniform seed. The definition has no separate integrability hypothesis on this terminal function; the integral is the library’s total integral operation, which returns zero on a nonintegrable function.
value. For any natural number , instance, arbitrary real multiplier , and policy , its value is , where and are the joint-law integrals of its terminal reward and terminal cost. This definition also accepts zero and negative multipliers.
optimal. For any natural number , instance, arbitrary real multiplier , and policy , optimality means that for every policy on the same boxes, , where and are expected terminal reward and cost. It imposes no budget constraint or uniqueness requirement.
optimalValue. For any natural number , instance, and arbitrary real multiplier , optimal value is the real supremum of all numbers as ranges over policies on the same boxes. This uses the real, conditionally complete supremum operation; the definition does not itself assert boundedness, attainment, or existence of a maximizing policy.
dualValue. For any natural number , instance, and arbitrary real budget and multiplier , the dual value is , with the supremum taken in the reals over all policies on the instance.
dualMinimizer. For any natural number , instance, real budget , and real multiplier , being a dual minimizer means both and for every real , where . There is no uniqueness requirement and no comparison to negative multipliers.
budgetFeasible. For any natural number , instance, arbitrary real budget , and policy , budget feasibility means , where is expected terminal opening cost. It is an expectation constraint and does not assert that the realized cost is always at most .
budgetOptimal. For any natural number , instance, arbitrary real budget , and policy , budget optimality means that and that every policy with satisfies , where and are expected terminal cost and reward. Feasibility of is an explicit conjunct.
fullInformationPayoff. For any natural number and arbitrary real reward vector on boxes , the full-information payoff starts from and successively takes the maximum with over all boxes. It equals and has no outside option of zero; when it is .
fullInformationReward. For any natural number and instance, full-information reward is the real Bochner integral of the maximum of all reward coordinates under the joint product law of the independent box rewards and independent uniform seed. This is a reward integral, with no costs subtracted.
zeroCostOptimal. For any natural number , instance, and policy , zero-cost optimality means optimality at multiplier zero: every policy satisfies . Actual box costs remain strictly positive; this predicate merely gives them zero coefficient in the objective and imposes no budget constraint.
budgetValue. For any natural number , instance, and arbitrary real budget , budget value is the real supremum of over policies satisfying . The definition includes budgets with no feasible policies and uses the total real supremum operation on the resulting set; it does not assert nonemptiness, boundedness, or attainment.
genuinelyActiveBudget. For any natural number , instance, and real budget , genuine activity means that at least one policy has expected cost at most and that the real supremum of expected rewards over all such policies is strictly less than the expected maximum of all box rewards. Both feasibility and a strict value gap are required.
belowEveryFullInformationPolicy. For any natural number , instance, and real budget , this condition says that for every policy whose expected terminal reward equals the expected maximum of all box rewards, its expected cost is strictly greater than . It is an implication quantified over all policies and has no explicit feasible-policy, supremum-gap, or multiplier assumption; if no policy met the equality, it would hold vacuously.
expectedImprovement. For any natural number , instance, box , and real threshold , expected improvement is the real Bochner integral , using only that box’s probability law. It is not an expectation over the other boxes or the seed.
reservationRoot. For any natural number , instance, box , and arbitrary real numbers , being a reservation root means exactly . The predicate itself requires neither nor root existence or uniqueness.
reservationIndices. For any natural number , instance, arbitrary real multiplier , and real-valued vector on all boxes, being reservation indices means that every box satisfies . All indices are finite real numbers; no positivity condition on occurs in this predicate.
isGittinsPolicy. For any natural number , instance, arbitrary real multiplier , and policy , this condition asserts existence of finite real numbers satisfying for every box. For every real seed , the first box chosen has index at least every box’s index. For every valid history (a nonempty occupied prefix with distinct boxes and arbitrary real observed rewards) and every real seed, if the next decision is stop, each unopened box has index at most the current maximum observed reward; if it chooses box , that maximum is at most , and every unopened box has index at most . The policy structure also requires the chosen box to be unopened. All comparisons are weak, so equality allows either decision, and the requirements cover histories and seeds of probability zero. The definition itself does not require a positive multiplier.
zeroReservationIndex. For any natural number , instance, and box , its zero reservation index is the infimum, in the extended reals , of all extended-real numbers such that for -almost every real reward , with embedded in the extended reals. The set of bounds includes ; the resulting essential supremum may be , and this definition is not a search for a finite root of an expected-improvement equation.
isZeroGittinsPolicy. For any natural number , instance, and policy, let be the extended-real infimum of the almost-sure upper bounds on box ’s reward. For every real seed, the first chosen box must have at least every box’s index. For every valid history (a nonempty occupied prefix with distinct boxes and arbitrary real observed rewards) and every real seed, stopping requires to be at most the real incumbent reward embedded in the extended reals for every unopened box; choosing box requires the embedded incumbent to be at most , and every unopened box’s index to be at most . The underlying policy additionally forbids opening an already occupied box. Indices may be , comparisons are non-strict, and these requirements hold at all valid histories and all real seeds, with no budget condition.
isGeneralizedGittinsPolicy. For any natural number , instance, real multiplier , and policy, this predicate is the disjunction of two cases: and the finite reservation-index policy rule holds, or and the extended-real essential-supremum policy rule holds. The finite rule uses roots , whereas the zero rule uses infima of almost-sure extended-real reward upper bounds; in both cases the first choice maximizes the indices, continuation chooses a maximum unopened index at least the incumbent, and stopping requires every unopened index to be at most the incumbent, at every real seed and valid history. Negative multipliers satisfy neither branch.
complementarySlackness. For any natural number , instance, arbitrary real budget and multiplier , and policy , complementary slackness means exactly , where is expected terminal cost. No multiplier-sign or feasibility condition is included: at the equation holds for every policy and budget, and at a nonzero multiplier it requires .