Finite families and map evaluation on linear m...

Stream: maths

[Ryan Lahfa]

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]

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

[Kenny Lau]

also you want parentheses around forall _, _

[Kenny Lau]

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

[Ryan Lahfa]

Alright

[Reid Barton]

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

[Kenny Lau]

oh right

[Kenny Lau]

also use \le instead of \subset

[Ryan Lahfa]

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

[Kenny Lau]

\bu

[Kenny Lau]

and drop the parentheses around t i

[Ryan Lahfa]

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

[Ryan Lahfa]

Okay

[Kenny Lau]

you still need parentheses around \forall _, _

[Ryan Lahfa]

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]

parentheses around \forall _, _

[Ryan Lahfa]

is it correct to use fin n for matrix?

[Ryan Lahfa]

ah!

[Kenny Lau]

yes

[Ryan Lahfa]

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?

[Kenny Lau]

exactly

[Ryan Lahfa]

nice!

[Ryan Lahfa]

we have a bad ™ puzzle

[Kenny Lau]

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

[Kenny Lau]

and matrix.eval

[Kenny Lau]

and use more newlines

[Ryan Lahfa]

Okay

[Ryan Lahfa]

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 ?

[Ryan Lahfa]

more newlines

[Kenny Lau]

yeah that looks brilliant

[Ryan Lahfa]

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]

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

[Kevin Buzzard]

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]

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

[Ryan Lahfa]

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