Fundamental theorem of asset pricing

TheoremFundamental theorem of asset pricing for a finite one-period market#✓fully proved

Let \(\Omega\) be a nonempty finite set of states and \(A\) a finite set of assets, and let \(g(a, \omega) \in \mathbb{R}\) be the gain of asset \(a\) in state \(\omega\). Call a portfolio \(h \colon A \to \mathbb{R}\) an arbitrage if its gain \(\sum_{a \in A} h(a)\, g(a, \omega)\) is nonnegative in every state \(\omega\) and positive in some state. There is no arbitrage if and only if there is a function \(q \colon \Omega \to \mathbb{R}\) with \(q(\omega) > 0\) for every \(\omega \in \Omega\) and \(\sum_{\omega \in \Omega} q(\omega) = 1\) such that \(\sum_{\omega \in \Omega} q(\omega)\, g(a, \omega) = 0\) for every asset \(a \in A\).

theorem one_period_fundamental_theorem_asset_pricing_general
    {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    {A : Type*} [Fintype A]
    (g : A → Ω → ℝ) :
    (¬ ∃ h : A → ℝ, (∀ ω : Ω, 0 ≤ ∑ a : A, h a * g a ω) ∧
      (∃ ω : Ω, 0 < ∑ a : A, h a * g a ω)) ↔
    ∃ q : Ω → ℝ, (∀ ω : Ω, 0 < q ω) ∧ (∑ ω : Ω, q ω = 1) ∧
      (∀ a : A, ∑ ω : Ω, q ω * g a ω = 0)

Used by 1

Used byOne-period fundamental theorem of asset pricing

TheoremOne-period fundamental theorem of asset pricing#✓fully proved

Let \(\Omega\) be a nonempty finite set of states and \(A\) a finite set of assets, and let \(g(a, \omega) \in \mathbb{R}\) be the gain of asset \(a\) in state \(\omega\). Call a portfolio \(h \colon A \to \mathbb{R}\) an arbitrage if its gain \(\sum_{a \in A} h(a)\, g(a, \omega)\) is nonnegative in every state \(\omega\) and positive in some state. There is no arbitrage if and only if there is a function \(q \colon \Omega \to \mathbb{R}\) with \(q(\omega) > 0\) for every \(\omega \in \Omega\) and \(\sum_{\omega \in \Omega} q(\omega) = 1\) such that \(\sum_{\omega \in \Omega} q(\omega)\, g(a, \omega) = 0\) for every asset \(a \in A\), that is, a strictly positive probability on the states under which every asset has zero expected gain.

theorem one_period_fundamental_theorem_asset_pricing
    {Ω : Type*} [Fintype Ω] [DecidableEq Ω] [Nonempty Ω]
    {A : Type*} [Fintype A] [DecidableEq A]
    (g : A → Ω → ℝ) :
    (¬ ∃ h : A → ℝ, (∀ ω : Ω, 0 ≤ ∑ a : A, h a * g a ω) ∧
      (∃ ω : Ω, 0 < ∑ a : A, h a * g a ω)) ↔
    ∃ q : Ω → ℝ, (∀ ω : Ω, 0 < q ω) ∧ (∑ ω : Ω, q ω = 1) ∧
      (∀ a : A, ∑ ω : Ω, q ω * g a ω = 0)

Sources

• J. M. Harrison and D. M. Kreps, J. Econom. Theory 20 (1979), DOI 10.1016/0022-0531(79)90043-7. It follows from one_period_fundamental_theorem_asset_pricing_general; the unused [DecidableEq Ω] and [DecidableEq A] keep the source's shape.

Uses 1

Proof usesFundamental theorem of asset pricing for a finite one-period market

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.