EconCSLib.MechanismDesign.Auction.Knapsack

Knapsack auctions in the single-parameter setting.

This file specializes Auction.SingleParameterMechanism to a standard knapsack-auction environment:

• each agent i reports a scalar value in U
• agent i has public weight w i
• the mechanism chooses an allocation vector x : I → U
• the total weighted allocation must respect the capacity bound W

Structure hierarchy

MechanismWithTransfers I (fun _ => U) (I → U) U   -- scalar reports and allocations
  └─ SingleParameterMechanism I U                 -- single-parameter transfer layer
       └─ KnapsackAuction I U                       -- public weights + total capacity
            └─ welfareMaximizingMechanism hW      -- Myerson-payment implementation

Main definitions

• KnapsackAuction — a single-parameter mechanism with public weights and a total capacity bound
• RespectsCapacity, IsFeasible — feasibility predicates for U-valued allocations
• BinaryAllocation, binaryToAllocation, binaryLoad, binaryRespectsCapacity — 0/1 allocation profiles and their induced load
• feasibleBinaryAllocations, binarySocialWelfare — the finite feasible allocation space and its welfare objective
• welfareMaximizer, maximalSocialWelfare — a chosen welfare-maximizing feasible binary allocation and its objective value
• welfareMaximizingAllocationRule, welfareMaximizingPaymentRule, welfareMaximizingMechanism — the induced single-parameter mechanism with Myerson payments
• dpSolveList, dynamicProgrammingOptimalAllocation, dynamicProgrammingOptimalValue — a dynamic-programming solver for the natural-number 0/1 knapsack specialization

Main proofs

• existence of a welfare-maximizing feasible binary allocation
• monotonicity of the welfare-maximizing allocation rule
• DSIC of the welfare-maximizing mechanism via SingleParameterMechanism.withMyersonPayment_isDSIC_of_isMonotone
• correctness of the dynamic-programming solver in the natural-number setting: dynamicProgrammingOptimalAllocation_feasible proves the DP output satisfies the capacity constraint, and dynamicProgrammingOptimalAllocation_optimal proves it maximizes social welfare among all feasible binary allocations

structure KnapsackAuction (I : Type u_1) (U : Type u_2) extends SingleParameterMechanism I U : Type (max u_1 u_2)

A knapsack auction with public weights w i and total capacity W.

The underlying strategic object is a SingleParameterMechanism I U, where the value type U is a linearly ordered field ([Field U] [LinearOrder U] [IsStrictOrderedRing U]; e.g. ℚ, ℝ): each agent reports a single scalar value in U, receives an allocation level xᵢ ∈ U, and makes a U-valued payment. The pointwise allocation bounds are inherited from SingleParameterMechanism.IsAllocFeasible; the knapsack constraint is recorded separately below.

• allocationRule : (I → U) → I → U
• paymentRule : (I → U) → I → U
• weight : I → U

  Public weight / size of agent i in the knapsack constraint.

• totalCapacity : U

  Total knapsack capacity.

