Proposition 2 — the constant rate λ^D = min{λ*, x/t} solves the deterministic problem (11); J^D(x,t) = t r(λ^D)
ProvedGVRPricing.FixedPrice.deterministic_solutionLet be a regular demand function, a stock and a horizon. Write for the run-out rate, and , and set
Then:
- the constant path , , is feasible for the deterministic problem (11);
- it is optimal: every feasible rate path satisfies ;
- the optimal revenue is
which equals when , and when ; 4. in terms of price, (when , and , so that both prices are finite).
If items are plentiful () the firm prices at the revenue-maximizing level; if they are scarce it prices to sell exactly its stock. This solution supplies the fixed-price heuristic and the value against which Theorems 2 and 3 compare the stochastic problem.
Formalization Note The page prints (eq. (12)) without a case distinction. That is wrong when : there , so , while the optimum is . For exponential demand with , but . The statement gives the corrected value , and the printed form in the case , where it is right. The page calls "the" optimal solution; under concavity alone it need not be unique, so the statement asserts optimality, not uniqueness. When the run-out quantities , are undefined, and the statement uses them only where . The OCR's "" is a typesetting slip for .
import Mathlib import Definitions.Def_GVRPricing_FixedPrice_Model import Definitions.Def_GVRPricing_FixedPrice_Deterministic open MeasureTheory Set
namespace GVRPricing.FixedPrice
/-- **Proposition 2** (p. 1006), with the value (12) corrected. For a stock `x ≥ 0` and a
horizon `t > 0`, with run-out rate `λ⁰ = x/t` and `λ^D = min{λ*, λ⁰}`:
1. the constant path `λ(s) = λ^D` is feasible for (11);
2. it is optimal: every feasible rate path earns at most `∫_0^t r(λ^D) ds`;
3. the optimal revenue is `J^D(x, t) = t r(λ^D)`, which equals `t min{r*, r⁰}` (`r⁰ = r(λ⁰)`)
when `x ≤ λ* t` and `t r*` when `x ≥ λ* t` (the printed `t min{r*, r⁰}` is wrong for
`x > λ* t`, where `r⁰ ≤ r*`);
4. in terms of price, `p^D = p(λ^D) = max{p*, p⁰}` whenever both prices are finite
(`λ* > 0`, `x > 0`, `λ⁰ ∈ Λ`). -/
theorem deterministic_solution (M : Model) (x t : ℝ) (hx : 0 ≤ x) (ht : 0 < t) :
IsFeasiblePath M x t (fun _ => min M.lstar (x / t)) ∧
(∀ ℓ : ℝ → ℝ, IsFeasiblePath M x t ℓ →
∫ s in (0 : ℝ)..t, M.r (ℓ s) ≤ ∫ s in (0 : ℝ)..t, M.r (min M.lstar (x / t))) ∧
detValue M x t = t * M.r (min M.lstar (x / t)) ∧
(x ≤ M.lstar * t → detValue M x t = t * min M.rstar (M.r (x / t))) ∧
(M.lstar * t ≤ x → detValue M x t = t * M.rstar) ∧
(0 < M.lstar → 0 < x → x / t ∈ M.Λ →
M.p (min M.lstar (x / t)) = max M.pstar (M.p (x / t))) := by sorry
end GVRPricing.FixedPrice
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.