structure W₁ : Type

• bal : T →₀ W₀
• unord (t0 t1 : T) : (self.bal t0) t1 = (self.bal t1) t0
• distinct (t : T) : (self.bal t) t = 0

def W₁.empty : W₁

Equations

• W₁.empty = { bal := 0, unord := W₁.empty.proof_1, distinct := W₁.empty.proof_2 }

instance instZeroW₁ : Zero W₁

Equations

• instZeroW₁ = { zero := W₁.empty }

def W₁.get (w : W₁) (t0 t1 : T) : NNReal

Equations

• w.get t0 t1 = (w.bal t0) t1

@[simp]

theorem W₁.zero_get (t0 t1 : T) : get 0 t0 t1 = 0

theorem W₁.bal_eq_get (w : W₁) (t0 t1 : T) : (w.bal t0) t1 = w.get t0 t1

theorem W₁.get_reorder (w : W₁) (t1 t0 : T) : w.get t1 t0 = w.get t0 t1

theorem W₁.samepair_get (w : W₁) {t0 t1 t0' t1' : T} (h : samemint t0 t1 t0' t1') : w.get t0 t1 = w.get t0' t1'

noncomputable def W₁.add (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) : W₁

Equations

• w.add t0 t1 hdif x = { bal := (w.bal.update t0 ((w.bal t0).add t1 x)).update t1 ((w.bal t1).add t0 x), unord := ⋯, distinct := ⋯ }

theorem W₁.add_reorder (w : W₁) (t1 t0 : T) (hdif : t0 ≠ t1) (x : NNReal) : w.add t1 t0 ⋯ x = w.add t0 t1 hdif x

@[simp]

theorem W₁.get_add_self (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) : (w.add t0 t1 hdif x).get t0 t1 = w.get t0 t1 + x

@[simp]

theorem W₁.get_add_diff (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (t0' t1' : T) (diffp : diffmint t0 t1 t0' t1') : (w.add t0 t1 hdif x).get t0' t1' = w.get t0' t1'

noncomputable def W₁.sub (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ w.get t0 t1) : W₁

Equations

• w.sub t0 t1 hdif x h = { bal := (w.bal.update t0 ((w.bal t0).sub t1 x h)).update t1 ((w.bal t1).sub t0 x ⋯), unord := ⋯, distinct := ⋯ }

theorem W₁.sub_reorder (w : W₁) (t1 t0 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ w.get t0 t1) : w.sub t1 t0 ⋯ x ⋯ = w.sub t0 t1 hdif x h

@[simp]

theorem W₁.get_sub_self (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ w.get t0 t1) : (w.sub t0 t1 hdif x h).get t0 t1 = w.get t0 t1 - x

@[simp]

theorem W₁.get_sub_diff (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ w.get t0 t1) (t0' t1' : T) (diffp : diffmint t0 t1 t0' t1') : (w.sub t0 t1 hdif x h).get t0' t1' = w.get t0' t1'

noncomputable def W₁.drain (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) : W₁

Equations

• w.drain t0 t1 hdif = w.sub t0 t1 hdif (w.get t0 t1) ⋯

theorem W₁.drain_reorder (w : W₁) (t1 t0 : T) (hdif : t0 ≠ t1) : w.drain t1 t0 ⋯ = w.drain t0 t1 hdif

@[simp]

theorem W₁.get_drain_self (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) : (w.drain t0 t1 hdif).get t0 t1 = 0

@[simp]

theorem W₁.get_drain_diff (w : W₁) (t0 t1 : T) (hdif : t0 ≠ t1) (t0' t1' : T) (diffp : diffmint t0 t1 t0' t1') : (w.drain t0 t1 hdif).get t0' t1' = w.get t0' t1'

noncomputable def W₁.u (w : W₁) : T × T →₀ NNReal

Equations

• w.u = w.bal.uncurry

theorem W₁.u_def (w : W₁) (t0 t1 : T) : w.u (t0, t1) = w.get t0 t1

noncomputable def W₁.worth (w : W₁) (o : T → T → NNReal) : NNReal

Equations

• w.worth o = (w.u.sum fun (p : T × T) (x : NNReal) => x * o p.1 p.2) / 2

theorem W₁.worth_destruct (w : W₁) (o : T → T → NNReal) (t0 t1 : T) (hdif : t0 ≠ t1) (ho : o t1 t0 = o t0 t1) : w.worth o = (w.drain t0 t1 hdif).worth o + w.get t0 t1 * o t0 t1