def KnapsackAuction.RespectsCapacity {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [Fintype I] (A : KnapsackAuction I U) : Prop

The allocation rule respects the knapsack capacity constraint.

Equations

• A.RespectsCapacity = ∀ (b : I → U), ∑ i : I, A.weight i * A.allocationRule b i ≤ A.totalCapacity

def KnapsackAuction.IsFeasible {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [Fintype I] (A : KnapsackAuction I U) : Prop

Feasibility for a knapsack auction:

• each agent's allocation lies in [0,1]
• the weighted allocation satisfies the total capacity bound

Equations

• A.IsFeasible = (A.IsAllocFeasible ∧ A.RespectsCapacity)

@[reducible, inline]

abbrev KnapsackAuction.size {I : Type u_1} {U : Type u_2} (A : KnapsackAuction I U) (i : I) : U

Agent i's public weight.

Equations

• A.size i = A.weight i

@[reducible, inline]

abbrev KnapsackAuction.capacity {I : Type u_1} {U : Type u_2} (A : KnapsackAuction I U) : U

The total capacity bound.

Equations

• A.capacity = A.totalCapacity

def KnapsackAuction.NonnegativeWeights {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] (A : KnapsackAuction I U) : Prop

Every public weight is nonnegative.

Equations

• A.NonnegativeWeights = ∀ (i : I), 0 ≤ A.weight i

def KnapsackAuction.PositiveWeights {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] (A : KnapsackAuction I U) : Prop

Every public weight is strictly positive.

Equations

• A.PositiveWeights = ∀ (i : I), 0 < A.weight i

def KnapsackAuction.NonnegativeCapacity {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] (A : KnapsackAuction I U) : Prop

The knapsack capacity is nonnegative.

Equations

• A.NonnegativeCapacity = (0 ≤ A.totalCapacity)

@[reducible, inline]

abbrev KnapsackAuction.BinaryAllocation (I : Type u_3) : Type u_3

A discrete knapsack allocation profile: each agent is either selected or not.

Equations

• KnapsackAuction.BinaryAllocation I = (I → Bool)

def KnapsackAuction.binaryToAllocation {I : Type u_1} {U : Type u_2} [Field U] (x : BinaryAllocation I) : I → U

The 0/1 allocation vector associated with a binary allocation profile.

Equations

• KnapsackAuction.binaryToAllocation x i = if x i = true then 1 else 0

def KnapsackAuction.binaryLoad {I : Type u_1} {U : Type u_2} [Field U] [Fintype I] (A : KnapsackAuction I U) (x : BinaryAllocation I) : U

The weighted load induced by a binary allocation profile.

Equations

• A.binaryLoad x = ∑ i : I, A.weight i * KnapsackAuction.binaryToAllocation x i

def KnapsackAuction.binaryRespectsCapacity {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [Fintype I] (A : KnapsackAuction I U) (x : BinaryAllocation I) : Prop

Capacity feasibility for a binary allocation profile.

Equations

• A.binaryRespectsCapacity x = (A.binaryLoad x ≤ A.totalCapacity)

noncomputable def KnapsackAuction.feasibleBinaryAllocations {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) : List (BinaryAllocation I)

The finite list of binary allocations satisfying the knapsack constraint.

Equations

• A.feasibleBinaryAllocations = {x : KnapsackAuction.BinaryAllocation I | A.binaryRespectsCapacity x}.toList

def KnapsackAuction.binarySocialWelfare {I : Type u_1} {U : Type u_2} [Field U] [Fintype I] (b : I → U) (x : BinaryAllocation I) : U

Social welfare of a binary allocation profile at valuation profile b.

Equations

• KnapsackAuction.binarySocialWelfare b x = ∑ i : I, b i * KnapsackAuction.binaryToAllocation x i

theorem KnapsackAuction.zeroBinaryRespectsCapacity {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] (A : KnapsackAuction I U) (hW : 0 ≤ A.totalCapacity) : A.binaryRespectsCapacity fun (x : I) => false

theorem KnapsackAuction.feasibleBinaryAllocations_nonempty {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) (hW : 0 ≤ A.totalCapacity) : A.feasibleBinaryAllocations ≠ []

theorem KnapsackAuction.exists_welfareMaximizer {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) (b : I → U) (hW : 0 ≤ A.totalCapacity) : ∃ x ∈ A.feasibleBinaryAllocations, ∀ y ∈ A.feasibleBinaryAllocations, binarySocialWelfare b y ≤ binarySocialWelfare b x

A welfare-maximizing feasible binary allocation, chosen using List.argMaxOn on the finite space of feasible 0/1 allocations.

noncomputable def KnapsackAuction.welfareMaximizer {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) (b : I → U) (hW : 0 ≤ A.totalCapacity) : BinaryAllocation I

Equations

• A.welfareMaximizer b hW = Classical.choose ⋯

noncomputable def KnapsackAuction.maximalSocialWelfare {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) (b : I → U) (hW : 0 ≤ A.totalCapacity) : U

The maximal social welfare over the feasible binary allocation space.

Equations

• A.maximalSocialWelfare b hW = KnapsackAuction.binarySocialWelfare b (A.welfareMaximizer b hW)

theorem KnapsackAuction.welfareMaximizer_mem_feasibleBinaryAllocations {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) (b : I → U) (hW : 0 ≤ A.totalCapacity) : A.welfareMaximizer b hW ∈ A.feasibleBinaryAllocations

theorem KnapsackAuction.welfareMaximizer_ge {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) (b : I → U) (hW : 0 ≤ A.totalCapacity) {x : BinaryAllocation I} (hx : x ∈ A.feasibleBinaryAllocations) : binarySocialWelfare b x ≤ binarySocialWelfare b (A.welfareMaximizer b hW)

theorem KnapsackAuction.binarySocialWelfare_update {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (b : I → U) (i : I) (θ : U) (x : BinaryAllocation I) : binarySocialWelfare (Function.update b i θ) x = θ * binaryToAllocation x i + ∑ j ∈ Finset.univ.erase i, b j * binaryToAllocation x j

noncomputable def KnapsackAuction.welfareMaximizingAllocationRule {I : Type u_1} [Fintype I] [DecidableEq I] (A : KnapsackAuction I ℝ) (hW : 0 ≤ A.totalCapacity) : (I → ℝ) → I → ℝ

The welfare-maximizing allocation rule for the knapsack auction, obtained by choosing a feasible binary allocation with maximal social welfare and then viewing it as an I → ℝ allocation vector.

Equations

• A.welfareMaximizingAllocationRule hW b = KnapsackAuction.binaryToAllocation (A.welfareMaximizer b hW)

noncomputable def KnapsackAuction.welfareMaximizingPaymentRule {I : Type u_1} [Fintype I] [DecidableEq I] (A : KnapsackAuction I ℝ) (hW : 0 ≤ A.totalCapacity) : (I → ℝ) → I → ℝ

The Myerson payment formula associated with the welfare-maximizing knapsack allocation rule.

Equations

• A.welfareMaximizingPaymentRule hW = SingleParameterMechanism.myersonPayment (A.welfareMaximizingAllocationRule hW)

noncomputable def KnapsackAuction.welfareMaximizingMechanism {I : Type u_1} [Fintype I] [DecidableEq I] (A : KnapsackAuction I ℝ) (hW : 0 ≤ A.totalCapacity) : SingleParameterMechanism I ℝ

The canonical welfare-maximizing single-parameter knapsack mechanism, with payments given by the Myerson formula.

Equations

• A.welfareMaximizingMechanism hW = { allocationRule := A.welfareMaximizingAllocationRule hW, paymentRule := A.welfareMaximizingPaymentRule hW }

theorem KnapsackAuction.welfareMaximizingAllocationRule_isMonotone {I : Type u_1} [Fintype I] [DecidableEq I] (A : KnapsackAuction I ℝ) (hW : 0 ≤ A.totalCapacity) : { allocationRule := A.welfareMaximizingAllocationRule hW, paymentRule := A.welfareMaximizingPaymentRule hW }.IsMonotone

theorem KnapsackAuction.welfareMaximizingMechanism_isDSIC {I : Type u_1} [Fintype I] [DecidableEq I] (A : KnapsackAuction I ℝ) (hW : 0 ≤ A.totalCapacity) : (A.welfareMaximizingMechanism hW).IsDSIC

def KnapsackAuction.fractionalSocialWelfare {I : Type u_1} {U : Type u_2} [Field U] [Fintype I] (b x : I → U) : U

Fractional social welfare for a U-valued allocation vector.

Equations

• KnapsackAuction.fractionalSocialWelfare b x = ∑ i : I, b i * x i

def KnapsackAuction.fractionalFeasible {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [Fintype I] (A : KnapsackAuction I U) (x : I → U) : Prop

Feasibility of a fractional knapsack allocation: pointwise fractions lie in [0,1] and the weighted load respects capacity.

Equations

• A.fractionalFeasible x = ((∀ (i : I), 0 ≤ x i ∧ x i ≤ 1) ∧ ∑ i : I, A.weight i * x i ≤ A.totalCapacity)

noncomputable def KnapsackAuction.ratio {I : Type u_1} {U : Type u_2} [Field U] (A : KnapsackAuction I U) (b : I → U) (i : I) : U

Value-to-weight ratio used by the fractional greedy rule.

Equations

• A.ratio b i = b i / A.weight i

noncomputable def KnapsackAuction.ratioTieKey {I : Type u_1} {U : Type u_2} [Field U] (A : KnapsackAuction I U) (b : I → U) (i : I) : U × I

Sorting key for the fractional greedy rule: higher ratio first, ties broken by the ambient linear order on I.

Equations

• A.ratioTieKey b i = (-A.ratio b i, i)

noncomputable def KnapsackAuction.sortedAgentsByRatio {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [Fintype I] [LinearOrder I] (A : KnapsackAuction I U) (b : I → U) : List I

Agents sorted by decreasing value-to-weight ratio, with lexicographic tie-breaking via the ambient order on I.

Equations

• A.sortedAgentsByRatio b = Finset.univ.toList.mergeSort fun (i j : I) => decide (A.ratioTieKey b i ≤ A.ratioTieKey b j)

@[irreducible]

noncomputable def KnapsackAuction.fractionalGreedyList {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [DecidableEq I] (A : KnapsackAuction I U) (b : I → U) : List I → U → I → U

Greedy fractional allocation along a fixed list order. If the next item does not fully fit, the algorithm takes exactly the remaining fraction and halts.

Equations

• One or more equations did not get rendered due to their size.
• A.fractionalGreedyList b [] x✝ = fun (x : I) => 0

noncomputable def KnapsackAuction.fractionalGreedyAllocation {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [Fintype I] [DecidableEq I] [LinearOrder I] (A : KnapsackAuction I U) (b : I → U) : I → U

The greedy fractional knapsack allocation obtained by sorting agents by value-to-weight ratio and then filling capacity in that order.

Equations

• A.fractionalGreedyAllocation b = A.fractionalGreedyList b (A.sortedAgentsByRatio b) A.totalCapacity

theorem KnapsackAuction.BinaryRespectsCapacity_of_mem_feasibleBinaryAllocations {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] (A : KnapsackAuction I U) {x : BinaryAllocation I} (hx : x ∈ A.feasibleBinaryAllocations) : A.binaryRespectsCapacity x

theorem KnapsackAuction.binaryToAllocation_fractionalFeasible_of_binaryRespectsCapacity {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] (A : KnapsackAuction I U) {x : BinaryAllocation I} (hx : A.binaryRespectsCapacity x) : A.fractionalFeasible (binaryToAllocation x)

theorem KnapsackAuction.fractionalGreedyWelfare_ge_zeroOneWelfare_of_optimal {I : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] [Fintype I] [DecidableEq I] [LinearOrder I] (A : KnapsackAuction I U) (b : I → U) (hW : 0 ≤ A.totalCapacity) (hgreedyOptimal : ∀ (x : I → U), A.fractionalFeasible x → fractionalSocialWelfare b x ≤ fractionalSocialWelfare b (A.fractionalGreedyAllocation b)) : A.maximalSocialWelfare b hW ≤ fractionalSocialWelfare b (A.fractionalGreedyAllocation b)

If the ratio-sorted greedy fractional allocation is optimal for the fractional relaxation, then its welfare dominates the welfare of the optimal 0/1 knapsack allocation. This is the standard relaxation comparison: every feasible binary allocation is also a feasible fractional allocation.

def KnapsackAuction.natBinarySocialWelfare {I : Type u_1} [Fintype I] (b : I → ℕ) (x : BinaryAllocation I) : ℕ

Integer-valued welfare of a binary allocation profile.

Equations

• KnapsackAuction.natBinarySocialWelfare b x = ∑ i : I, if x i = true then b i else 0

def KnapsackAuction.natBinaryLoad {I : Type u_1} [Fintype I] (w : I → ℕ) (x : BinaryAllocation I) : ℕ

Integer-valued load of a binary allocation profile.

Equations

• KnapsackAuction.natBinaryLoad w x = ∑ i : I, if x i = true then w i else 0

def KnapsackAuction.supportedOn {I : Type u_1} (items : List I) (x : BinaryAllocation I) : Prop

An allocation is supported on a list of agents if every selected agent appears in that list.

Equations

• KnapsackAuction.supportedOn items x = ∀ (i : I), x i = true → i ∈ items

theorem KnapsackAuction.eq_false_of_supportedOn_of_not_mem {I : Type u_1} {items : List I} {x : BinaryAllocation I} (hsupp : supportedOn items x) {i : I} (hi : i ∉ items) : x i = false

theorem KnapsackAuction.supportedOn_nil_iff {I : Type u_1} {x : BinaryAllocation I} : supportedOn [] x ↔ x = fun (x : I) => false

theorem KnapsackAuction.supportedOn_tail_of_eq_false {I : Type u_1} {i : I} {items : List I} {x : BinaryAllocation I} (hsupp : supportedOn (i :: items) x) (hxi : x i = false) : supportedOn items x

theorem KnapsackAuction.supportedOn_update_false {I : Type u_1} [DecidableEq I] {i : I} {items : List I} {x : BinaryAllocation I} (hsupp : supportedOn (i :: items) x) : supportedOn items (Function.update x i false)

theorem KnapsackAuction.natBinarySocialWelfare_eq_add_of_true {I : Type u_1} [Fintype I] [DecidableEq I] (b : I → ℕ) {x : BinaryAllocation I} {i : I} (hxi : x i = true) : natBinarySocialWelfare b x = b i + natBinarySocialWelfare b (Function.update x i false)

theorem KnapsackAuction.natBinaryLoad_eq_add_of_true {I : Type u_1} [Fintype I] [DecidableEq I] (w : I → ℕ) {x : BinaryAllocation I} {i : I} (hxi : x i = true) : natBinaryLoad w x = w i + natBinaryLoad w (Function.update x i false)

theorem KnapsackAuction.natBinarySocialWelfare_update_true_of_false {I : Type u_1} [Fintype I] [DecidableEq I] (b : I → ℕ) {x : BinaryAllocation I} {i : I} (hxi : x i = false) : natBinarySocialWelfare b (Function.update x i true) = b i + natBinarySocialWelfare b x

theorem KnapsackAuction.natBinaryLoad_update_true_of_false {I : Type u_1} [Fintype I] [DecidableEq I] (w : I → ℕ) {x : BinaryAllocation I} {i : I} (hxi : x i = false) : natBinaryLoad w (Function.update x i true) = w i + natBinaryLoad w x

@[irreducible]

def KnapsackAuction.dpSolveList {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) : List I → ℕ → BinaryAllocation I

A computable dynamic-programming solver for finite 0/1 knapsack instances.

The solver processes the agents in the given list order and uses the standard "skip or take" recursion on the remaining capacity. This is the algorithmic counterpart to the abstract welfare-maximizer above, specialized to natural weights, natural capacity, and natural reported values.

Equations

• One or more equations did not get rendered due to their size.
• KnapsackAuction.dpSolveList w b [] x✝ = fun (x : I) => false

theorem KnapsackAuction.dpSolveList_supportedOn {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (items : List I) (capacity : ℕ) : supportedOn items (dpSolveList w b items capacity)

theorem KnapsackAuction.dpSolveList_feasible {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (items : List I) : items.Nodup → ∀ (capacity : ℕ), natBinaryLoad w (dpSolveList w b items capacity) ≤ capacity

theorem KnapsackAuction.dpSolveList_optimal {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (items : List I) : items.Nodup → ∀ (capacity : ℕ) {x : BinaryAllocation I}, supportedOn items x → natBinaryLoad w x ≤ capacity → natBinarySocialWelfare b x ≤ natBinarySocialWelfare b (dpSolveList w b items capacity)

noncomputable def KnapsackAuction.dynamicProgrammingOptimalAllocation {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (capacity : ℕ) : BinaryAllocation I

The computable knapsack allocation obtained by running the dynamic program on the full finite agent list.

Equations

• KnapsackAuction.dynamicProgrammingOptimalAllocation w b capacity = KnapsackAuction.dpSolveList w b Finset.univ.toList capacity

noncomputable def KnapsackAuction.dynamicProgrammingOptimalValue {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (capacity : ℕ) : ℕ

The social welfare achieved by the dynamic-programming allocation.

Equations

• KnapsackAuction.dynamicProgrammingOptimalValue w b capacity = KnapsackAuction.natBinarySocialWelfare b (KnapsackAuction.dynamicProgrammingOptimalAllocation w b capacity)

theorem KnapsackAuction.dynamicProgrammingOptimalAllocation_feasible {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (capacity : ℕ) : natBinaryLoad w (dynamicProgrammingOptimalAllocation w b capacity) ≤ capacity

The dynamic-programming allocation always satisfies the knapsack capacity constraint in the natural-number specialization.

theorem KnapsackAuction.dynamicProgrammingOptimalAllocation_optimal {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (capacity : ℕ) {x : BinaryAllocation I} (hfeas : natBinaryLoad w x ≤ capacity) : natBinarySocialWelfare b x ≤ natBinarySocialWelfare b (dynamicProgrammingOptimalAllocation w b capacity)

The dynamic-programming allocation maximizes integer social welfare among all feasible binary allocations.

def KnapsackAuction.natAuctionData {I : Type u_1} (w : I → ℕ) (capacity : ℕ) : KnapsackAuction I ℝ

The knapsack-auction data obtained from natural-number weights and capacity, with dummy zero allocation/payment rules. This is only used to instantiate the fractional greedy construction.

Equations

• One or more equations did not get rendered due to their size.

def KnapsackAuction.realBidOfNat {I : Type u_1} (b : I → ℕ) : I → ℝ

Natural-number bids viewed as real-valued bids.

Equations

• KnapsackAuction.realBidOfNat b i = ↑(b i)

@[irreducible]

def KnapsackAuction.integralGreedyList {I : Type u_1} [DecidableEq I] (w : I → ℕ) : List I → ℕ → BinaryAllocation I

The integral greedy prefix algorithm: process items in a fixed order, take each whole item if it fits, and halt when the first item fails to fit.

Equations

• KnapsackAuction.integralGreedyList w [] x✝ = fun (x : I) => false
• KnapsackAuction.integralGreedyList w (i :: is) x✝ = if w i ≤ x✝ then Function.update (KnapsackAuction.integralGreedyList w is (x✝ - w i)) i true else fun (x : I) => false

noncomputable def KnapsackAuction.integralGreedyAllocation {I : Type u_1} [Fintype I] [DecidableEq I] [LinearOrder I] (w b : I → ℕ) (capacity : ℕ) : BinaryAllocation I

The ratio-sorted integral greedy allocation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KnapsackAuction.integralGreedyValue {I : Type u_1} [Fintype I] [DecidableEq I] [LinearOrder I] (w b : I → ℕ) (capacity : ℕ) : ℕ

Welfare of the ratio-sorted integral greedy allocation.

Equations

• KnapsackAuction.integralGreedyValue w b capacity = KnapsackAuction.natBinarySocialWelfare b (KnapsackAuction.integralGreedyAllocation w b capacity)

noncomputable def KnapsackAuction.highestBidValue {I : Type u_1} [Fintype I] [Nonempty I] (b : I → ℕ) : ℕ

Highest single-item value.

Equations

• KnapsackAuction.highestBidValue b = Finset.univ.sup' ⋯ b

theorem KnapsackAuction.le_highestBidValue {I : Type u_1} [Fintype I] [Nonempty I] (b : I → ℕ) (i : I) : b i ≤ highestBidValue b

theorem KnapsackAuction.fractionalSocialWelfare_realBidOfNat_binaryToAllocation {I : Type u_1} [Fintype I] (b : I → ℕ) (x : BinaryAllocation I) : fractionalSocialWelfare (realBidOfNat b) (binaryToAllocation x) = ↑(natBinarySocialWelfare b x)

@[irreducible]

noncomputable def KnapsackAuction.natFractionalGreedyList {I : Type u_1} [DecidableEq I] (w : I → ℕ) : List I → ℕ → I → ℝ

Fractional greedy prefix algorithm on a natural-number remaining capacity: take each whole item if it fits, and otherwise take exactly the remaining fraction of the current item and halt.

Equations

• One or more equations did not get rendered due to their size.
• KnapsackAuction.natFractionalGreedyList w [] x✝ = fun (x : I) => 0

noncomputable def KnapsackAuction.natFractionalGreedyAllocation {I : Type u_1} [Fintype I] [DecidableEq I] [LinearOrder I] (w b : I → ℕ) (capacity : ℕ) : I → ℝ

The ratio-sorted fractional greedy allocation on natural-number data.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KnapsackAuction.natFractionalGreedyValue {I : Type u_1} [Fintype I] [DecidableEq I] [LinearOrder I] (w b : I → ℕ) (capacity : ℕ) : ℝ

Welfare of the ratio-sorted fractional greedy allocation.

Equations

• KnapsackAuction.natFractionalGreedyValue w b capacity = KnapsackAuction.fractionalSocialWelfare (KnapsackAuction.realBidOfNat b) (KnapsackAuction.natFractionalGreedyAllocation w b capacity)

def KnapsackAuction.fractionalSupportedOn {I : Type u_1} (items : List I) (x : I → ℝ) : Prop

A real-valued allocation is supported on a list if every nonzero coordinate appears in that list.

Equations

• KnapsackAuction.fractionalSupportedOn items x = ∀ (i : I), x i ≠ 0 → i ∈ items

theorem KnapsackAuction.eq_zero_of_fractionalSupportedOn_of_not_mem {I : Type u_1} {items : List I} {x : I → ℝ} (hsupp : fractionalSupportedOn items x) {i : I} (hi : i ∉ items) : x i = 0

theorem KnapsackAuction.integralGreedyList_supportedOn {I : Type u_1} [DecidableEq I] (w : I → ℕ) (items : List I) (remaining : ℕ) : supportedOn items (integralGreedyList w items remaining)

theorem KnapsackAuction.natFractionalGreedyList_supportedOn {I : Type u_1} [DecidableEq I] (w : I → ℕ) (items : List I) (remaining : ℕ) : fractionalSupportedOn items (natFractionalGreedyList w items remaining)

theorem KnapsackAuction.fractionalSocialWelfare_update_one_of_zero {I : Type u_1} [Fintype I] [DecidableEq I] (b : I → ℝ) {x : I → ℝ} {i : I} (hxi : x i = 0) : fractionalSocialWelfare b (Function.update x i 1) = b i + fractionalSocialWelfare b x

theorem KnapsackAuction.fractionalSocialWelfare_singleton {I : Type u_1} [Fintype I] [DecidableEq I] (b : I → ℝ) (i : I) (α : ℝ) : (fractionalSocialWelfare b fun (j : I) => if j = i then α else 0) = b i * α

theorem KnapsackAuction.natFractionalGreedyList_le_integralGreedyList_plus_highest {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] (w b : I → ℕ) (hwpos : ∀ (i : I), 0 < w i) {items : List I} : items.Nodup → ∀ (remaining : ℕ), fractionalSocialWelfare (realBidOfNat b) (natFractionalGreedyList w items remaining) ≤ ↑(natBinarySocialWelfare b (integralGreedyList w items remaining)) + ↑(highestBidValue b)

theorem KnapsackAuction.natFractionalGreedyValue_le_integralGreedyValue_plus_highest {I : Type u_1} [Fintype I] [DecidableEq I] [LinearOrder I] [Nonempty I] (w b : I → ℕ) (capacity : ℕ) (hwpos : ∀ (i : I), 0 < w i) : natFractionalGreedyValue w b capacity ≤ ↑(integralGreedyValue w b capacity) + ↑(highestBidValue b)

theorem KnapsackAuction.dynamicProgrammingOptimalAllocation_fractionalFeasible {I : Type u_1} [Fintype I] [DecidableEq I] (w b : I → ℕ) (capacity : ℕ) : (natAuctionData w capacity).fractionalFeasible (binaryToAllocation (dynamicProgrammingOptimalAllocation w b capacity))

theorem KnapsackAuction.integralGreedy_halfApprox_dpOptimal {I : Type u_1} [Fintype I] [DecidableEq I] [LinearOrder I] [Nonempty I] (w b : I → ℕ) (capacity : ℕ) (hwpos : ∀ (i : I), 0 < w i) (_hallfit : ∀ (i : I), w i ≤ capacity) (hfracOptimal : ∀ (x : I → ℝ), (natAuctionData w capacity).fractionalFeasible x → fractionalSocialWelfare (realBidOfNat b) x ≤ natFractionalGreedyValue w b capacity) : ↑(dynamicProgrammingOptimalValue w b capacity) / 2 ≤ ↑(max (integralGreedyValue w b capacity) (highestBidValue b))

The ratio-sorted integral greedy algorithm, compared with the highest single-value item, achieves a 1/2-approximation to the DP-optimal 0/1 knapsack welfare, provided the fractional greedy allocation is optimal for the fractional relaxation and every item fits individually in the knapsack.