structure Deposit (s : Γ) (a : A) (t0 t1 : T) (v0 : ℝ>0) : Prop

• exi : s.amms.init t0 t1
• possupp : 0 < s.mints.supply t0 t1
• hen0 : ↑v0 ≤ (s.atoms.get a) t0
• hen1 : ↑v0 * ↑(s.amms.r0 t0 t1 ⋯) / s.mints.supply t0 t1 ≤ (s.atoms.get a) t1

noncomputable def Deposit.v1 {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (d : Deposit s a t0 t1 v0) : ℝ>0

Equations

• d.v1 = v0 * s.amms.r0 t0 t1 ⋯ / (s.mints.supply t0 t1).toPReal ⋯

noncomputable def Deposit.v {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (d : Deposit s a t0 t1 v0) : ℝ>0

Equations

• d.v = v0 * (s.mints.supply t0 t1).toPReal ⋯ / s.amms.r0 t0 t1 ⋯

noncomputable def Deposit.apply {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (d : Deposit s a t0 t1 v0) : Γ

Equations

• d.apply = { atoms := (s.atoms.sub a t0 ↑v0 ⋯).sub a t1 ↑d.v1 ⋯, mints := s.mints.add a t0 t1 ⋯ ↑d.v, amms := (s.amms.add_r0 t0 t1 ⋯ v0).add_r1 t0 t1 ⋯ d.v1 }

@[simp]

theorem Deposit.atoms {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (d : Deposit s a t0 t1 v0) : d.apply.atoms = (s.atoms.sub a t0 ↑v0 ⋯).sub a t1 ↑d.v1 ⋯

@[simp]

theorem Deposit.mints {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (d : Deposit s a t0 t1 v0) : d.apply.mints = s.mints.add a t0 t1 ⋯ ↑d.v

@[simp]

theorem Deposit.amms {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (d : Deposit s a t0 t1 v0) : d.apply.amms = (s.amms.add_r0 t0 t1 ⋯ v0).add_r1 t0 t1 ⋯ d.v1