Determinant bound

Stream: maths

[Oliver Nash]

Here's a result I almost proved this afternoon because I thought it would give me a short cut to something I want. I subsequently decided it was not the shortcut I had hoped but it's elementary and useful so maybe if I dump it here, it will magically get formalised:

import linear_algebra.determinant
import analysis.normed_space.multilinear

variables (k : Type*) [normed_comm_ring k] [norm_one_class k]

open_locale nat big_operators

lemma norm_det_le {ι : Type*} [fintype ι] [decidable_eq ι] (A : matrix ι ι k) :
  ∥A.det∥ ≤ (fintype.card ι)! * ∏ i, ∥A i∥ :=
sorry -- induction + `matrix.det_succ_column_zero`

-- or even just
lemma norm_det_le' {n : ℕ} (A : matrix (fin n) (fin n) k) :
  ∥A.det∥ ≤ n! * ∏ i, ∥A i∥ :=
sorry

[Anne Baanen]

I proved something like that for the class number, let me see what it is called...

[Oliver Nash]

No way!

[Oliver Nash]

That would be awesome.

[Anne Baanen]

Check out docs#matrix.det_le

[Oliver Nash]

Hmm, I think that's just slightly weaker than I need.

[Anne Baanen]

Yeah, I only have an element-wise upper bound and you need it column-wise :(

[Oliver Nash]

The application would be to apply docs#multilinear_map.continuous_of_bound to docs#matrix.det_row_alternating

[Oliver Nash]

Maybe I could use multilinearity to rescale each column and deduce what I want from your result!

[Oliver Nash]

That should work actually!

[Oliver Nash]

I'm out of time for the day but for the record I think the rescaling approach will work nicely for matrices taking values in ℝ but seems to be awkward otherwise because we cannot scale an element by an absolute value or norm.