structure S₀ : Type

• map : A →₀ W₀

def S₀.get (s : S₀) (a : A) : W₀

Equations

• s.get a = s.map a

theorem S₀.ext {s1 s2 : S₀} (h : ∀ (a : A), s1.get a = s2.get a) : s1 = s2

@[simp]

theorem S₀.map_eq_get (s : S₀) : ⇑s.map = s.get

noncomputable def S₀.add (s : S₀) (a : A) (t : T) (x : NNReal) : S₀

Equations

• s.add a t x = { map := s.map.update a ((s.map a).add t x) }

@[simp]

theorem S₀.get_add_self (s : S₀) (a : A) (t : T) (x : NNReal) : (s.add a t x).get a = (s.get a).add t x

@[simp]

theorem S₀.get_add_diffa (s : S₀) (a : A) (t : T) (x : NNReal) (a' : A) (hdif : a ≠ a') : (s.add a t x).get a' = s.get a'

noncomputable def S₀.sub (s : S₀) (a : A) (t : T) (x : NNReal) (h : x ≤ (s.get a) t) : S₀

Equations

• s.sub a t x h = { map := s.map.update a ((s.map a).sub t x h) }

@[simp]

theorem S₀.get_sub_self (s : S₀) (a : A) (t : T) (x : NNReal) (h : x ≤ (s.get a) t) : (s.sub a t x h).get a = (s.get a).sub t x h

@[simp]

theorem S₀.get_sub_diffa (s : S₀) (a : A) (t : T) (x : NNReal) (h : x ≤ (s.get a) t) (a' : A) (hdif : a ≠ a') : (s.sub a t x h).get a' = s.get a'

noncomputable def S₀.drainw (s : S₀) (a : A) : S₀

Equations

• s.drainw a = { map := Finsupp.erase a s.map }

def S₀.supply (s : S₀) (t : T) : NNReal

Equations

• s.supply t = s.map.sum fun (x : A) (w : W₀) => w t

@[simp]

theorem S₀.supply_of_add_self (s : S₀) (a : A) (t : T) (x : NNReal) : (s.add a t x).supply t = s.supply t + x

@[simp]

theorem S₀.supply_of_add_diff (s : S₀) (a : A) (t : T) (x : NNReal) (t' : T) (hdiff : t ≠ t') : (s.add a t x).supply t' = s.supply t'

@[simp]

theorem S₀.supply_of_sub_self (s : S₀) (a : A) (t : T) (x : NNReal) (h : x ≤ (s.get a) t) : (s.sub a t x h).supply t = s.supply t - x

@[simp]

theorem S₀.supply_of_sub_diff (s : S₀) (a : A) (t : T) (x : NNReal) (h : x ≤ (s.get a) t) (t' : T) (hdifp : t ≠ t') : (s.sub a t x h).supply t' = s.supply t'