def SX.additive (sx : SX) : Prop

Equations

• sx.additive = ∀ (x y r0 r1 : ℝ>0) (h : x * sx x r0 r1 < r1), sx (x + y) r0 r1 = (x * sx x r0 r1 + y * sx y (r0 + x) (r1.sub (x * sx x r0 r1) h)) / (x + y)

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

def Swap.additive {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (addi : sx.additive) : Swap sx s a t0 t1 (x₀ + x₁)

Equations

• ⋯ = ⋯

def Swap.bound_split1 {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw : Swap sx s a t0 t1 (x₀ + x₁)) (bound : sx.outputbound) : Swap sx s a t0 t1 x₀

Equations

• ⋯ = ⋯

def Swap.bound_split2 {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw : Swap sx s a t0 t1 (x₀ + x₁)) (bound : sx.outputbound) : Swap sx ⋯.apply a t0 t1 x₁

Equations

• ⋯ = ⋯

@[simp]

theorem Swap.additive_y {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (addi : sx.additive) : ⋯.y = sw0.y + sw1.y

@[simp]

theorem Swap.additive_y' {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (sw2 : Swap sx s a t0 t1 (x₀ + x₁)) (addi : sx.additive) : sw2.y = sw0.y + sw1.y

@[simp]

theorem Swap.join_additive_atoms {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (addi : sx.additive) : sw1.apply.atoms = ⋯.apply.atoms

@[simp]

theorem Swap.join_additive_amms {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (addi : sx.additive) : sw1.apply.amms = ⋯.apply.amms

@[simp]

theorem Swap.join_additive {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (addi : sx.additive) : sw1.apply = ⋯.apply

theorem Swap.additive_gain {sx : SX} {s : Γ} {a : A} {t0 t1 : T} {x₀ x₁ : ℝ>0} (sw0 : Swap sx s a t0 t1 x₀) (sw1 : Swap sx sw0.apply a t0 t1 x₁) (sw2 : Swap sx s a t0 t1 (x₀ + x₁)) (addi : sx.additive) (o : T → ℝ>0) : a.gain o s sw2.apply = a.gain o s sw0.apply + a.gain o sw0.apply sw1.apply

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