The condensed form of a bilinear form

For a bilinear form B and a vector v, the corresponding condensed form is

S(x, y) = B(v, v) · B(x, y) - B(x, v) · B(v, y).

It is symmetric when B is, and it vanishes when either argument is v, so it does not change when multiples of v are added to its arguments. If B is positive definite, S is positive on the nonzero vectors of the kernel of any linear functional that does not vanish at v; this is the strict Cauchy–Schwarz inequality. If v is the first vector of a basis c, the Gram matrix of S on the other basis vectors is the condensation of the Gram matrix of B in c, so Chiò's identity (Matrix.mul_det_condensation_eq_pow_mul_det) computes its determinant. That is the inductive step of Hermite's inequality for the minimum of a positive definite quadratic form over ℤ.

Main results

• LinearMap.BilinForm.IsSymm.exists_isSymm_forall_apply_eq: the condensed form of a symmetric form, read on any module through a linear map, is a symmetric form.
• LinearMap.BilinForm.mul_apply_add_smul_add_smul: completing the square along v, B(v, v) B(x + s v, y + t v) = B(x + s v, v) B(v, y + t v) + S(x, y).
• LinearMap.BilinForm.apply_mul_apply_lt_of_mem_ker: for B positive definite, the condensed form is positive on the nonzero vectors of the kernel of a functional not vanishing at v.
• LinearMap.BilinForm.mul_det_toMatrix_eq_pow_mul_det_toMatrix: Chiò's identity for Gram matrices, B(v, v) · det S = B(v, v)ⁿ · det B.

theorem LinearMap.BilinForm.IsSymm.exists_isSymm_forall_apply_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) (v : M) (φ : N →ₗ[R] M) : ∃ (S : LinearMap.BilinForm R N), S.IsSymm ∧ ∀ (y z : N), (S y) z = (B v) v * (B (φ y)) (φ z) - (B (φ y)) v * (B v) (φ z)

The condensed form along v. For a symmetric form B, a vector v and a linear map φ : N →ₗ[R] M, the condensed form along v, read on N through φ, is a symmetric form: some symmetric S on N has S(y, z) = B(v, v) B(φ y, φ z) - B(φ y, v) B(v, φ z).

theorem LinearMap.BilinForm.mul_apply_add_smul_add_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (v x y : M) (s t : R) : (B v) v * (B (x + s • v)) (y + t • v) = (B (x + s • v)) v * (B v) (y + t • v) + ((B v) v * (B x) y - (B x) v * (B v) y)

Completing the square along v. Adding multiples of v to the arguments of B does not change the condensed form S(x, y) = B(v, v) B(x, y) - B(x, v) B(v, y): B(v, v) B(x + s v, y + t v) = B(x + s v, v) B(v, y + t v) + S(x, y).

theorem LinearMap.BilinForm.apply_mul_apply_lt_of_mem_ker {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [LinearOrder R] [IsStrictOrderedRing R] [Module.IsTorsionFree R M] {B : LinearMap.BilinForm R M} (hpos : ∀ (x : M), x ≠ 0 → 0 < (B x) x) {f : M →ₗ[R] R} {v x : M} (hv : f v ≠ 0) (hx : x ∈ f.ker) (hx0 : x ≠ 0) : (B x) v * (B v) x < (B v) v * (B x) x

The condensed form of a positive definite form is positive on a complement of v. Let B be positive definite on a torsion-free module over an ordered ring. If a linear functional f does not vanish at v, then every nonzero x in its kernel satisfies B(x, v) B(v, x) < B(v, v) B(x, x). This is the strict Cauchy–Schwarz inequality, since v and x are linearly independent.

theorem LinearMap.BilinForm.mul_det_toMatrix_eq_pow_mul_det_toMatrix {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {n : ℕ} (B : LinearMap.BilinForm R M) (c : Module.Basis (Fin (n + 1)) R M) {S : LinearMap.BilinForm R N} (b : Module.Basis (Fin n) R N) (hS : ∀ (i j : Fin n), (S (b i)) (b j) = (B (c 0)) (c 0) * (B (c i.succ)) (c j.succ) - (B (c i.succ)) (c 0) * (B (c 0)) (c j.succ)) : (B (c 0)) (c 0) * ((toMatrix b) S).det = (B (c 0)) (c 0) ^ n * ((toMatrix c) B).det

Chiò's condensation for Gram matrices. Let c be a basis of M indexed by Fin (n + 1) and S a bilinear form on N whose values on a basis b are those of the condensed form along c 0 on c 1, …, c n, that is, whose Gram matrix in b is the condensation of the Gram matrix of B in c. Then B(c 0, c 0) · det S = B(c 0, c 0)ⁿ · det B, the determinants being taken in b and c.