@[reducible, inline]

abbrev W₀ : Type

Equations

• W₀ = (T →₀ NNReal)

noncomputable def W₀.add (w : W₀) (t : T) (x : NNReal) : W₀

Equations

• w.add t x = Finsupp.update w t (w t + x)

@[simp]

theorem W₀.get_add_self (w : W₀) (t : T) (x : NNReal) : (w.add t x) t = w t + x

@[simp]

theorem W₀.get_add_diff (w : W₀) (t : T) (x : NNReal) (t' : T) (hdif : t ≠ t') : (w.add t x) t' = w t'

noncomputable def W₀.sub (w : W₀) (t : T) (x : NNReal) : x ≤ w t → W₀

Equations

• w.sub t x x✝ = Finsupp.update w t (w t - x)

@[simp]

theorem W₀.get_sub_self (w : W₀) (t : T) (x : NNReal) (h : x ≤ w t) : (w.sub t x h) t = w t - x

@[simp]

theorem W₀.get_sub_diff (w : W₀) (t : T) (x : NNReal) (h : x ≤ w t) (t' : T) (diff : t ≠ t') : (w.sub t x h) t' = w t'

noncomputable def W₀.drain (w : W₀) (t : T) : W₀

Equations

• w.drain t = w.sub t (w t) ⋯

@[simp]

theorem W₀.get_drain_self (w : W₀) (t : T) : (w.drain t) t = 0

@[simp]

theorem W₀.get_drain_diff (w : W₀) (t t' : T) (diff : t ≠ t') : (w.drain t) t' = w t'

theorem W₀.drain_comm (w : W₀) (t0 t1 : T) : (w.drain t1).drain t0 = (w.drain t0).drain t1

@[simp]

theorem W₀.drain_add_self (w : W₀) (t : T) (x : NNReal) : (w.add t x).drain t = w.drain t

@[simp]

theorem W₀.drain_sub_self (w : W₀) (t : T) (x : NNReal) (h : x ≤ w t) : (w.sub t x h).drain t = w.drain t

@[simp]

theorem W₀.drain_add_diff (w : W₀) (t : T) (x : NNReal) (t' : T) (hdif : t ≠ t') : (w.add t x).drain t' = (w.drain t').add t x

@[simp]

theorem W₀.drain_sub_diff (w : W₀) (t : T) (x : NNReal) (h : x ≤ w t) (t' : T) (hdif : t ≠ t') : (w.sub t x h).drain t' = (w.drain t').sub t x ⋯

noncomputable def W₀.worth (w : W₀) (o : T → ℝ>0) : NNReal

Equations

• w.worth o = Finsupp.sum w fun (t : T) (x : NNReal) => x * ↑(o t)

theorem Finsupp.update_zero_eq_erase {α β : Type} [DecidableEq α] [Zero β] (f : α →₀ β) (a : α) : f.update a 0 = erase a f

theorem W₀.worth_destruct (w : W₀) (o : T → ℝ>0) (t : T) : w.worth o = (w.drain t).worth o + w t * ↑(o t)

@[simp]

theorem W₀.get_add_diff' (w : W₀) (t : T) (x : NNReal) (t' : T) (hdif : t' ≠ t) : (w.add t x) t' = w t'

@[simp]

theorem W₀.get_sub_diff' (w : W₀) (t : T) (x : NNReal) (h : x ≤ w t) (t' : T) (diff : t' ≠ t) : (w.sub t x h) t' = w t'

@[simp]

theorem W₀.get_drain_diff' (w : W₀) (t t' : T) (diff : t' ≠ t) : (w.drain t) t' = w t'

@[simp]

theorem W₀.drain_add_diff' (w : W₀) (t : T) (x : NNReal) (t' : T) (hdif : t' ≠ t) : (w.add t x).drain t' = (w.drain t').add t x

@[simp]

theorem W₀.drain_sub_diff' (w : W₀) (t : T) (x : NNReal) (h : x ≤ w t) (t' : T) (hdif : t' ≠ t) : (w.sub t x h).drain t' = (w.drain t').sub t x ⋯