noncomputable def SX.fee.z (φ x y r0 : ℝ>0) : ℝ>0

Equations

• SX.fee.z φ x y r0 = (x + y) * (r0 + φ * x) * (r0 + x + φ * y) / ((r0 + φ * x + φ * y) * (x ^ 2 + r0 * x + φ * x * y + r0 * y))

noncomputable def SX.fee.z_extended (φ x y r0 r1 : ℝ>0) : ℝ>0

Equations

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

theorem SX.fee.z_toReal (φ x y r0 : ℝ>0) : ↑(z φ x y r0) = (↑x + ↑y) * (↑r0 + ↑φ * ↑x) * (↑r0 + ↑x + ↑φ * ↑y) / ((↑r0 + ↑φ * ↑x + ↑φ * ↑y) * (↑x ^ 2 + ↑r0 * ↑x + ↑φ * ↑x * ↑y + ↑r0 * ↑y))

theorem SX.fee.z_eq_z_extended (φ x y r0 r1 : ℝ>0) : z φ x y r0 = z_extended φ x y r0 r1

def SX.fee.extended_additivity (φ : ℝ>0) (sx : SX) : Prop

Equations

• SX.fee.extended_additivity φ sx = ∀ (x y r0 r1 : ℝ>0) (ho : sx.outputbound), sx (x + y) r0 r1 = (x * sx x r0 r1 + y * sx y (r0 + x) (r1.sub (x * sx x r0 r1) ⋯)) / (x + y) * SX.fee.z φ x y r0

theorem SX.fee.z_factor_gt_1 (φ : ℝ>0) {x y r0 : ℝ>0} (hφ : φ < 1) : z φ x y r0 > 1

noncomputable def SX.fee.εφ (φ : ℝ>0) {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (hφ : φ < 1) (o : T → ℝ>0) (h_supply : s.mints.supply t0 t1 > 0) (h_mint : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) : ℝ>0

Equations

• SX.fee.εφ φ sw0 sw1 hφ o h_supply h_mint = o t1 * (SX.fee.z φ x₀ x₁ (s.amms.r0 t0 t1 ⋯)).sub 1 ⋯ * (sw0.y + sw1.y) * Swap.fee.frac_gain_Rpos s h_supply h_mint

noncomputable def SX.fee.εφ_toReal (φ : ℝ>0) {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ r0 r1 α : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (hφ : φ < 1) (hr0 : r0 = s.amms.r0 t0 t1 ⋯) (hr1 : r1 = s.amms.r1 t0 t1 ⋯) (hα : α = sx x₀ r0 r1) (o : T → ℝ>0) (h_supply : s.mints.supply t0 t1 > 0) (h_mint : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) : ↑(εφ φ sw0 sw1 hφ o h_supply h_mint) = ↑(o t1) * (↑(z φ x₀ x₁ r0) - 1) * (↑x₀ * ↑α + ↑sw1.y) * ↑(Swap.fee.frac_gain_Rpos s h_supply h_mint)

Equations

• ⋯ = ⋯

theorem sub_eq_iff_add_eq (a b c : ℝ) (h : a - b = c) : a = b + c

theorem SX.fee.additive_gain (φ : ℝ>0) {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (sw2 : Swap sx s a t0 t1 (x₀ + x₁)) (addi : extended_additivity φ sx) (out_b : sx.outputbound) (h_supply : s.mints.supply t0 t1 > 0) (h_mint : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) (hφ : φ < 1) (o : T → ℝ>0) : a.gain o s sw2.apply = a.gain o s sw0.apply + a.gain o sw0.apply sw1.apply + ↑(εφ φ sw0 sw1 hφ o h_supply h_mint)