Single-block precision: the literal formula (4)
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision · def · Teaching coverage
Mathematical statement
For every natural dimension n, real parameter kappa and real orthogonal matrix O, define A_O by the displayed expression. The definition is algebraic on the whole carrier; the regularity theorem retains the source standing range n≥3 and kappa≥4.
Lean statement · singleBlockPrecision
A literal matrix-valued definition on every n, κ and O.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
noncomputable def singleBlockPrecision {n : ℕ} (κ : ℝ)
(O : Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝProof roadmap
- 1Retain the coefficients and transpose
The identity coefficient is (kappa+1)/2, while the coefficient of O+O^T is -(kappa-1)/4. The definition contains no precomputed spectral estimate.
Full assumptions and notation
All objects and hypotheses
- n is a natural number; κ is real.
- O is an n by n real orthogonal matrix; both determinant signs are allowed.
Construction and meaning
1. Retain the coefficients and transpose
The identity coefficient is (kappa+1)/2, while the coefficient of O+O^T is -(kappa-1)/4. The definition contains no precomputed spectral estimate.
Corresponding Lean step
The body is exactly the scalar multiples, matrix addition, transpose and subtraction shown in the formula.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · singleBlockPrecision
No existence or fallback branch: this is the displayed algebraic expression.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
noncomputable def singleBlockPrecision {n : ℕ} (κ : ℝ)
(O : Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ :=
((κ + 1) / 2) • (1 : Matrix (Fin n) (Fin n) ℝ) -
((κ - 1) / 4) • ((O : Matrix (Fin n) (Fin n) ℝ) +
(O : Matrix (Fin n) (Fin n) ℝ).transpose)Source assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Real orthogonal matrix, literal coefficients and full coordinate-vector quantifier. | Matrix.orthogonalGroup (Fin n) ℝ; literal scalar/matrix formula; IsHermitian over ℝ and dotProduct. | same | Real Hermitian means symmetric, and dotProduct v v is the Euclidean squared norm; no entrywise matrix order or Pi norm is used. |
| Section 3.1 uses kappa>=4 and 3<=n<=d in ambient dimension d. | The literal matrix-valued definition is total for every natural n and every real kappa; its regularity theorem retains n>=3 and kappa>=4. | generalization | This is only the same algebraic expression on a larger carrier. No off-source fallback, spectral estimate outside the theorem range, or ambient block conclusion is asserted. Ambient n<=d belongs to the later block construction. |
Only the single-block equation (26). Full block diagonal assembly, Gaussian normalization, unique minimizer and both query-complexity lower bounds remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: The literal matrix definition has a transparently larger algebraic carrier than the published construction range; the theorem range is unchanged. — The source restatement retains kappa>=4,3<=n<=d; the English lesson and candidate-assumptions row separately disclose the total definition and n>=3,kappa>=4 regularity boundary.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- Only the single-block equation (26). Full block diagonal assembly, Gaussian normalization, unique minimizer and both query-complexity lower bounds remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Matrix.orthogonalGroup
Mathematical sources
- Source equation (4) — Literal definition of one precision block.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.