theorem SX.fee.constprod.x_max_pos_cond (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (o : O) (h_equil : sw_to_equil φ sw0 o) (hφ : φ < 1) : (o t0).sqrt * (s.amms.r0 t0 t1 ⋯ + φ * x₀) < (o t1 * φ * s.amms.r0 t0 t1 ⋯ * s.amms.r1 t0 t1 ⋯).sqrt

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

Equations

• SX.fee.constprod.x_max' φ sw0 o h_equil hφ = (o t1 * φ * s.amms.r0 t0 t1 ⋯ * s.amms.r1 t0 t1 ⋯).sqrt.sub ((o t0).sqrt * (s.amms.r0 t0 t1 ⋯ + φ * x₀)) ⋯ / ((o t0).sqrt * φ)

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

Equations

• SX.fee.constprod.x_max φ sw0 o h_equil hφ = x₀ + SX.fee.constprod.x_max' φ sw0 o h_equil hφ

theorem SX.fee.constprod.x_max'_eq_cond (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (o : O) (h_equil : sw_to_equil φ sw0 o) (hφ : φ < 1) : √↑(o t0) * (↑(s.amms.r0 t0 t1 ⋯) + ↑φ * ↑x₀ + ↑φ * ↑(x_max' φ sw0 o h_equil hφ)) = √(↑(o t1) * ↑φ * ↑(s.amms.r0 t0 t1 ⋯) * ↑(s.amms.r1 t0 t1 ⋯))

theorem SX.fee.constprod.x_max_lt_x₀_div_φ (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (o : O) (h_equil : sw_to_equil φ sw0 o) (hφ : φ < 1) : x_max φ sw0 o h_equil hφ < x₀ / φ

theorem SX.fee.constprod.gain_xmax_gt_x₀ (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (o : O) (h_equil : sw_to_equil φ sw0 o) (hφ : φ < 1) (sw_max : Swap (constprod φ) s a t0 t1 (x_max φ sw0 o h_equil hφ)) (h_supply : s.mints.supply t0 t1 > 0) (h_mints : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) : a.gain o s sw0.apply < a.gain o s sw_max.apply

theorem SX.fee.constprod.x_max_gain_gt_x_gt_equil (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ x : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (sw2 : Swap (constprod φ) s a t0 t1 x) (o : O) (h_equil : sw_to_equil φ sw0 o) (hφ : φ < 1) (sw_max : Swap (constprod φ) s a t0 t1 (x_max φ sw0 o h_equil hφ)) (x_gt_x₀ : x > x₀) (x_diff_x_max : x ≠ x_max φ sw0 o h_equil hφ) (h_supply : s.mints.supply t0 t1 > 0) (h_mints : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) : a.gain o s sw2.apply < a.gain o s sw_max.apply

theorem SX.fee.constprod.x_max_gain (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (o : O) (h_equil : sw_to_equil φ sw0 o) (hφ : φ < 1) (sw_max : Swap (constprod φ) s a t0 t1 (x_max φ sw0 o h_equil hφ)) (x : ℝ>0) (sw2 : Swap (constprod φ) s a t0 t1 x) : x ≠ x_max φ sw0 o h_equil hφ → s.mints.supply t0 t1 > 0 → (s.mints.get a).get t0 t1 < s.mints.supply t0 t1 → a.gain o s sw2.apply < a.gain o s sw_max.apply

theorem SX.fee.constprod.x_max_unique (φ : ℝ>0) {s : Γ} {a : A} {t0 t1 : T} {x₀ : ℝ>0} (sw0 : Swap (constprod φ) s a t0 t1 x₀) (o : O) (h_equil : sw_to_equil φ sw0 o) (h_supply : s.mints.supply t0 t1 > 0) (h_mints : (s.mints.get a).get t0 t1 < s.mints.supply t0 t1) (hφ : φ < 1) (sw_max : Swap (constprod φ) s a t0 t1 (x_max φ sw0 o h_equil hφ)) : ¬∃ (x₁ : ℝ>0) (h_enough : ↑x₁ ≤ (s.atoms.get a) t0), x₁ ≠ x_max φ sw0 o h_equil hφ ∧ ∀ (x : ℝ>0) (sw2 : Swap (constprod φ) s a t0 t1 x), x ≠ x₁ → s.mints.supply t0 t1 > 0 → (s.mints.get a).get t0 t1 < s.mints.supply t0 t1 → a.gain o s sw2.apply < a.gain o s ⋯.apply