DeterminantFamily: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Single-block precision: the literal formula (4)
Orthogonality and Cauchy–Schwarz give the single-block spectral bounds

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

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.

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

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.

Samplinglib mathematical lesson

Orthogonality and Cauchy–Schwarz give the single-block spectral bounds

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

Read this first

Mathematical statement

Let n≥3, kappa≥4 and O belong to the real orthogonal group O(n). The matrix A_O in equation (4) is real symmetric, and every real vector v satisfies v^T v ≤ v^T A_O v ≤ kappa v^T v. This is the quadratic-form formulation of source equation (26).

\[A_O=A_O^\top,\qquad \|v\|_2^2\le v^\top A_Ov\le\kappa\|v\|_2^2\quad(\forall v\in\mathbb R^n)\]

Lean statement · singleBlockPrecision_regular

The statement uses IsHermitian over ℝ and explicit universal dot-product inequalities, avoiding entrywise matrix order and the default Pi norm.

Download module (.lean)

theorem singleBlockPrecision_regular {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    (singleBlockPrecision κ O).IsHermitian ∧
      ∀ v : Fin n → ℝ,
        v ⬝ᵥ v ≤ v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v) ∧
        v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v) ≤ κ * (v ⬝ᵥ v)

Exact module and namespace context

Proof roadmap

1Orthogonality preserves the Euclidean squared norm
Use O^T O=I to reduce (Ov)^T(Ov) to v^T v. Squared Euclidean norms are represented by sums of squared coordinates.
2Control the cross term
Finite-sum Cauchy–Schwarz bounds the square of the cross term. Together with v^T v≥0 this gives both signed inequalities. These estimates are derived inside the proof.
3Expand the quadratic form
Over the reals, v^T O^T v equals v^T O v, so the two transpose cross terms combine.
4Scale with the correct sign and prove symmetry
The standing kappa≥4 implies (kappa-1)/2≥0. Substituting the upper and lower cross-term bounds gives the lower and upper quadratic bounds respectively. Transpose fixes both I and O+O^T, hence A_O is symmetric.

Full assumptions and notation

All objects and hypotheses

n≥3 and κ≥4 are the standing range in Section 3.1.
O belongs to the full real orthogonal group O(n).
The bounds hold for every real coordinate vector, including zero.

Mathematical proof

1. Orthogonality preserves the Euclidean squared norm

Use O^T O=I to reduce (Ov)^T(Ov) to v^T v. Squared Euclidean norms are represented by sums of squared coordinates.

\[\|Ov\|_2^2=v^\top O^\top Ov=\|v\|_2^2\]

Corresponding Lean step

horth uses Matrix.mem_orthogonalGroup_iff'; hiso uses the transpose dot-product identity and matrix multiplication.

2. Control the cross term

Finite-sum Cauchy–Schwarz bounds the square of the cross term. Together with v^T v≥0 this gives both signed inequalities. These estimates are derived inside the proof.

\[|v^\top Ov|^2\le\|v\|_2^2\|Ov\|_2^2=\|v\|_2^4,\qquad-\|v\|_2^2\le v^\top Ov\le\|v\|_2^2\]

Corresponding Lean step

hcs applies Finset.sum_mul_sq_le_sq_mul_sq; hcross derives the two real bounds.

3. Expand the quadratic form

Over the reals, v^T O^T v equals v^T O v, so the two transpose cross terms combine.

\[v^\top A_Ov=\frac{\kappa+1}{2}\|v\|_2^2-\frac{\kappa-1}{2}v^\top Ov\]

Corresponding Lean step

htranspose is Matrix.dotProduct_transpose_mulVec; hexpand distributes mulVec and dotProduct and checks the coefficient algebra.

4. Scale with the correct sign and prove symmetry

The standing kappa≥4 implies (kappa-1)/2≥0. Substituting the upper and lower cross-term bounds gives the lower and upper quadratic bounds respectively. Transpose fixes both I and O+O^T, hence A_O is symmetric.

\[\frac{(\kappa+1)-(\kappa-1)}2=1,\qquad\frac{(\kappa+1)+(\kappa-1)}2=\kappa\]

Corresponding Lean step

hc discharges the sign from hκ. hlow/hupp scale hcross. The first conjunction proves real Hermitianity, equivalently symmetry.

Lean verification

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

Lean proof · singleBlockPrecision_regular

The checked proof follows the source orthogonality → Cauchy–Schwarz → quadratic expansion route.

Download module (.lean)

theorem singleBlockPrecision_regular {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    (singleBlockPrecision κ O).IsHermitian ∧
      ∀ v : Fin n → ℝ,
        v ⬝ᵥ v ≤ v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v) ∧
        v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v) ≤ κ * (v ⬝ᵥ v) := by
  constructor
  · rw [Matrix.isHermitian_iff_isSymm]
    unfold Matrix.IsSymm singleBlockPrecision
    simp only [Matrix.transpose_sub, Matrix.transpose_smul, Matrix.transpose_one,
      Matrix.transpose_add, Matrix.transpose_transpose]
    rw [add_comm (O : Matrix (Fin n) (Fin n) ℝ).transpose]
  · intro v
    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 hiso : ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v) ⬝ᵥ
        ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v) = v ⬝ᵥ v := by
      rw [dotProduct_comm, ← Matrix.dotProduct_transpose_mulVec,
        Matrix.mulVec_mulVec, horth, Matrix.one_mulVec]
    have hq : 0 ≤ v ⬝ᵥ v := by
      exact Finset.sum_nonneg (fun i _ => mul_self_nonneg (v i))
    have hcs : (v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v)) ^ 2 ≤
        (v ⬝ᵥ v) ^ 2 := by
      have h := Finset.sum_mul_sq_le_sq_mul_sq Finset.univ v
        ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v)
      simp only [pow_two] at h ⊢
      change (v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v)) *
          (v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v)) ≤
        (v ⬝ᵥ v) * (((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v) ⬝ᵥ
          ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v)) at h
      rw [hiso] at h
      exact h
    have hcross : -(v ⬝ᵥ v) ≤ v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v) ∧
        v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v) ≤ v ⬝ᵥ v := by
      constructor <;> nlinarith
    have htranspose : v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ).transpose *ᵥ v) =
        v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v) :=
      Matrix.dotProduct_transpose_mulVec _ _ _
    have hexpand : v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v) =
        ((κ + 1) / 2) * (v ⬝ᵥ v) -
          ((κ - 1) / 2) * (v ⬝ᵥ ((O : Matrix (Fin n) (Fin n) ℝ) *ᵥ v)) := by
      simp only [singleBlockPrecision, Matrix.sub_mulVec, Matrix.smul_mulVec,
        Matrix.add_mulVec, Matrix.one_mulVec, dotProduct_sub, dotProduct_smul,
        dotProduct_add, htranspose, smul_eq_mul]
      ring
    have hc : 0 ≤ (κ - 1) / 2 := by linarith
    have hlow := mul_le_mul_of_nonneg_left hcross.2 hc
    have hupp := mul_le_mul_of_nonneg_left hcross.1 hc
    rw [hexpand]
    constructor <;> nlinarith

end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily

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

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision

Mathlib API called (external library)

Matrix.mem_orthogonalGroup_iff'
Matrix.dotProduct_transpose_mulVec
Matrix.mulVec_mulVec
Finset.sum_mul_sq_le_sq_mul_sq

Mathematical sources

Source single-block equation (26) — Single-block symmetry and quadratic bounds, not the full Lemma 3.4/B.8.

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