Sum lemmas

Stream: new members

[Steven Herbert]

I am struggling with some ``simple'' lemmas concerning splitting up and combining sums by elements and subsets:

[Steven Herbert]

import Mathlib

structure Network (V : Type) [Fintype V] where
  cap             : V → V → ℝ
  cap_pos         : ∀ u : V, ∀ v : V, 0 ≤ cap u v
  flow            : V → V → ℝ
  flow_pos         : ∀ u : V, ∀ v : V, 0 ≤ flow u v
  integerflow     : V → V → ℕ
  s               : V
  s_no_in_flow    : ∀ v : V , cap v s  = 0
  s_pos_out_cap  : ∃ v : V, 0 < cap s v
  s_unique        : ∀ v : V, (∑ u : V, cap u v = 0) → v = s
  t               : V
  t_no_out_flow   : ∀ v : V , cap t v  = 0
  t_pos_in_cap   : ∃ v : V, 0 < cap v t
  t_unique        : ∀ v : V, (∑ u : V, cap v u = 0) → v = t
  no_self_flow    : ∀ v : V, cap v v = 0
  flow_leq_cap    : ∀ u v : V, ↑(flow u v) ≤ cap u v
  Kirchoff        : ∀ u : V, (u = s) ∨ (u = t)
                      ∨ ((∑ w : V, flow w u) = (∑ v : V, flow u v))

open Network Classical Set NNReal Finset

@[ext]
structure Cutc {V : Type} [Fintype V] (N: Network V) where
  cutc             : Finset V
  t_in_cutc        : N.t ∈ cutc
  s_notin_cutc    : N.s ∉ cutc

lemma sum_lem_1 {V : Type} [Fintype V] {N : Network V} :
    ∑ x : V, N.flow x N.t - ∑ x : V, N.flow N.t x =
    (∑ x ∈ {N.t}ᶜ, N.flow x N.t - ∑ x ∈ {N.t}ᶜ, N.flow N.t x) +
    (∑ x ∈ {N.t}, N.flow x N.t - ∑ x ∈ {N.t}, N.flow N.t x) := by sorry

lemma sum_lem_2 {V : Type} [Fintype V] {N : Network V} {P : Cutc N} (w : V) (h₁ : w ∉ P.cutc) :
    (∑ u : V, (N.flow w u -  N.flow u w)) = (∑ u ∈ P.cutcᶜ, (N.flow w u -  N.flow u w)) +
    (∑ u ∈  P.cutc, (N.flow w u -  N.flow u w))  := by sorry

lemma sum_lem_3 {V : Type} [Fintype V] {N : Network V} {P : Cutc N} (w : V) (h₁ : w ∉ P.cutc) :
    ∑ v ∈ P.cutcᶜ, (N.flow v w -  N.flow w v) =
    (∑ v ∈ P.cutcᶜ \ {w}, (N.flow  v w -  N.flow w v)) +(N.flow w w - N.flow w w) := by sorry

lemma sum_lem_4 {V : Type} [Fintype V] {N : Network V} {P : Cutc N} (w : V) :
    ∑ u ∈ P.cutcᶜ, ∑ v ∈ P.cutc, ((N.flow u v) - (N.flow v u)) =
    ∑ u ∈ P.cutcᶜ \ {w}, ∑ v ∈ P.cutc, ((N.flow u v) - (N.flow v u))
    + ∑ v ∈ P.cutc, (N.flow w v - N.flow v w ) := by sorry

lemma sum_lem_5 {V : Type} [Fintype V] {N : Network V} {P : Cutc N} (w : V) :
    ∑ u ∈ P.cutcᶜ \ {w}, ∑ v ∈ P.cutc, ((N.flow u v) - (N.flow v u)) +
    ∑ u ∈ P.cutcᶜ \ {w}, (N.flow u w -  N.flow w u)
    = ∑ u ∈ P.cutcᶜ \ {w}, ∑ v ∈ P.cutc ∪ {w}, ((N.flow u v) - (N.flow v u)) := by sorry

[Steven Herbert]

Any help for the five 'sorrys' much appreciated!

[Vasilii Nesterov]

I suggest using loogle to search for the lemmas. For example, for the first one you can do

[Vasilii Nesterov]

@loogle Finset.sum, _ᶜ

[Vasilii Nesterov]

@loogle Finset.sum, _ᶜ

[loogle]

:search: Fintype.sum_eq_add_sum_compl, Fintype.sum_eq_sum_compl_add, and 10 more

[Steven Herbert]

Thanks! I've untangled all of these now