Hadamard's inequality for Gram determinants

Hadamard's inequality bounds the volume spanned by a finite family of vectors by the product of their lengths. This file proves it in two forms over an RCLike field 𝕜.

• In coordinates: for an orthonormal basis b of E indexed by a finite type ι and any family v : ι → E, ‖b.toBasis.det v‖ ≤ ∏ i, ‖v i‖. The Gram–Schmidt orthonormal basis e of v makes the coordinate matrix of v triangular, so e.toBasis.det v = ∏ i, ⟪e i, v i⟫, and b.toBasis.det e has norm one.
• For Gram matrices: for any finite family v in an inner product space, which need not be finite-dimensional, det (gram 𝕜 v) ≤ ∏ i, ‖v i‖ ^ 2 for the order of ComplexOrder. Since that order compares only elements with equal imaginary parts, the bound also says that the Gram determinant is real. Its nonnegativity is Mathlib's Matrix.PosSemidef.det_nonneg applied to Matrix.posSemidef_gram. A dependent family has Gram determinant zero, and an independent family is a basis of its span, where the Gram determinant is the squared norm of a coordinate determinant.

These bounds control the covolume of a lattice by the lengths of its generators, as in the Gram/covolume calculation of J.-M. Couveignes, Enumerating number fields, Ann. of Math. 192 (2020), §3.

Main results

• OrthonormalBasis.norm_det_le_prod_norm: Hadamard's inequality for the coordinate determinant in an orthonormal basis.
• OrthonormalBasis.det_gram_eq_norm_det_sq: the Gram determinant of a family is the squared norm of its coordinate determinant in an orthonormal basis.
• Matrix.ofReal_re_det_gram, Matrix.re_det_gram_nonneg: the Gram determinant is real, with nonnegative real part. These specialise Matrix.IsHermitian.ofReal_re_det and Matrix.PosSemidef.re_det_nonneg.
• Matrix.det_gram_le_prod_norm_sq, Matrix.re_det_gram_le_prod_norm_sq: Hadamard's inequality for Gram determinants, in ComplexOrder and for the real part.
• Matrix.re_det_gram_le_pow: the uniform form, re (det (gram 𝕜 v)) ≤ D ^ card ι when every ‖v i‖ ^ 2 ≤ D.

theorem OrthonormalBasis.norm_det_le_prod_norm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (v : ι → E) : ‖b.toBasis.det v‖ ≤ ∏ i : ι, ‖v i‖

Hadamard's inequality. The determinant of a family v in the coordinates of an orthonormal basis has norm at most the product of the norms of the vectors. The family may be linearly dependent.

theorem OrthonormalBasis.det_gram_eq_norm_det_sq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (v : ι → E) : (Matrix.gram 𝕜 v).det = ↑‖b.toBasis.det v‖ ^ 2

The Gram determinant of a family v is the squared norm of its determinant in the coordinates of an orthonormal basis.

@[simp]

theorem Matrix.ofReal_re_det_gram {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (v : ι → E) : ↑(RCLike.re (gram 𝕜 v).det) = (gram 𝕜 v).det

The Gram determinant of a finite family is real: it is the image of its real part. This is Matrix.IsHermitian.ofReal_re_det for Gram matrices, stated without hypotheses so that simp can use it.

theorem Matrix.re_det_gram_nonneg {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (v : ι → E) : 0 ≤ RCLike.re (gram 𝕜 v).det

The real part of the Gram determinant of a finite family is nonnegative. This is Matrix.PosSemidef.re_det_nonneg for Gram matrices.

theorem Matrix.det_gram_le_prod_norm_sq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (v : ι → E) : (gram 𝕜 v).det ≤ ∏ i : ι, ↑‖v i‖ ^ 2

Hadamard's inequality for Gram determinants. In any inner product space, the Gram determinant of a finite family is at most the product of the squared norms of its vectors. The order is that of ComplexOrder, so this also says that the Gram determinant is real; together with Matrix.PosSemidef.det_nonneg it lies between 0 and ∏ i, ‖v i‖ ^ 2.

theorem Matrix.re_det_gram_le_prod_norm_sq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (v : ι → E) : RCLike.re (gram 𝕜 v).det ≤ ∏ i : ι, ‖v i‖ ^ 2

Hadamard's inequality for Gram determinants, for the real part: the real part of the Gram determinant of a finite family is at most the product of the squared norms of its vectors.

theorem Matrix.re_det_gram_le_pow {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {v : ι → E} {D : ℝ} (hD : ∀ (i : ι), ‖v i‖ ^ 2 ≤ D) : RCLike.re (gram 𝕜 v).det ≤ D ^ Fintype.card ι

Hadamard's inequality, uniform form. If every vector of a finite family has squared norm at most D, the real part of its Gram determinant is at most D ^ card ι.