noncomputable def SX.fee.constprod (φ : ℝ>0) : SX

Equations

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

theorem SX.fee.constprod.outputbound (φ : ℝ>0) : (constprod φ).outputbound

theorem SX.fee.constprod.homogeneous (φ : ℝ>0) : (constprod φ).homogeneous

theorem SX.fee.constprod.strictmono (φ : ℝ>0) : (constprod φ).strictmono

theorem Swap.constprod.mkSwap (φ : ℝ>0) (s : Γ) (a : A) (t0 t1 : T) (x : ℝ>0) (h_init : s.amms.init t0 t1) (h_enoguh : ↑x ≤ (s.atoms.get a) t0) : Swap (SX.fee.constprod φ) s a t0 t1 x

theorem SX.fee.constprod.φ_r1_sub_α_x_simp (φ x r0 r1 : ℝ>0) (h : x * (φ * r1 / (r0 + φ * x)) < r1) : φ * r1.sub (x * (φ * r1 / (r0 + φ * x))) h = φ * r0 * r1 / (r0 + φ * x)

theorem SX.fee.constprod.rate_toReal (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) : ↑sw0.rate = ↑φ * ↑(s.amms.r1 t0 t1 ⋯) / (↑(s.amms.r0 t0 t1 ⋯) + ↑φ * ↑x₀)

theorem SX.fee.constprod.beta_simp (φ x y r0 r1 : ℝ>0) (h : x * constprod φ x r0 r1 < r1) : constprod φ y (r0 + x) (r1.sub (x * constprod φ x r0 r1) h) = φ * r1 * r0 / ((r0 + φ * x) * (r0 + x + φ * y))

theorem SX.fee.constprod.beta_simp_rate (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (sw1 : Swap (constprod φ) sw0.apply a t0 t1 x₁) : x₁ * sw1.rate = φ * s.amms.r1 t0 t1 ⋯ * s.amms.r0 t0 t1 ⋯ * x₁ / ((s.amms.r0 t0 t1 ⋯ + φ * x₀) * (s.amms.r0 t0 t1 ⋯ + x₀ + φ * x₁))

theorem SX.fee.constprod.extended_additivity (φ : ℝ>0) : fee.extended_additivity φ (constprod φ)

noncomputable def SX.fee.constprod.int_rate (φ r0 r1 : ℝ>0) : ℝ>0

Equations

• SX.fee.constprod.int_rate φ r0 r1 = φ * r1 / r0

noncomputable def SX.fee.constprod.sw_to_equil (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (o : O) : Prop

Equations

• SX.fee.constprod.sw_to_equil φ sw0 o = (SX.fee.constprod.int_rate φ (sw0.apply.amms.r0 t0 t1 ⋯) (sw0.apply.amms.r1 t0 t1 ⋯) = o t0 / o t1)

def SX.fee.constprod.int_rate_strictmono (φ : ℝ>0) : Prop

Equations

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

theorem SX.fee.constprod.int_rate_is_strictmono (φ : ℝ>0) : int_rate_strictmono φ

theorem SX.fee.constprod.int_rate_gt_sx_rate_pre_swap (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap (constprod φ) s a t0 t1 x) : sw.rate < int_rate φ (s.amms.r0 t0 t1 ⋯) (s.amms.r1 t0 t1 ⋯)

theorem SX.fee.constprod.sx_rate_gt_int_rate_post_swap (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap (constprod φ) s a t0 t1 x) (hφ : φ ≤ 1) : sw.rate > int_rate φ (sw.apply.amms.r0 t0 t1 ⋯) (sw.apply.amms.r1 t0 t1 ⋯)

theorem SX.fee.constprod.sx_rate_vs_int_rate (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap (constprod φ) s a t0 t1 x) (hφ : φ ≤ 1) : constprod φ x (s.amms.r0 t0 t1 ⋯) (s.amms.r1 t0 t1 ⋯) > int_rate φ (sw.apply.amms.r0 t0 t1 ⋯) (sw.apply.amms.r1 t0 t1 ⋯) ∧ constprod φ x (s.amms.r0 t0 t1 ⋯) (s.amms.r1 t0 t1 ⋯) < int_rate φ (s.amms.r0 t0 t1 ⋯) (s.amms.r1 t0 t1 ⋯)

theorem SX.fee.constprod.r1_lt_split_after_swap (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ x₂ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (sw1 : Swap (constprod φ) s a t0 t1 x₁) (sw2 : Swap (constprod φ) sw1.apply a t0 t1 x₂) (hφ : φ < 1) (h_split : x₀ = x₁ + x₂) : sw0.apply.amms.r1 t0 t1 ⋯ < sw2.apply.amms.r1 t0 t1 ⋯

theorem SX.fee.constprod.int_rate_lt_split (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ x₂ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (sw1 : Swap (constprod φ) s a t0 t1 x₁) (sw2 : Swap (constprod φ) sw1.apply a t0 t1 x₂) (hφ : φ < 1) (h_split : x₀ = x₁ + x₂) : int_rate φ (sw2.apply.amms.r0 t0 t1 ⋯) (sw2.apply.amms.r1 t0 t1 ⋯) > int_rate φ (sw0.apply.amms.r0 t0 t1 ⋯) (sw0.apply.amms.r1 t0 t1 ⋯)

theorem SX.fee.constprod.additive_int_rate_vs_ext_rate (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ x₂ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (sw1 : Swap (constprod φ) s a t0 t1 x₁) (sw2 : Swap (constprod φ) sw1.apply a t0 t1 x₂) (o : O) (hφ : φ < 1) (h_equil : int_rate φ (sw0.apply.amms.r0 t0 t1 ⋯) (sw0.apply.amms.r1 t0 t1 ⋯) = o t0 / o t1) (h_split : x₀ = x₁ + x₂) : o t0 / o t1 < int_rate φ (sw2.apply.amms.r0 t0 t1 ⋯) (sw2.apply.amms.r1 t0 t1 ⋯)