Gram determinants of pairs

The Gram determinant of two vectors, with inner products valued in a commutative ring, is <u, u> * <v, v> - <u, v> * <v, u>. Over the reals this is <u, u> * <v, v> - <u, v> ^ 2, the squared area of the parallelogram spanned by the pair and the denominator in the definition of sectional curvature.

The results here specialize Mathlib's general Gram-matrix API to a pair, exposing the explicit formula without introducing a second notion of Gram determinant. The real Gram determinant ‖u‖² ‖v‖² - ⟪u, v⟫² of a pair is also differentiated as a function of the pair (TauCeti.hasStrictFDerivAt_sq_sub_inner_sq); in mechanics it is the squared angular momentum ℓ² = ‖q‖² ‖p‖² - ⟪q, p⟫² of a phase-space point (q, p). Replacing the pair by (a q + b p, c q + d p) multiplies it by (a d - b c)² (TauCeti.sq_sub_inner_sq_smul_add_smul), so changes with a d - b c = ±1 preserve it.

theorem Matrix.det_gram_fin_two {𝕜 : Type u_1} {E : Type u_2} [CommRing 𝕜] [Inner 𝕜 E] (u v : E) : (gram 𝕜 ![u, v]).det = inner 𝕜 u u * inner 𝕜 v v - inner 𝕜 u v * inner 𝕜 v u

The Gram determinant of a pair, for inner products valued in a commutative ring.

theorem Matrix.real_det_gram_fin_two {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u v : E) : (gram ℝ ![u, v]).det = inner ℝ u u * inner ℝ v v - inner ℝ u v ^ 2

The Gram determinant of a pair in a real inner-product space is its squared parallelogram area.

theorem TauCeti.hasStrictFDerivAt_sq_sub_inner_sq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V × V) : HasStrictFDerivAt (fun (y : V × V) => ‖y.1‖ ^ 2 * ‖y.2‖ ^ 2 - inner ℝ y.1 y.2 ^ 2) (((innerSL ℝ) ((2 * ‖x.2‖ ^ 2) • x.1 - (2 * inner ℝ x.1 x.2) • x.2)).coprod ((innerSL ℝ) ((2 * ‖x.1‖ ^ 2) • x.2 - (2 * inner ℝ x.1 x.2) • x.1))) x

The partial gradients of the real Gram determinant G(q, p) = ‖q‖² ‖p‖² - ⟪q, p⟫² of a pair are ∇_q G = 2 ‖p‖² q - 2 ⟪q, p⟫ p and ∇_p G = 2 ‖q‖² p - 2 ⟪q, p⟫ q, as a strict derivative.

theorem TauCeti.sq_sub_inner_sq_smul_add_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a b c d : ℝ) (q p : V) : ‖a • q + b • p‖ ^ 2 * ‖c • q + d • p‖ ^ 2 - inner ℝ (a • q + b • p) (c • q + d • p) ^ 2 = (a * d - b * c) ^ 2 * (‖q‖ ^ 2 * ‖p‖ ^ 2 - inner ℝ q p ^ 2)

Replacing a pair (q, p) by (a q + b p, c q + d p) multiplies its real Gram determinant ‖q‖² ‖p‖² - ⟪q, p⟫² by the square of the determinant a d - b c of the change of basis.