Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

The literal full precision, including its residual identity block

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.blockPrecision · def · Teaching coverage

Read this first

Mathematical statement

Within the standing range kappa≥4 and 3≤n≤d, put k=floor(d/n). For every tuple of k real orthogonal n by n matrices, define the d by d precision as diag(A_O1,...,A_Ok,I_(d-kn)), where A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T).

\[A_{\boldsymbol O}=\operatorname{diag}(A_{O_1},\ldots,A_{O_k},I_{d-kn}),\qquad k=\lfloor d/n\rfloor\]
Lean statement · blockPrecision

Coordinates are Fin d with the exact quotient/remainder adapter; dotProduct represents the Euclidean quadratic form.

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.

Download module (.lean)
noncomputable def blockPrecision {d n : ℕ} (κ : ℝ)
    (O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin d) (Fin d) ℝ

Exact module and namespace context

Proof roadmap

  1. 1Use consecutive coordinates

    Mathlib indexes equal blocks by (inner coordinate, block). Swap these indices before flattening, so the original coordinate is inner+n*block. The residual coordinate starts at k*n.

  2. 2Retain the residual identity

    Euclidean division gives d=k*n+r with r=d mod n=d-k*n. Reindex the literal block diagonal to Fin d. When r=0, Fin0 is empty and no residual coordinate is introduced.

Full assumptions and notation

All objects and hypotheses

  • d and n are natural dimensions; kappa is a real number.
  • n≥3, n≤d and kappa≥4 are the source standing range.
  • O is a tuple indexed by Fin(d/n), with each matrix in the full real orthogonal group on Fin n.
  • The literal algebraic definition extends to every natural d,n and real kappa; spectral and minimizer theorems retain the source range.

Construction and meaning

1. Use consecutive coordinates

Mathlib indexes equal blocks by (inner coordinate, block). Swap these indices before flattening, so the original coordinate is inner+n*block. The residual coordinate starts at k*n.

\[(i,j)\mapsto i+nj,\qquad z_t\mapsto kn+t\]
Corresponding Lean step

The private blockCoordinates uses prodComm, finProdFinEquiv, sumCongr, finSumFinEquiv and finCongr.

2. Retain the residual identity

Euclidean division gives d=k*n+r with r=d mod n=d-k*n. Reindex the literal block diagonal to Fin d. When r=0, Fin0 is empty and no residual coordinate is introduced.

\[d=kn+r,\quad r=d\bmod n=d-kn\]
Corresponding Lean step

blockPrecision applies Matrix.reindex to fromBlocks (blockDiagonal ...) 0 0 1; no padding or fallback replaces the residual block.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · blockPrecision

The adjacent checked Lean body supplies the actual matrix assembly and all internal dependencies.

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.

Download module (.lean)
noncomputable def blockPrecision {d n : ℕ} (κ : ℝ)
    (O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin d) (Fin d) ℝ :=
  Matrix.reindex (blockCoordinates d n) (blockCoordinates d n)
    (Matrix.fromBlocks (Matrix.blockDiagonal (fun j => singleBlockPrecision κ (O j)))
      0 0 (1 : Matrix (Fin (d % n)) (Fin (d % n)) ℝ))

Exact module and namespace context

Scope and omitted-condition boundaries
  • Only determinant-family regularity and the quadratic minimum in Lemma3.4/B.8. Gaussian normalization, Haar posterior laws, oracle indistinguishability, test separation and both main complexity lower bounds remain open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Matrix.blockDiagonal
  • Matrix.fromBlocks
  • Matrix.reindex
  • finProdFinEquiv
  • finSumFinEquiv
  • Nat.div_add_mod

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.