def
SX.fee.arbitrage.is_solution
(φ : ℝ>0)
{sx : SX}
{s : Γ}
{a : A}
{t0 t1 : T}
{x₀ : ℝ>0}
(sw : Swap sx s a t0 t1 x₀)
(o : O)
:
Equations
- SX.fee.arbitrage.is_solution φ sw o = (SX.fee.arbitrage.is_solution_less sw o ∧ SX.fee.arbitrage.is_solution_more φ sw o)
Instances For
theorem
SX.fee.arbitrage.add_gain_εφ_neg
(φ : ℝ>0)
{s : Γ}
{a : A}
{t0 t1 : T}
{x₀ x x₁ : ℝ>0}
{hφ : φ < 1}
{h_supply : s.mints.supply t0 t1 > 0}
{h_mints : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1}
(sw0 : Swap (constprod φ) s a t0 t1 x₀)
:
Swap (constprod φ) s a t0 t1 x →
∀ (sw2 : Swap (constprod φ) sw0.apply a t0 t1 x₁) (h_split : x = x₀ + x₁) (o : O)
(h_equil : constprod.int_rate φ (sw0.apply.amms.r0 t0 t1 ⋯) (sw0.apply.amms.r1 t0 t1 ⋯) = o t0 / o t1),
a.gain o sw0.apply sw2.apply + ↑(εφ φ sw0 sw2 hφ o h_supply h_mints) < 0 ↔ x > x₀ / φ
theorem
SX.fee.arbitrage.add_gain_εφ_pos
(φ : ℝ>0)
{s : Γ}
{a : A}
{t0 t1 : T}
{x₀ x x₁ : ℝ>0}
{hφ : φ < 1}
{h_supply : s.mints.supply t0 t1 > 0}
{h_mints : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1}
(sw0 : Swap (constprod φ) s a t0 t1 x₀)
:
Swap (constprod φ) s a t0 t1 x →
∀ (sw2 : Swap (constprod φ) sw0.apply a t0 t1 x₁) (h_split : x = x₀ + x₁) (o : O)
(h_equil : constprod.int_rate φ (sw0.apply.amms.r0 t0 t1 ⋯) (sw0.apply.amms.r1 t0 t1 ⋯) = o t0 / o t1),
a.gain o sw0.apply sw2.apply + ↑(εφ φ sw0 sw2 hφ o h_supply h_mints) > 0 ↔ x < x₀ / φ
theorem
SX.fee.arbitrage.constprod.equil_value
(φ : ℝ>0)
{s : Γ}
{a : A}
{t0 t1 : T}
{x₀ : ℝ>0}
(sw0 : Swap (constprod φ) s a t0 t1 x₀)
(o : O)
(hφ : φ < 1)
(h_pos :
(o t0).sqrt * s.amms.r0 t0 t1 ⋯ * (1 + φ) < (s.amms.r0 t0 t1 ⋯).sqrt * (o t0 * s.amms.r0 t0 t1 ⋯ * ⟨(↑φ - 1) ^ 2, ⋯⟩ + ⟨4, ⋯⟩ * o t1 * s.amms.r1 t0 t1 ⋯ * φ ^ 2).sqrt)
(h0 :
x₀ = ((s.amms.r0 t0 t1 ⋯).sqrt * (o t0 * s.amms.r0 t0 t1 ⋯ * ⟨(↑φ - 1) ^ 2, ⋯⟩ + ⟨4, ⋯⟩ * o t1 * s.amms.r1 t0 t1 ⋯ * φ ^ 2).sqrt).sub
((o t0).sqrt * s.amms.r0 t0 t1 ⋯ * (1 + φ)) h_pos / (⟨2, ⋯⟩ * (o t0).sqrt * φ))
:
theorem
SX.fee.arbitrage.constprod.equil_value_solution_arbitrage
(φ : ℝ>0)
{s : Γ}
{a : A}
{t0 t1 : T}
{x₀ : ℝ>0}
(sw0 : Swap (constprod φ) s a t0 t1 x₀)
(o : O)
(hφ : φ < 1)
(h_pos :
(o t0).sqrt * s.amms.r0 t0 t1 ⋯ * (1 + φ) < (s.amms.r0 t0 t1 ⋯).sqrt * (o t0 * s.amms.r0 t0 t1 ⋯ * ⟨(↑φ - 1) ^ 2, ⋯⟩ + ⟨4, ⋯⟩ * o t1 * s.amms.r1 t0 t1 ⋯ * φ ^ 2).sqrt)
(h0 :
x₀ = ((s.amms.r0 t0 t1 ⋯).sqrt * (o t0 * s.amms.r0 t0 t1 ⋯ * ⟨(↑φ - 1) ^ 2, ⋯⟩ + ⟨4, ⋯⟩ * o t1 * s.amms.r1 t0 t1 ⋯ * φ ^ 2).sqrt).sub
((o t0).sqrt * s.amms.r0 t0 t1 ⋯ * (1 + φ)) h_pos / (⟨2, ⋯⟩ * (o t0).sqrt * φ))
:
is_solution φ sw0 o