Summing over pairs

Stream: Is there code for X?

[Aleksandar Milchev]

Hey, I am trying to implement the max-flow min-cut theorem in my branch of mathlib: https://github.com/leanprover-community/mathlib/blob/max_flow_min_cut/src/combinatorics/quiver/max_flow_min_cut.lean.
However, I don't know how to sum over pairs and I need it on lines 391 and 393. Is there a direct code in the library or I need to do a clever transformation? The code, which is commented out (after the two sorry's) is my first try, but it doesn't work. Thank you!

[Eric Wieser]

What do you mean by "over pairs"?

[Eric Wieser]

It looks to me like you might want docs#finset.add_sum_erase

[Aleksandar Milchev]

Eric Wieser said:

It looks to me like you might want docs#finset.add_sum_erase

Thank you very mich! That was useful!

I am also searching for code proving that for all sets A and B:
∑ x in A, ∑ y in B, f x y = ∑ y in B, ∑ x in A, f x y, i.e. summing over pairs is commutative.
Thank you in advance!

[Kyle Miller]

docs#finset.sum_comm

[Aleksandar Milchev]

Once again, hopefully for the last time, while proving this theorem, I need to sum over pairs. I need to prove that
∑ (x : V) in S, ∑ (y : V) in V' \ S, afn.f x y ≤ ∑ (x : V) in S, ∑ (y : V) in V' \ S, afn.network.to_capacity.c x y, when knowing that
∀ (x y : V), (x ∈ V' \ S ∧ y ∈ S) → (afn.f x y ≤ afn.network.to_capacity.c x y), and similarly conclude that
0 ≤ ∑ (x : V) in V' \ S, ∑ (y : V) in S, afn.f x y from ∀ (u v : V), (u ∈ V' \ S ∧ v ∈ S) → afn.f u v ≥ 0, but both finset.sum_le_sum and finset.sum_nonneg don't work.

Is there code for that? Thank you in advance!

[Eric Wieser]

Can you write that in #backticks, or better yet as a #mwe?

[Floris van Doorn]

It looks like two applications of docs#finset.sum_le_sum and two applications of docs#finset.sum_nonneg should prove what you want. A #mwe would indeed be useful to see why that doesn't work in your case.

[Aleksandar Milchev]

Floris van Doorn said:

It looks like two applications of docs#finset.sum_le_sum and two applications of docs#finset.sum_nonneg should prove what you want. A #mwe would indeed be useful to see why that doesn't work in your case.

I was thinking of applying two commands, but the functions take two arguments and I am not sure how this will work.
Here is the mwe:

import data.finset.basic
import data.real.basic
import data.set.basic
import tactic

universe u

variable (V: Type u)

open finset

open_locale big_operators
open_locale classical

notation ` V' ` := univ

lemma leq {V : Type u} (S : finset V) [inst : fintype V] (f : V -> V -> ℝ) (g : V -> V -> ℝ) :
  ∑ (x : V) in S, ∑ (y : V) in V' \ S, f x y ≤ ∑ (x : V) in S, ∑ (y : V) in V' \ S, g x y :=
begin
   have help: ∀ (x y : V), (x ∈ V' \ S ∧ y ∈ S) → (f x y ≤ g x y) := by sorry,
   sorry,
end

lemma nonneg {V : Type u} (S : finset V) [inst : fintype V] (f : V -> V -> ℝ) :
0 ≤ ∑ (x : V) in V' \ S, ∑ (y : V) in S, f x y :=
begin
  have help: ∀ (u v : V), (u ∈ V' \ S ∧ v ∈ S) → f u v ≥ 0 := by sorry,
  sorry,
end

[Floris van Doorn]

I had to change the statement of the first help a little bit (and made some other stylistic modifications), but here you go:

import data.finset.basic
import data.real.basic
import algebra.big_operators.order

variables {V : Type*}

open finset

open_locale big_operators classical

notation ` V' ` := univ

lemma leq (S : finset V) [inst : fintype V] (f : V -> V -> ℝ) (g : V -> V -> ℝ) :
  ∑ (x : V) in S, ∑ (y : V) in V' \ S, f x y ≤ ∑ (x : V) in S, ∑ (y : V) in V' \ S, g x y :=
begin
   have help: ∀ (x y : V), (x ∈ S ∧ y ∈ V' \ S) → (f x y ≤ g x y) := by sorry,
   exact sum_le_sum (λ i hi, sum_le_sum $ λ j hj, help i j ⟨hi, hj⟩)
end

lemma nonneg (S : finset V) [inst : fintype V] (f : V -> V -> ℝ) :
0 ≤ ∑ (x : V) in V' \ S, ∑ (y : V) in S, f x y :=
begin
  have help: ∀ (u v : V), (u ∈ V' \ S ∧ v ∈ S) → f u v ≥ 0 := by sorry,
  exact sum_nonneg (λ i hi, sum_nonneg $ λ j hj, help i j ⟨hi, hj⟩),
end

[Floris van Doorn]

Here is the first proof step-by-step:

lemma leq (S : finset V) [inst : fintype V] (f : V -> V -> ℝ) (g : V -> V -> ℝ) :
  ∑ (x : V) in S, ∑ (y : V) in V' \ S, f x y ≤ ∑ (x : V) in S, ∑ (y : V) in V' \ S, g x y :=
begin
   have help: ∀ (x y : V), (x ∈ S ∧ y ∈ V' \ S) → (f x y ≤ g x y) := by sorry,
   apply sum_le_sum,
   intros i hi,
   apply sum_le_sum,
   intros j hj,
   apply help,
   split,
   { assumption },
   { assumption }
end

[Aleksandar Milchev]

Floris van Doorn said:

I had to change the statement of the first help a little bit (and made some other stylistic modifications), but here you go:

import data.finset.basic
import data.real.basic
import algebra.big_operators.order

variables {V : Type*}

open finset

open_locale big_operators classical

notation ` V' ` := univ

lemma leq (S : finset V) [inst : fintype V] (f : V -> V -> ℝ) (g : V -> V -> ℝ) :
  ∑ (x : V) in S, ∑ (y : V) in V' \ S, f x y ≤ ∑ (x : V) in S, ∑ (y : V) in V' \ S, g x y :=
begin
   have help: ∀ (x y : V), (x ∈ S ∧ y ∈ V' \ S) → (f x y ≤ g x y) := by sorry,
   exact sum_le_sum (λ i hi, sum_le_sum $ λ j hj, help i j ⟨hi, hj⟩)
end

lemma nonneg (S : finset V) [inst : fintype V] (f : V -> V -> ℝ) :
0 ≤ ∑ (x : V) in V' \ S, ∑ (y : V) in S, f x y :=
begin
  have help: ∀ (u v : V), (u ∈ V' \ S ∧ v ∈ S) → f u v ≥ 0 := by sorry,
  exact sum_nonneg (λ i hi, sum_nonneg $ λ j hj, help i j ⟨hi, hj⟩),
end

Thank you very much!

[Eric Wieser]

Note your V' \ S is better spelt Sᶜ