@[simp]

theorem swap_price_mint_diff {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) (o : O) (t0' t1' : T) (init : s.amms.init t0' t1') (hdif : diffmint t0 t1 t0' t1') : sw.apply.mintedprice o t0' t1' = s.mintedprice o t0' t1'

@[simp]

theorem Swap.networth_erase {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : (sw.apply.mints.get a).drain t0 t1 ⋯ = (s.mints.get a).drain t0 t1 ⋯

theorem Swap.atoms_drain_drain_worth {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) (o : O) : (((sw.apply.atoms.get a).drain t0).drain t1).worth o = (((s.atoms.get a).drain t0).drain t1).worth o

@[simp]

theorem Swap.worth_wallet_without_minted {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) (o : O) (w : W₁) (h : w.get t0 t1 = 0) : w.worth (sw.apply.mintedprice o) = w.worth (s.mintedprice o)

theorem expandprice (s : Γ) (o : O) (t0 t1 : T) (init : s.amms.init t0 t1) : s.mintedprice o t0 t1 = (↑(s.amms.r0 t0 t1 init) * ↑(o t0) + ↑(s.amms.r1 t0 t1 init) * ↑(o t1)) / s.mints.supply t0 t1

theorem Swap.self_gain_eq {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap sx s a t0 t1 x) (o : O) : a.gain o s sw.apply = (↑sw.y * ↑(o t1) - ↑x * ↑(o t0)) * (1 - ↑((s.mints.get a).get t0 t1) / ↑(s.mints.supply t0 t1))

theorem Swap.swaprate_vs_exchrate {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap sx s a t0 t1 x) (o : O) (hzero : (s.mints.get a).get t0 t1 = 0) : cmp (a.gain o s sw.apply) 0 = cmp sw.rate (o t0 / o t1)

theorem Swap.swaprate_vs_exchrate_lt {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) (o : O) (hzero : (s.mints.get a).get t0 t1 = 0) : a.gain o s sw.apply < 0 ↔ sw.rate < o t0 / o t1

theorem Swap.swaprate_vs_exchrate_gt {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) (o : O) (hzero : (s.mints.get a).get t0 t1 = 0) : 0 < a.gain o s sw.apply ↔ o t0 / o t1 < sw.rate

def Swap.swappedtoks {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) {x : ℝ>0} (henough : ↑x ≤ (s.atoms.get a) t1) (nodrain : x * sx x (s.amms.r0 t1 t0 ⋯) (s.amms.r1 t1 t0 ⋯) < s.amms.r1 t1 t0 ⋯) : Swap sx s a t1 t0 x

Equations

• ⋯ = ⋯