Zulip Chat Archive

Stream: maths

Topic: Finite families and map evaluation on linear m...


view this post on Zulip Ryan Lahfa (May 30 2020 at 20:52):

I'm trying to write some oral exams from ENS Ulm in Lean, for Kata & annoyingly hard puzzles, take this one:

import linear_algebra.matrix
import linear_algebra.determinant
import linear_algebra.dimension
import data.real.basic
import data.finset

lemma ulm2019_2 (n: ) (A B: matrix (fin n) (fin n) ) (t: (finset.range n)  ) (Ht: function.injective t):
   i  n, matrix.det (A + (t i)*B) = 0
      (V W: subspace  (fin n  )), (V.map (matrix.eval A))  W  V.map (matrix.eval B)  W  vector_space.dim  W < vector_space.dim  V := sorry

I don't know how can I have a (t_i)_i a finite family, @Kenny Lau suggested me to use this + injective, but maybe I got wrong his hint.

Also, I have this issue that modules seems to not have subsets (?).

view this post on Zulip Kenny Lau (May 30 2020 at 20:53):

ah sorry maybe use fin (n+1) -> \R instead

view this post on Zulip Kenny Lau (May 30 2020 at 20:54):

also you want parentheses around forall _, _

view this post on Zulip Kenny Lau (May 30 2020 at 20:54):

and then instead of t i you would write t \<i, _\>

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:55):

Alright

view this post on Zulip Reid Barton (May 30 2020 at 20:55):

Alternatively, just delete ≤ n from i ≤ n, right?

view this post on Zulip Kenny Lau (May 30 2020 at 20:55):

oh right

view this post on Zulip Kenny Lau (May 30 2020 at 20:56):

also use \le instead of \subset

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:56):

Hmm, but * is not working for scalar/matrix products, right?

view this post on Zulip Kenny Lau (May 30 2020 at 20:56):

\bu

view this post on Zulip Kenny Lau (May 30 2020 at 20:56):

and drop the parentheses around t i

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:56):

import linear_algebra.matrix
import linear_algebra.determinant
import linear_algebra.dimension
import data.real.basic
import data.finset

lemma ulm2019_2 (n: ) (A B: matrix (fin n) (fin n) ) (t: fin (n + 1)  ) (Ht: function.injective t):
   i, matrix.det (A + (t i)B) = 0
      (V W: subspace  (fin n  )), (V.map (matrix.eval A))  W  V.map (matrix.eval B)  W  vector_space.dim  W < vector_space.dim  V := sorry

And here we go

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:56):

Okay

view this post on Zulip Kenny Lau (May 30 2020 at 20:57):

you still need parentheses around \forall _, _

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:57):

lemma ulm2019_2 (n: ) (A B: matrix (fin n) (fin n) ) (t: fin (n + 1)  ) (Ht: function.injective t):
   i, (matrix.det (A + t iB) = 0)
      (V W: subspace  (fin n  )), (V.map (matrix.eval A))  W  V.map (matrix.eval B)  W  vector_space.dim  W < vector_space.dim  V := sorry

is it good now?

view this post on Zulip Kenny Lau (May 30 2020 at 20:57):

parentheses around \forall _, _

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:57):

is it correct to use fin n for matrix?

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:57):

ah!

view this post on Zulip Kenny Lau (May 30 2020 at 20:57):

yes

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:58):

lemma ulm2019_2 (n: ) (A B: matrix (fin n) (fin n) ) (t: fin (n + 1)  ) (Ht: function.injective t):
  ( i, matrix.det (A + t iB) = 0)
      (V W: subspace  (fin n  )), (V.map (matrix.eval A))  W  V.map (matrix.eval B)  W  vector_space.dim  W < vector_space.dim  V := sorry

like this?

view this post on Zulip Kenny Lau (May 30 2020 at 20:58):

exactly

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:58):

nice!

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:58):

we have a bad ™ puzzle

view this post on Zulip Kenny Lau (May 30 2020 at 20:58):

now put space around \bu and use projection notation for matrix.det

view this post on Zulip Kenny Lau (May 30 2020 at 20:58):

and matrix.eval

view this post on Zulip Kenny Lau (May 30 2020 at 20:59):

and use more newlines

view this post on Zulip Ryan Lahfa (May 30 2020 at 20:59):

Okay

view this post on Zulip Ryan Lahfa (May 30 2020 at 21:00):

import linear_algebra.matrix
import linear_algebra.determinant
import linear_algebra.dimension
import data.real.basic
import data.finset

lemma ulm2019_2 (n: ) (A B: matrix (fin n) (fin n) ) (t: fin (n + 1)  ) (Ht: function.injective t):
  ( i, (A + t i  B).det = 0)
      (V W: subspace  (fin n  )),
      V.map A.eval  W
       V.map B.eval  W
       vector_space.dim  W < vector_space.dim  V := sorry

is it nice, @Kenny Lau ?

view this post on Zulip Ryan Lahfa (May 30 2020 at 21:00):

more newlines

view this post on Zulip Kenny Lau (May 30 2020 at 21:00):

yeah that looks brilliant

view this post on Zulip Ryan Lahfa (May 30 2020 at 21:01):

import linear_algebra.matrix
import linear_algebra.determinant
import linear_algebra.dimension
import data.real.basic
import data.finset

lemma ulm2019_2 (n: ) (A B: matrix (fin n) (fin n) )
  (t: fin (n + 1)  ) (Ht: function.injective t):
  ( i, (A + t i  B).det = 0)
      (V W: subspace  (fin n  )),
      V.map A.eval  W
       V.map B.eval  W
       vector_space.dim  W < vector_space.dim  V := sorry

seems like perfect now

view this post on Zulip Ryan Lahfa (May 30 2020 at 21:01):

now, i have to do some undergraduate list stuff, then my first Kata

view this post on Zulip Kevin Buzzard (May 30 2020 at 21:31):

If you want to solve it then Kenny or I can post it. I don't want to get sidetracked on this right now though

view this post on Zulip Sebastien Gouezel (May 31 2020 at 07:31):

Who's the examiner now at ENS, by the way?

view this post on Zulip Ryan Lahfa (May 31 2020 at 15:04):

Sebastien Gouezel said:

Who's the examiner now at ENS, by the way?

It depends on the years, but for 2019, their names is written here: https://www.ens.psl.eu/sites/default/files/19_mp_rap_omath_u.pdf


Last updated: May 09 2021 at 10:11 UTC