noncomputable def SX.constprod : SX

Equations

• SX.constprod x r0 r1 = r1 / (r0 + x)

def SX.constprod.outputbound : constprod.outputbound

Equations

• SX.constprod.outputbound = ⋯

def SX.constprod.reversible : constprod.reversible outputbound

Equations

• SX.constprod.reversible = ⋯

theorem SX.constprod.homogeneous : constprod.homogeneous

theorem SX.constprod.strictmono : constprod.strictmono

theorem SX.constprod.additive : constprod.additive

theorem SX.constprod.exchrate_vs_oracle (x r0 r1 p0 p1 : ℝ>0) (h : p0 / p1 ≤ constprod x r0 r1) (y : ℝ>0) : constprod y r1 r0 < p1 / p0

theorem SX.constprod.gain_direction {s : Γ} {a : A} {t0 t1 : T} {x x' : ℝ>0} (sw1 : Swap constprod s a t0 t1 x) (sw2 : Swap constprod s a t1 t0 x') (o : O) (hzero : (s.mints.get a).get t0 t1 = 0) (hgain : 0 < a.gain o s sw1.apply) : a.gain o s sw2.apply < 0

theorem SX.constprod.optimality_suff {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw1 : Swap constprod s a t0 t1 x₀) (o : O) (h : sw1.apply.amms.r1 t0 t1 ⋯ / sw1.apply.amms.r0 t0 t1 ⋯ = o t0 / o t1) : sw1.is_solution o

theorem SX.constprod.arbitrage_solve {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw : Swap constprod s a t0 t1 x₀) (o : O) (less : s.amms.r0 t0 t1 ⋯ < (o t1 * (o t0)⁻¹ * s.amms.r0 t0 t1 ⋯ * s.amms.r1 t0 t1 ⋯).sqrt) (h : x₀ = (o t1 * (o t0)⁻¹ * s.amms.r0 t0 t1 ⋯ * s.amms.r1 t0 t1 ⋯).sqrt.sub (s.amms.r0 t0 t1 ⋯) less) : sw.is_solution o