noncomputable def AMMs.supply (amms : AMMs) (t : T) : NNReal

Equations

• amms.supply t = Finsupp.sum (amms.res t) fun (x : T) (x : NNReal) => x

noncomputable def Γ.atomsupply (s : Γ) (t : T) : NNReal

Equations

• s.atomsupply t = s.atoms.supply t + s.amms.supply t

noncomputable def Γ.mintsupply (s : Γ) (t0 t1 : T) : NNReal

Equations

• s.mintsupply t0 t1 = s.mints.supply t0 t1