simplifying matrix math

Stream: new members

[David Chanin]

I'm trying to do a simple proof that says that there exists a number t such that [3,1,4], [2,-3,5], [5,9,t] is not linearly independent in R3. I'm framing the problem as below:

example : ∃ t a b c: ℝ, a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
begin
  use [14, -3, 22, 7],
  simp,
  linarith,
end

basically, I just want it to subsitute these numbers into t, a, b, c and show that the results are equal. simp sort of helps, it does the smul and addition, but doesn't resolve the proof and leaves stuff in this weird form:

![-(3 * 3) + 22 * 2, -3 + -(22 * 3), -(3 * 4) + 22 * 5] = ![7 * 5, 7 * 9, 7 * 14]

Then, linarith throws an error. How can I get this to properly simplify and close the goal? It's just basic algebra to show these are the same thing

[Eric Rodriguez]

does ext x help?

[Eric Rodriguez]

after the use, before the simp

[Eric Rodriguez]

and maybe norm_num is the right thing

[David Chanin]

aah norm_num did it! Thanks so much!

[Eric Wieser]

congr' 1, {sorry}, congr' 1, { sorry } I think would let you equate each component separately, in case that's helpful

[Eric Rodriguez]

shouldn't we prefer interval_cases x?

[David Chanin]

ah doing congr' 1 { ... }3 times also works! That's handy to know

[David Chanin]

how would interval_cases work here?

[David Chanin]

( I also realized I had a mistake in the previous post, the correct values are as follows):

example : ∃ t a b c: ℝ, a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
begin
  use [2, 3, -2 , 1],
  simp,
  norm_num,
end

[Eric Rodriguez]

sorry, I meant fin_cases!

[Eric Rodriguez]

example : ∃ t a b c: ℝ, a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
begin
  use [2, 3, -2 , 1],
  ext x,
  fin_cases x,
  /-
    3 goals
  ⊢ (3 • ![3, 1, 4] + (-2) • ![2, -3, 5]) 0 = (1 • ![5, 9, 2]) 0
  ⊢ (3 • ![3, 1, 4] + (-2) • ![2, -3, 5]) 1 = (1 • ![5, 9, 2]) 1
  ⊢ (3 • ![3, 1, 4] + (-2) • ![2, -3, 5]) 2 = (1 • ![5, 9, 2]) 2
  -/
end

[Patrick Johnson]

Why not use all zeros? Or maybe the question is about tactics, rather than proving this exact statement?

example : ∃ (t a b c : ℝ), a • ![3, 1, 4] + b • ![2, -3, 5] = c • ![5, 9, t] :=
⟨0, 0, 0, 0, by simp⟩

[David Chanin]

Ah that's a good point, I should add a constraint that a, b, and c can't be 0 too since that would also be a valid solution as I wrote it

[Patrick Johnson]

Alternatively, you could just drop c

example : ∃ (t a b : ℝ), a • ![3, 1, 4] + b • ![2, -3, 5] = ![5, 9, t] :=
⟨2, 3, -2, by norm_num⟩

[David Chanin]

Good call, that's even cleaner!

[Eric Wieser]

Are you aware of docs#linear_independent? Perhaps you already stated your problem that way and reduced it to the case above

[David Chanin]

That would probably be a smarter approach. I don't really understand how to use linear_independent though. How would I frame this problem in terms of using that term?

[Eric Wieser]

I think ∃ t : ℝ, ¬linear_independent ℝ ![![3, 1, 4], ![2, -3, 5], ![5, 9, t]] is the correct statement

[David Chanin]

ah ok, I'll see if I can figure out the proof that way, it does look a lot more legit

[Eric Wieser]

I imagine it will be more work to prove not less

[Adam Topaz]

If you simplify with docs#fin.sum_univ_succ that should reduce it easily to the previous proof

[Adam Topaz]

import data.real.basic
import linear_algebra.linear_independent

example : ∃ t : ℝ, ¬linear_independent ℝ ![![3, 1, 4], ![2, -3, 5], ![5, 9, t]] :=
begin
  use 2,
  rw [fintype.not_linear_independent_iff],
  use ![3,-2,-1],
  split,
  { simp only [fin.sum_univ_succ, matrix.cons_val_zero, matrix.smul_cons, algebra.id.smul_eq_mul,
      mul_one, matrix.cons_val_succ, neg_mul, mul_neg, neg_neg, fintype.univ_of_subsingleton,
      matrix.cons_val_fin_one, one_mul, finset.sum_const, finset.card_singleton, nsmul_eq_mul,
      nat.cast_one, matrix.cons_add_cons, matrix.cons_eq_zero_iff,
      eq_iff_true_of_subsingleton, and_true], -- found with `squeeze_simp [fin.sum_univ_succ]`
    norm_num },
  { use 0, norm_num }
end

[Eric Rodriguez]

Adam, if you add the import import algebra.big_operators.norm_num then norm_num does all of the first case :)