Type definition doesn't auto unfold

Stream: general

[Shi Zhengyu]

Hi all,

I defined mat n as a shorthand for square real matrix with size n.

variable n: ℕ
def mat := matrix (fin n) (fin n)  ℝ

But it doesn't seems to be unfolded by type elaborator?

invalid type ascription, term has type
  mat n →L[ℝ] ℝ
but is expected to have type
  matrix (fin n) (fin n) ℝ →L[ℝ] ℝ

I tried add @[reducible] to definition of mat, but that makes everything unfold themselves and create more errors as well ...

[Shi Zhengyu]

Or is there better way to create type aliases?

[Kyle Miller]

It'd help to have a #mwe of what's causing that error, but it looks like ℝ isn't being included in the mat expression. (I'd expect to see mat n ℝ →L[ℝ] ℝ).

[Shi Zhengyu]

Oh sorry that was a typo, fixed

[Shi Zhengyu]

import data.fintype.basic
import data.real.basic
import data.matrix.basic
import linear_algebra.matrix
import analysis.calculus.fderiv
import analysis.calculus.deriv
import linear_algebra.matrix.adjugate

open_locale matrix
open fintype finset matrix complex
local attribute [instance] real.nondiscrete_normed_field matrix.normed_group matrix.normed_space -- introduce an arbitrary canonical instance of normed_group and normed_space.

variable n: ℕ
def mat := matrix (fin n) (fin n) ℝ
variable A : ℝ -> (mat n)

theorem jacobi [normed_group (mat n)] [normed_space ℝ (mat n)]:
  ∀(x: ℝ) , differentiable_at ℝ A x -> deriv (det ∘ A) x = matrix.trace (fin n) ℝ ℝ (adjugate(A x) ⬝ (deriv A x)) :=
