## Stream: maths

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

#### 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 (?).

#### Kenny Lau (May 30 2020 at 20:53):

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

#### Kenny Lau (May 30 2020 at 20:54):

also you want parentheses around forall _, _

#### Kenny Lau (May 30 2020 at 20:54):

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

Alright

#### Reid Barton (May 30 2020 at 20:55):

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

oh right

#### Kenny Lau (May 30 2020 at 20:56):

also use \le instead of \subset

#### Ryan Lahfa (May 30 2020 at 20:56):

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

#### Kenny Lau (May 30 2020 at 20:56):

\bu

#### Kenny Lau (May 30 2020 at 20:56):

and drop the parentheses around t i

#### 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

Okay

#### Kenny Lau (May 30 2020 at 20:57):

you still need parentheses around \forall _, _

#### 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 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


is it good now?

#### Kenny Lau (May 30 2020 at 20:57):

parentheses around \forall _, _

#### Ryan Lahfa (May 30 2020 at 20:57):

is it correct to use fin n for matrix?

ah!

yes

#### 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 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


like this?

exactly

nice!

#### Ryan Lahfa (May 30 2020 at 20:58):

we have a bad ™ puzzle

#### Kenny Lau (May 30 2020 at 20:58):

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

#### Kenny Lau (May 30 2020 at 20:58):

and matrix.eval

#### Kenny Lau (May 30 2020 at 20:59):

and use more newlines

Okay

#### 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 ?

more newlines

#### Kenny Lau (May 30 2020 at 21:00):

yeah that looks brilliant

#### 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

#### Ryan Lahfa (May 30 2020 at 21:01):

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

#### 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

#### Sebastien Gouezel (May 31 2020 at 07:31):

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

#### 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