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

Single-block precision: the literal formula (4)

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

Read this first

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.

\[A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top)\]
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.

Download module (.lean)
noncomputable def singleBlockPrecision {n : ℕ} (κ : ℝ)
    (O : Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ

Exact module and namespace context

Proof roadmap

  1. 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.

\[A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top)\]
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.

Download module (.lean)
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)

Exact module and namespace context

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

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