begin
  intro x,
  set f'comp := deriv (det ∘ A) with hmh,
  set f'det: mat n →L[ℝ] ℝ := fderiv ℝ det (A x) with f1h,
  set f'A:  ℝ →L[ℝ] (mat n) := fderiv ℝ A x with f2h,
 have hg : has_fderiv_at det (f'det: (matrix (fin n) (fin n) ℝ) →L[ℝ] ℝ) (A x),
 sorry

end

[Heather Macbeth]

@Shi Zhengyu Practice making a truly minimal working example (see the instructions at #mwe). Here it would be something like this:

import linear_algebra.matrix
import analysis.calculus.fderiv

open matrix
local attribute [instance] real.nondiscrete_normed_field matrix.normed_group matrix.normed_space -- introduce an arbitrary canonical instance of normed_group and normed_space.

variable n: ℕ
def mat := matrix (fin n) (fin n) ℝ

example [normed_group (mat n)] [normed_space ℝ (mat n)] (A : ℝ -> (mat n)) (x : ℝ) :
  (matrix (fin n) (fin n) ℝ) →L[ℝ] ℝ :=
begin
  set f'det: mat n →L[ℝ] ℝ := fderiv ℝ det (A x) with f1h,
  exact f'det,
end

[Heather Macbeth]

And in answer to your questions:

• You don't want a type synonym here; it just causes headaches when Lean can't find the information it needs through the wall of a new variable definition. If you hate writing out matrix (fin n) (fin n) ℝ over and over, you can use notation.
• I think you need some parentheses.

import linear_algebra.matrix
import analysis.calculus.fderiv

open matrix
local attribute [instance] real.nondiscrete_normed_field matrix.normed_group matrix.normed_space -- introduce an arbitrary canonical instance of normed_group and normed_space.

local notation `mat`:1000 n := matrix (fin n) (fin n) ℝ

variable n: ℕ

example (A : ℝ -> (mat n)) (x : ℝ) : (matrix (fin n) (fin n) ℝ) →L[ℝ] ℝ :=
begin
  set f'det: (mat n) →L[ℝ] ℝ := fderiv ℝ det (A x) with f1h,
  exact f'det,
end

[Heather Macbeth]

Also a bit of advice about your original problem, see below for a modified version:

• no need to restrict to the reals
• has_deriv_at is typically more user-friendly than deriv+differentiable

import analysis.calculus.deriv
import linear_algebra.matrix.adjugate

open_locale matrix
open matrix
local attribute [instance]  matrix.normed_group matrix.normed_space -- introduce an arbitrary canonical instance of normed_group and normed_space.

variables {𝕜: Type*} [nondiscrete_normed_field 𝕜]
local notation `mat` n := matrix (fin n) (fin n) 𝕜
variable n: ℕ
variable A : 𝕜 → (mat n)

theorem jacobi (A₀ : mat n) (x : 𝕜) (h : has_deriv_at A A₀ x) :
  has_deriv_at (det ∘ A) (trace (fin n) 𝕜 𝕜 (adjugate (A x) ⬝ A₀)) x :=
begin
  sorry
end

[Heather Macbeth]

Finally, I think it would be better not to phrase it in terms of "if A has this derivative then det ∘ A has that derivative", but as a multivariable statement about the derivative of the determinant function.

[Heather Macbeth]

Like this maybe:

import analysis.calculus.fderiv
import linear_algebra.matrix.adjugate
import analysis.normed_space.finite_dimension

open matrix
local attribute [instance]  matrix.normed_group matrix.normed_space

noncomputable theory

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [complete_space 𝕜]
local notation `mat` n := matrix (fin n) (fin n) 𝕜
variable (n : ℕ)

theorem jacobi' (A : mat n) :
  has_fderiv_at
    (det : (mat n) → 𝕜)
    (linear_map.to_continuous_linear_map ((matrix.trace (fin n) 𝕜 𝕜) ∘ₗ (algebra.lmul_left 𝕜 (adjugate A))))
    A :=
begin
  sorry
end

(I think @Oliver Nash has worked on related things.)

[Eric Wieser]

@Shi Zhengyu, is it a coincidence that you're working on this after I mentioned it in a thread last night?

[Heather Macbeth]

(I assumed you were working together!)

[Eric Wieser]

Don't let that dissuade you from working on it!

[Eric Wieser]

Heather, how were you able to avoid a proof obligation in docs#linear_map.to_continuous_linear_map above? (Edit: ah, I confused it with docs#linear_map.mk_continuous)

[Eric Wieser]

#13009 was motivated by the assumption I was going to have to provide one

[Heather Macbeth]

I assumed [complete_space 𝕜]

[Heather Macbeth]

But indeed, the trace should be a bounded linear map without that assumption.

[Heather Macbeth]

And so should left-multiplication in a normed algebra.

[Eric Wieser]

What's your opinion on the right way to state this; by creating matrix.trace_clm, mstrix.adjugate_clm, or by promoting the linear map to a continuous one at the last moment?

[Heather Macbeth]

I think matrix.trace_clm and matrix.adjugate_clm would be good to have. (Over topological or uniform rings, whatever works, rather than normed rings.)

[Heather Macbeth]

Er, wait -- the adjugate's not linear.

[Heather Macbeth]

So just the trace one :)

[Eric Wieser]

Right, I already have a proof trace is continuous

[Heather Macbeth]

Then you should be good to go with making

(matrix.trace (fin n) 𝕜 𝕜) ∘ₗ (algebra.lmul_left 𝕜 (adjugate A))

a "native" continuous linear map.

[Eric Wieser]

I think I'll let @Shi Zhengyu have a go at that once #13009 is merged, rather than treading on their toes

[Shi Zhengyu]

Eric Wieser said:

Shi Zhengyu, is it a coincidence that you're working on this after I mentioned it in a thread last night?

Oh what a coincidence! we've been trying to formalize Cauchy's Interlace Theorem, but then we met difficulty and decided to turn to Jacobi's formula instead ... Can you point me to the thread you mentioned? Thanks!

[Shi Zhengyu]

Also I don't think we are writing code with high enough quality suitable for anything serious now, so it's more of a project for learning to read mathlib etc. :D

[Eric Wieser]

docs#continuous.matrix_trace now exists, along with all the other new matrix lemmas in the same file