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

• enough : ↑v0 ≤ (s.atoms.get a) t0
• exi : s.amms.init t0 t1
• nodrain : v0 * sx v0 (s.amms.r0 t0 t1 ⋯) (s.amms.r1 t0 t1 ⋯) < s.amms.r1 t0 t1 ⋯

theorem Swap.singleton {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {x : ℝ>0} (sw0 sw1 : Swap sx s a t0 t1 x) : sw0 = sw1

def Swap.rate {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : ℝ>0

Equations

• sw.rate = sx v0 (s.amms.r0 t0 t1 ⋯) (s.amms.r1 t0 t1 ⋯)

def Swap.y {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : ℝ>0

Equations

• sw.y = v0 * sw.rate

theorem Swap.y_eq {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {x : ℝ>0} (s✝ : Swap sx s a t0 t1 x) : s✝.y = x * s✝.rate

theorem Swap.y_lt_r1 {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : sw.y < s.amms.r1 t0 t1 ⋯

theorem Swap.y_lt_r1₀ {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : ↑sw.y < s.amms.r1₀ t0 t1

noncomputable def Swap.apply {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : Γ

Equations

• sw.apply = { atoms := (s.atoms.sub a t0 ↑v0 ⋯).add a t1 ↑sw.y, mints := s.mints, amms := (s.amms.sub_r1 t0 t1 ⋯ sw.y ⋯).add_r0 t0 t1 ⋯ v0 }

def Swap.is_solution {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {x₀ : ℝ>0} (sw : Swap sx s a t0 t1 x₀) (o : O) : Prop

Equations

• sw.is_solution o = ∀ (x : ℝ>0) (sw2 : Swap sx s a t0 t1 x), x ≠ x₀ → (s.mints.get a).get t0 t1 = 0 → a.gain o s sw2.apply < a.gain o s sw.apply

@[simp]

theorem Swap.atoms {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : sw.apply.atoms = (s.atoms.sub a t0 ↑v0 ⋯).add a t1 ↑sw.y

@[simp]

theorem Swap.mints {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : sw.apply.mints = s.mints

@[simp]

theorem Swap.amms {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : sw.apply.amms = (s.amms.sub_r1 t0 t1 ⋯ sw.y ⋯).add_r0 t0 t1 ⋯ v0

@[simp]

theorem Swap.b0_self {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : (sw.apply.atoms.get a) t0 = (s.atoms.get a) t0 - ↑v0

@[simp]

theorem Swap.b1_self {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) : (sw.apply.atoms.get a) t1 = (s.atoms.get a) t1 + ↑sw.y

@[simp]

theorem Swap.drain_atoms {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) (a' : A) : ((sw.apply.atoms.get a').drain t0).drain t1 = ((s.atoms.get a').drain t0).drain t1

@[simp]

theorem Swap.mintsupply {sx : SX} {s : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (sw : Swap sx s a t0 t1 v0) (t0' t1' : T) : sw.apply.mintsupply t0' t1' = s.mintsupply t0' t1'