Leading Gram block and pivot square (gramTake, pivotSq)

Definition

gramTake

by sensei · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

harmonic-analysiskakeyalinear-algebra

For vectors $v_1,\dots,v_r$ in $\mathbb{R}^d$ , $G_k$ is the $k \times k$ Gram matrix of the first $k$ vectors, and the pivot $\pi_k^2 = \det G_{k+1}/\det G_k$ is the squared orthogonal distance of $v_{k+1}$ from the span of the previous vectors.

Definition code

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.Notation

/-!
# Filtered descent — Gram–Schmidt pivots (paper (32)–(42))

The Gram–Schmidt pivot decomposition of the ordered Cauchy–Binet identity.
For an ordered `r`-tuple of vectors, `p_j^2 = det G_j / det G_{j-1}` is the
squared distance of the `j`-th vector to the span of the previous ones
(paper (32)–(33)), and `|det S| = ∏_j p_j` (paper (36)–(42)).
-/

namespace FilteredDescent

/-- Gram matrix of the leading `k`-subfamily of `s` (embedded as `k × k`). -/
noncomputable def gramTake {r d : ℕ} (s : Fin r → (Fin d → ℝ)) (k : ℕ)
    (hk : k ≤ r) : Matrix (Fin k) (Fin k) ℝ :=
  Matrix.of (fun i j =>
    ∑ a, s ⟨i.val, lt_of_lt_of_le i.isLt hk⟩ a * s ⟨j.val, lt_of_lt_of_le j.isLt hk⟩ a)

/-- Gram–Schmidt pivot (paper (32)–(33)):
`p_j^2 = det G_{j+1} / det G_j`, the squared distance of `s_j` to the span of
the previous vectors.  Positivity of the Gram determinants is a hypothesis
of the pivot dichotomy theorem, not of this definition. -/
noncomputable def pivotSq {r d : ℕ} (s : Fin r → (Fin d → ℝ)) (j : Fin r) : ℝ :=
  (gramTake s (j.val + 1) (Nat.succ_le_of_lt j.isLt)).det /
    (gramTake s j.val (le_of_lt j.isLt)).det

end FilteredDescent

Source

Cai, Filtered Descent for the Physical Kakeya Incidence, 2026, https://cchx0000.github.io/papers/filtered-descent-physical-kakeya/filtered-descent-physical-kakeya.pdf, §4 ((32)–(42))

Read-back

What the Lean code literally says, in plain math · muse-spark

I have read both the auditor instructions and the Lean file. I have not consulted any other material. Here are the blind read-backs.

Read-back: `FilteredDescent.gramTake`

For any natural numbers $r$ and $d$ (both implicit), any ordered $r$ -tuple $s = (s_0, \dots, s_{r-1})$ of vectors in $\mathbb{R}^d$ (each vector given as a function $\{1,\dots,d\} \to \mathbb{R}$ ), any natural number $k$ , and any proof $h_k$ that $k \le r$ , gramTake produces a $k \times k$ real matrix whose $(i,j)$ -entry, for $i, j \in \{0, \dots, k-1\}$ , is the sum

G_{i,j} = \sum_{a=1}^{d} s_i(a)\, s_j(a),

i.e. the ordinary Euclidean dot product of the $i$ -th and $j$ -th vectors among the first $k$ vectors of $s$ (the indices $i, j$ are coerced into $\{0,\dots,r-1\}$ using $i < k \le r$ , so only the leading $k$ -subfamily $s_0, \dots, s_{k-1}$ is ever referenced). In other words it is the Gram matrix of the first $k$ vectors of $s$ . Edge cases included silently by the quantifiers: $k = 0$ is allowed and yields the empty $0 \times 0$ matrix; $k = r$ is allowed; if $d = 0$ every entry is an empty sum, hence $0$ . The definition is marked noncomputable and carries no hypotheses beyond $k \le r$ — in particular nothing is assumed about linear independence or about any determinant.

Read-back: `FilteredDescent.pivotSq`

For any natural numbers $r$ and $d$ (implicit), any ordered $r$ -tuple $s = (s_0, \dots, s_{r-1})$ of vectors in $\mathbb{R}^d$ , and any index $j \in \{0, \dots, r-1\}$ , pivotSq returns the real number

\frac{\det G_{j+1}}{\det G_j},

where $G_m$ denotes the $m \times m$ Gram matrix of the first $m$ vectors of $s$ as computed by gramTake — so the numerator is the determinant of the Gram matrix of $s_0, \dots, s_j$ and the denominator is the determinant of the Gram matrix of $s_0, \dots, s_{j-1}$ (with $G_0$ the empty $0 \times 0$ matrix, whose determinant is $1$ ; hence for $j = 0$ the value is $\|s_0\|^2 / 1 = \|s_0\|^2$ ). The two proof arguments supplied to gramTake (that $j+1 \le r$ and $j \le r$ ) are mere evidence for the $k \le r$ requirement and do not affect the value. Crucially, the code imposes no non-vanishing or positivity hypothesis on either determinant: since division on the reals is total in Lean, if $\det G_j = 0$ the result is $0$ by the $x/0 = 0$ convention, and the value may in principle be zero (or, formally, anything the determinant ratio yields) — the file's own doc comment notes that positivity of these Gram determinants is left as a hypothesis of a separate theorem, not of this definition.

View graph

Leading Gram block and pivot square (gramTake, pivotSq)

Read-back: FilteredDescent.gramTake

Read-back: FilteredDescent.pivotSq

Read-back: `FilteredDescent.gramTake`

Read-back: `FilteredDescent.pivotSq`