-- Mathlib/Data/Matrix/DoublyStochastic.lean
/--
A matrix is `s` times a doubly stochastic matrix iff all entries are nonnegative, and all row and
column sums are equal to `s`.

This lemma is useful for the proof of Birkhoff's theorem - in particular because it allows scaling
by nonnegative factors rather than positive ones only.
-/
lemma exists_mem_doublyStochastic_eq_smul_iff {M : Matrix n n R} {s : R} (hs : 0 ≤ s) :
    (∃ M' ∈ doublyStochastic R n, M = s • M') ↔
      (∀ i j, 0 ≤ M i j) ∧ (∀ i, ∑ j, M i j = s) ∧ (∀ j, ∑ i, M i j = s)

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

Tactic:
rintro ⟨M', hM', rfl⟩

Result:
case intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : M' ∈ doublyStochastic R n
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j : n, (s • M') i j = s) ∧ ∀ (j : n), ∑ i : n, (s • M') i j = s

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), ∑ j : n, M i j = 0
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
⊢ (∃ x, x ∈ doublyStochastic R n) ∧ M = 0

Tactic:
refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), ∑ j : n, M i j = 0
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
⊢ M = 0

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
h₂ : ∑ j : n, M i j = 0
⊢ ∀ i_1 ∈ univ, 0 ≤ M i i_1

Tactic:
simp [h₁ i]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j : n, M i j = s
hM₃ : ∀ (j : n), ∑ i : n, M i j = s
⊢ s⁻¹ • M ∈ doublyStochastic R n ∧ M = s • s⁻¹ • M

Tactic:
simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', inv_mul_cancel₀, *]

Result:
no goals

Proof state:
case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

case mpr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Tactic:
case mp =>
  rintro ⟨M', hM', rfl⟩
  rw [mem_doublyStochastic_iff_sum] at hM'
  simp only [smul_apply, smul_eq_mul, ← mul_sum]
  exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩

Result:
case mpr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
⊢ (∀ (i j : n), 0 ≤ M i j) →
    (∀ (i : n), ∑ j : n, M i j = 0) → (∀ (j : n), ∑ i : n, M i j = 0) → (∃ x, x ∈ doublyStochastic R n) ∧ M = 0

Tactic:
intro h₁ h₂ _

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), ∑ j : n, M i j = 0
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
⊢ (∃ x, x ∈ doublyStochastic R n) ∧ M = 0

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

Tactic:
constructor

Result:
case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

case mpr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : (∀ (i j : n), 0 ≤ M' i j) ∧ (∀ (i : n), ∑ j : n, M' i j = 1) ∧ ∀ (j : n), ∑ i : n, M' i j = 1
⊢ (∀ (i : n), s * ∑ i_1 : n, M' i i_1 = s) ∧ ∀ (j : n), s * ∑ i : n, M' i j = s

Tactic:
simp [hM']

Result:
no goals

Proof state:
case a
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
h₂ : ∀ i_1 ∈ univ, M i i_1 = 0
⊢ M i j = 0 i j

Tactic:
exact h₂ _ (by simp)

Result:
no goals

Proof state:
case a
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), ∑ j : n, M i j = 0
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
⊢ M i j = 0 i j

Tactic:
specialize h₂ i

Result:
case a
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
h₂ : ∑ j : n, M i j = 0
⊢ M i j = 0 i j

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
h₂ : ∀ i_1 ∈ univ, M i i_1 = 0
⊢ j ∈ univ

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

Tactic:
classical
constructor
case mp =>
  rintro ⟨M', hM', rfl⟩
  rw [mem_doublyStochastic_iff_sum] at hM'
  simp only [smul_apply, smul_eq_mul, ← mul_sum]
  exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
rcases eq_or_lt_of_le hs with rfl | hs
case inl =>
  simp only [zero_smul, exists_and_right, and_imp]
  intro h₁ h₂ _
  refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
  ext i j
  specialize h₂ i
  rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
  exact h₂ _ (by simp)
rintro ⟨hM₁, hM₂, hM₃⟩
exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', inv_mul_cancel₀, *]⟩

Result:
no goals