noncomputable def Γ.mintedprice (s : Γ) (o : T → ℝ>0) (t0 t1 : T) : NNReal

Equations

• s.mintedprice o t0 t1 = if h : s.amms.init t0 t1 then (↑(s.amms.r0 t0 t1 h) * ↑(o t0) + ↑(s.amms.r1 t0 t1 h) * ↑(o t1)) / s.mints.supply t0 t1 else 0

theorem Γ.mintedprice_reorder (s : Γ) (o : T → ℝ>0) (t1 t0 : T) : s.mintedprice o t1 t0 = s.mintedprice o t0 t1

noncomputable def Γ.networth (s : Γ) (a : A) (o : T → ℝ>0) : NNReal

Equations

• s.networth a o = (s.atoms.get a).worth o + (s.mints.get a).worth (s.mintedprice o)

noncomputable def A.gain (a : A) (o : T → ℝ>0) (s s' : Γ) : ℝ

Equations

• a.gain o s s' = ↑(s'.networth a o) - ↑(s.networth a o)