Samplinglib mathematical lesson

Factor the actual precision as a positive square

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_factorization · theorem · Teaching coverage

Read this first

Mathematical statement

For every natural n≥3, real kappa≥4 and real orthogonal n by n matrix O, put M=(sqrt(kappa)+1)I-(sqrt(kappa)-1)O. The literal precision A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T) equals (1/4) M^T M.

\[A_O=\tfrac14 M^\top M,\qquad M=(\sqrt\kappa+1)I-(\sqrt\kappa-1)O\]

Lean statement · singleBlockPrecision_factorization

The source real precision is used literally; finite indices Fin n express the real n-dimensional matrix.

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)

theorem singleBlockPrecision_factorization {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    singleBlockPrecision κ O = (1 / 4 : ℝ) •
      ((((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).transpose) *
       ((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)))

Exact module and namespace context

Proof roadmap

1Expand the orthogonal square
Write s=sqrt(kappa). Orthogonality gives O^T O=I. Expand the two factors, keeping O and O^T distinct.
2Use the nonnegative square root
The standing kappa≥4 implies kappa≥0, so s^2=kappa. The diagonal and cross coefficients then give the exact source precision.

Full assumptions and notation

All objects and hypotheses

n is a natural number with n≥3, retaining the source standing block range.
kappa is real with kappa≥4.
O belongs to the full real orthogonal group O(n); determinant -1 and +1 are both included.
All square roots are the nonnegative real square root. No Haar law, probabilistic average or integrability premise is part of these pointwise identities.

Mathematical proof

1. Expand the orthogonal square

Write s=sqrt(kappa). Orthogonality gives O^T O=I. Expand the two factors, keeping O and O^T distinct.

\[M^\top M=((s+1)^2+(s-1)^2)I-(s+1)(s-1)(O+O^\top)\]

Corresponding Lean step

Use mem_orthogonalGroup_iff', transpose linearity and distributivity of matrix multiplication.

2. Use the nonnegative square root

The standing kappa≥4 implies kappa≥0, so s^2=kappa. The diagonal and cross coefficients then give the exact source precision.

\[\tfrac14\bigl((s+1)^2+(s-1)^2\bigr)=\tfrac{\kappa+1}{2},\qquad \tfrac14(s+1)(s-1)=\tfrac{\kappa-1}{4}\]

Corresponding Lean step

After expanding matrix entries, ring normalization and Real.sq_sqrt prove the coefficients. The existing literal singleBlockPrecision is used unchanged.

Lean verification

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

Lean proof · singleBlockPrecision_factorization

The adjacent checked Lean body supplies each actual algebraic and sign dependency internally.

Download module (.lean)

theorem singleBlockPrecision_factorization {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    singleBlockPrecision κ O = (1 / 4 : ℝ) •
      ((((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).transpose) *
       ((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ))) := by
  have horth : (O : Matrix (Fin n) (Fin n) ℝ).transpose *
      (O : Matrix (Fin n) (Fin n) ℝ) = 1 :=
    (Matrix.mem_orthogonalGroup_iff' (Fin n) ℝ).mp O.property
  simp only [Matrix.transpose_sub, Matrix.transpose_smul, Matrix.transpose_one,
    Matrix.sub_mul, Matrix.mul_sub, Matrix.smul_mul, Matrix.mul_smul,
    Matrix.one_mul, Matrix.mul_one, horth]
  ext i j
  simp only [singleBlockPrecision, Matrix.sub_apply, Matrix.add_apply,
    Matrix.smul_apply, smul_eq_mul]
  ring_nf
  rw [Real.sq_sqrt (by linarith : 0 ≤ κ)]
  ring

Exact module and namespace context

Scope and omitted-condition boundaries

Pointwise equations16-18 only. Haar probability and signed averaging, reflection/principal-minor cancellation and equation15, actual Gaussian laws/densities and Fubini, spherical Poisson identities, testing amplification, oracle indistinguishability, and both main lower bounds remain open.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision

Mathlib API called (external library)

Matrix.mem_orthogonalGroup_iff'
Real.sq_sqrt
Matrix.transpose_sub
Matrix.mul_sub

Mathematical sources

Determinant normalization identities — Only the pointwise part through equation18, including its sign argument.

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