Samplinglib mathematical lesson

Move the determinant sign inside the normalization factor

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

Read this first

Mathematical statement

For every natural n≥3, real kappa≥4 and real orthogonal n by n matrix O of either determinant sign, det(O) sqrt(det(A_O)) equals 2^(-n) det((sqrt(kappa)+1)O-(sqrt(kappa)-1)I).

\[\det(O)\sqrt{\det A_O}=2^{-n}\det\bigl((\sqrt\kappa+1)O-(\sqrt\kappa-1)I\bigr)\]

Lean statement · singleBlockPrecision_signed_sqrt_det

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_signed_sqrt_det {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det =
      (1 / (2 : ℝ) ^ n) *
      (((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).det)

Exact module and namespace context

Proof roadmap

1Multiply by the transpose inside the determinant
The exact matrix identity O^T M=(sqrt(kappa)+1)O^T-(sqrt(kappa)-1)I follows from O^T O=I. Determinant multiplicativity and det(O^T)=det(O) bring the sign inside.
2Transpose once more
A determinant equals that of its transpose. Combine the preceding identity with the actual square-root theorem, leaving O rather than O^T in the final formula. This works for both determinant components.

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. Multiply by the transpose inside the determinant

The exact matrix identity O^T M=(sqrt(kappa)+1)O^T-(sqrt(kappa)-1)I follows from O^T O=I. Determinant multiplicativity and det(O^T)=det(O) bring the sign inside.

\[\det(O)\det M=\det\bigl((\sqrt\kappa+1)O^\top-(\sqrt\kappa-1)I\bigr)\]

Corresponding Lean step

hmatrix proves the matrix equality from orthogonality; hdet is its determinant image, using det_mul and det_transpose.

2. Transpose once more

A determinant equals that of its transpose. Combine the preceding identity with the actual square-root theorem, leaving O rather than O^T in the final formula. This works for both determinant components.

\[\det\bigl((\sqrt\kappa+1)O^\top-(\sqrt\kappa-1)I\bigr)=\det\bigl((\sqrt\kappa+1)O-(\sqrt\kappa-1)I\bigr)\]

Corresponding Lean step

The proof calls singleBlockPrecision_sqrt_det, not an assumed Gaussian normalization law or a sign-restricted orthogonal subgroup.

Lean verification

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

Lean proof · singleBlockPrecision_signed_sqrt_det

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

Download module (.lean)

theorem singleBlockPrecision_signed_sqrt_det {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det =
      (1 / (2 : ℝ) ^ n) *
      (((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).det) := 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
  have hmatrix : (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) ℝ)) =
      ((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).transpose := by
    simp only [Matrix.mul_sub, Matrix.mul_smul, Matrix.mul_one, horth,
      Matrix.transpose_sub, Matrix.transpose_smul, Matrix.transpose_one]
  have hdet := congrArg Matrix.det hmatrix
  rw [Matrix.det_mul, Matrix.det_transpose, Matrix.det_transpose] at hdet
  rw [singleBlockPrecision_sqrt_det hn hκ O]
  calc
    _ = (1 / (2 : ℝ) ^ n) *
        ((O : Matrix (Fin n) (Fin n) ℝ).det *
          ((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
            (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).det) := by ring
    _ = _ := by rw [hdet]

end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily

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

Mathlib API called (external library)

Matrix.mem_orthogonalGroup_iff'
Matrix.det_mul
Matrix.det_transpose

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.