def «tacticCustom_have_:_:=_» : Lean.ParserDescr

Equations

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

def «tacticCustom_let_:_:=_» : Lean.ParserDescr

Equations

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

def tacticSet_and_subst_reserves____ : Lean.ParserDescr

Equations

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

def tacticSet_and_subst_α_β__ : Lean.ParserDescr

Equations

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

def tacticSet_reserves____ : Lean.ParserDescr

Equations

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

def tacticSet_reserves_with_eqs____ : Lean.ParserDescr

Equations

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

def tacticSubst_reserves___ : Lean.ParserDescr

Equations

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

theorem Swap.fee.valid_sw_y_lt_r1 {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap sx s a t0 t1 x) : ↑sw.y ≤ ↑(s.amms.r1 t0 t1 ⋯)

theorem Swap.fee.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.fee.self_gain_no_mint_eq {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap sx s a t0 t1 x) (no_mint : (s.mints.get a).get t0 t1 = 0) (o : O) : a.gain o s sw.apply = ↑sw.y * ↑(o t1) - ↑x * ↑(o t0)

theorem Swap.fee.same_wall_diff_act {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} {b : A} (sw : Swap sx s a t0 t1 x) : O → ∀ (h_dif : a ≠ b), s.atoms.get b = sw.apply.atoms.get b

theorem Swap.fee.swap_apply_amm_exi {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap sx s a t0 t1 x) : sw.apply.amms.init t0 t1

theorem Swap.r0_after_swap {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap sx s a t0 t1 x) : sw.apply.amms.r0 t0 t1 ⋯ = s.amms.r0 t0 t1 ⋯ + x

theorem Swap.r1_after_swap {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} (sw : Swap sx s a t0 t1 x) : sw.apply.amms.r1 t0 t1 ⋯ = (s.amms.r1 t0 t1 ⋯).sub (x * sx x (s.amms.r0 t0 t1 ⋯) (s.amms.r1 t0 t1 ⋯)) ⋯

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

theorem Swap.fee.frac_gain_pos {t0 t1 : T} {a : A} (s : Γ) (h_supply : s.mints.supply t0 t1 > 0) (h_mint : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) : 1 - ↑((s.mints.get a).get t0 t1) / ↑(s.mints.supply t0 t1) > 0

noncomputable def Swap.fee.frac_gain_Rpos {t0 t1 : T} {a : A} (s : Γ) (h_supply : s.mints.supply t0 t1 > 0) (h_mint : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) : ℝ>0

Equations

• Swap.fee.frac_gain_Rpos s h_supply h_mint = ⟨1 - ↑((s.mints.get a).get t0 t1) / ↑(s.mints.supply t0 t1), ⋯⟩

theorem Swap.fee.frac_gain_Rpos_toReal {t0 t1 : T} {a : A} (s : Γ) (h_supply : s.mints.supply t0 t1 > 0) (h_mint : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) : ↑(frac_gain_Rpos s h_supply h_mint) = 1 - ↑((s.mints.get a).get t0 t1) / ↑(s.mints.supply t0 t1)

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

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

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