def SX.reversible (sx : SX) (bound : sx.outputbound) : Prop

Equations

• sx.reversible bound = ∀ (x r0 r1 : ℝ>0), sx (x * sx x r0 r1) (r1.sub (x * sx x r0 r1) ⋯) (x + r0) = 1 / sx x r0 r1

def Swap.inv {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {v0 : ℝ>0} {hbound : sx.outputbound} (sw : Swap sx s a t0 t1 v0) : sx.reversible hbound → Swap sx sw.apply a t1 t0 sw.y

Equations

• ⋯ = ⋯

theorem Swap.rate_of_inv_eq_inv_rate {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} {hbound : sx.outputbound} (sw : Swap sx s a t0 t1 x) (hrev : sx.reversible hbound) : ⋯.rate = sw.rate⁻¹

@[simp]

theorem Swap.inv_y_eq_x {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} {hbound : sx.outputbound} (sw : Swap sx s a t0 t1 x) (hrev : sx.reversible hbound) : ⋯.y = x

theorem Swap.inv_apply_eq_atoms {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} {hbound : sx.outputbound} (sw : Swap sx s a t0 t1 x) (hrev : sx.reversible hbound) : ⋯.apply.atoms = s.atoms

theorem Swap.inv_apply_eq_amms {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} {hbound : sx.outputbound} (sw : Swap sx s a t0 t1 x) (hrev : sx.reversible hbound) : ⋯.apply.amms = s.amms

@[simp]

theorem Swap.inv_apply {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} {hbound : sx.outputbound} (sw : Swap sx s a t0 t1 x) (hrev : sx.reversible hbound) : ⋯.apply = s

theorem Swap.rev_gain {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x : ℝ>0} {hbound : sx.outputbound} (sw : Swap sx s a t0 t1 x) (hrev : sx.reversible hbound) (o : T → ℝ>0) : -a.gain o sw.apply ⋯.apply = a.gain o s sw.apply