Sum the actual single-block estimates in the original coordinates

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. ASTIS mathematical restatement.

Complete source statement (Samplinglib restatement)

For n>=3,n<=d,kappa>=4 and every tuple of floor(d/n) real orthogonal n by n matrices, the literal d-dimensional precision A is symmetric and every x in R^d satisfies x^T x<=x^T A x<=kappa x^T x. Hence A belongs to the source admissible precision class.

Lemma3.4/B.8

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Sum the actual single-block estimates in the original coordinates

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

Read this first

Mathematical statement

For n≥3,n≤d,kappa≥4 and every tuple of floor(d/n) real orthogonal n by n matrices, the literal d-dimensional precision A is symmetric and every x in R^d satisfies x^T x≤x^T A x≤kappa x^T x. Hence A belongs to the source admissible precision class.

\[A=A^\top,\qquad \|x\|_2^2\le x^\top A x\le\kappa\|x\|_2^2\quad(\forall x\in\mathbb R^d)\]

Lean statement · blockPrecision_regular

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)

theorem blockPrecision_regular {d n : ℕ} (hn : 3 ≤ n) (_hnd : n ≤ d)
    {κ : ℝ} (hκ : 4 ≤ κ)
    (O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) :
    (blockPrecision κ O).IsHermitian ∧
      ∀ x : Fin d → ℝ,
        x ⬝ᵥ x ≤ x ⬝ᵥ (blockPrecision κ O *ᵥ x) ∧
        x ⬝ᵥ (blockPrecision κ O *ᵥ x) ≤ κ * (x ⬝ᵥ x)

Exact module and namespace context

Proof roadmap

1Symmetry survives block assembly
The existing single-block theorem proves each A_Oj symmetric. Block diagonal assembly, the identity tail and the coordinate equivalence preserve real Hermitianity, which is symmetry.
2Split the two quadratic forms
Pull x back through the exact coordinate equivalence. Its blocks are v_j and its residual is z. Matrix-vector multiplication has no cross-block terms, so both expressions split into finite sums.
3Sum the existing bounds and handle the tail
Apply the compiled single-block lower and upper bounds to each v_j and sum them. The standing kappa≥4 implies kappa≥1, so the residual squared norm is at most kappa times itself. Empty residual sums also cover kn=d.

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.

Mathematical proof

1. Symmetry survives block assembly

The existing single-block theorem proves each A_Oj symmetric. Block diagonal assembly, the identity tail and the coordinate equivalence preserve real Hermitianity, which is symmetry.

\[A_{O_j}=A_{O_j}^\top\ (\forall j)\ \Longrightarrow\ A=A^\top\]

Corresponding Lean step

hB uses singleBlockPrecision_regular, isHermitian_blockDiagonal_iff and IsHermitian.fromBlocks; IsHermitian.reindex returns the result on Fin d.

2. Split the two quadratic forms

Pull x back through the exact coordinate equivalence. Its blocks are v_j and its residual is z. Matrix-vector multiplication has no cross-block terms, so both expressions split into finite sums.

\[\|x\|_2^2=\sum_j\|v_j\|_2^2+\|z\|_2^2,\qquad x^\top Ax=\sum_jv_j^\top A_{O_j}v_j+\|z\|_2^2\]

Corresponding Lean step

hchange proves the quadratic form is preserved under reindex. hvec, hnorm and hquad expand the actual fromBlocks/blockDiagonal matrix, using finite sum reordering.

3. Sum the existing bounds and handle the tail

Apply the compiled single-block lower and upper bounds to each v_j and sum them. The standing kappa≥4 implies kappa≥1, so the residual squared norm is at most kappa times itself. Empty residual sums also cover kn=d.

\[\sum_j\|v_j\|_2^2+\|z\|_2^2\le x^\top Ax\le\kappa\sum_j\|v_j\|_2^2+\|z\|_2^2\le\kappa\|x\|_2^2\]

Corresponding Lean step

hlo and hupp call singleBlockPrecision_regular inside the proof; htail derives its coefficient condition from hκ. No spectral estimate is a public hypothesis.

Lean verification

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

Lean proof · blockPrecision_regular

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

Download module (.lean)

theorem blockPrecision_regular {d n : ℕ} (hn : 3 ≤ n) (_hnd : n ≤ d)
    {κ : ℝ} (hκ : 4 ≤ κ)
    (O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) :
    (blockPrecision κ O).IsHermitian ∧
      ∀ x : Fin d → ℝ,
        x ⬝ᵥ x ≤ x ⬝ᵥ (blockPrecision κ O *ᵥ x) ∧
        x ⬝ᵥ (blockPrecision κ O *ᵥ x) ≤ κ * (x ⬝ᵥ x) := by
  let e := blockCoordinates d n
  let B := Matrix.fromBlocks (Matrix.blockDiagonal (fun j => singleBlockPrecision κ (O j)))
    0 0 (1 : Matrix (Fin (d % n)) (Fin (d % n)) ℝ)
  have hB : B.IsHermitian := by
    apply Matrix.IsHermitian.fromBlocks
    · exact Matrix.isHermitian_blockDiagonal_iff.mpr
        (fun j => (singleBlockPrecision_regular hn hκ (O j)).1)
    · simp
    · exact Matrix.isHermitian_one
  constructor
  · exact hB.reindex e
  · intro x
    let y := x ∘ e
    let v := fun j i => y (Sum.inl (i, j))
    let z := y ∘ Sum.inr
    have hchange (M : Matrix ((Fin n × Fin (d / n)) ⊕ Fin (d % n))
        ((Fin n × Fin (d / n)) ⊕ Fin (d % n)) ℝ) :
        x ⬝ᵥ (Matrix.reindex e e M *ᵥ x) = y ⬝ᵥ (M *ᵥ y) := by
      change x ⬝ᵥ (M.submatrix e.symm e.symm *ᵥ x) = _
      rw [Matrix.submatrix_mulVec_equiv]
      exact dotProduct_comp_equiv_symm _ _ e
    have hvec (w : Fin n × Fin (d / n) → ℝ) (i : Fin n) (j : Fin (d / n)) :
        (Matrix.blockDiagonal (fun j => singleBlockPrecision κ (O j)) *ᵥ w) (i, j) =
          (singleBlockPrecision κ (O j) *ᵥ (fun a => w (a, j))) i := by
      simp [Matrix.mulVec, dotProduct, Fintype.sum_prod_type, Matrix.blockDiagonal_apply,
        ite_mul]
    have hnorm : x ⬝ᵥ x = (∑ j, v j ⬝ᵥ v j) + z ⬝ᵥ z := by
      have h := e.sum_comp (fun i => x i * x i)
      change y ⬝ᵥ y = x ⬝ᵥ x at h
      rw [← h, Matrix.dotProduct_block]
      congr 1
      simp only [dotProduct, Fintype.sum_prod_type]
      exact Finset.sum_comm
    have hquad : x ⬝ᵥ (blockPrecision κ O *ᵥ x) =
        (∑ j, v j ⬝ᵥ (singleBlockPrecision κ (O j) *ᵥ v j)) + z ⬝ᵥ z := by
      change x ⬝ᵥ (Matrix.reindex e e B *ᵥ x) = _
      rw [hchange]
      simp only [B, Matrix.fromBlocks_mulVec, Matrix.zero_mulVec, Matrix.one_mulVec,
        add_zero, zero_add]
      rw [Matrix.dotProduct_block]
      congr 1
      simp only [dotProduct, Fintype.sum_prod_type, Function.comp_apply, Sum.elim_inl,
        hvec]
      exact Finset.sum_comm
    have hlo : (∑ j, v j ⬝ᵥ v j) ≤
        ∑ j, v j ⬝ᵥ (singleBlockPrecision κ (O j) *ᵥ v j) :=
      Finset.sum_le_sum (fun j _ => ((singleBlockPrecision_regular hn hκ (O j)).2 (v j)).1)
    have hupp : (∑ j, v j ⬝ᵥ (singleBlockPrecision κ (O j) *ᵥ v j)) ≤
        κ * (∑ j, v j ⬝ᵥ v j) := by
      rw [Finset.mul_sum]
      exact Finset.sum_le_sum (fun j _ =>
        ((singleBlockPrecision_regular hn hκ (O j)).2 (v j)).2)
    have hz : 0 ≤ z ⬝ᵥ z := Finset.sum_nonneg (fun i _ => mul_self_nonneg (z i))
    have htail : z ⬝ᵥ z ≤ κ * (z ⬝ᵥ z) := by
      simpa using mul_le_mul_of_nonneg_right (show (1 : ℝ) ≤ κ by linarith) hz
    rw [hnorm, hquad]
    constructor <;> nlinarith

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
n>=3,n<=d,kappa>=4; k=floor(d/n); residual d-k*n.	The theorem retains n>=3,n<=d,kappa>=4; Fin(d/n) blocks and Fin(d%n) residual, with contiguous coordinate equivalence.	same	Euclidean division identifies d%n with d-k*n. Real Hermitianity and universal dot-product bounds express source symmetry and Loewner bounds; no Pi norm or entrywise matrix order is used.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

conclusion: Loewner bounds for the real symmetric precision are expressed by equivalent inequalities for every quadratic form. — These are the same finite-dimensional real symmetric matrix conditions; Appendix B.3 derives class membership from precisely these inequalities.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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.isHermitian_blockDiagonal_iff
Matrix.IsHermitian.fromBlocks
Matrix.IsHermitian.reindex
Matrix.submatrix_mulVec_equiv
Matrix.dotProduct_block
Finset.sum_le_sum

Mathematical sources

Source block family and full regularity lemma — Literal equation(5), block quadratic bounds and unique minimum only.

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

Sum the actual single-block estimates in the original coordinates

Complete source statement (Samplinglib restatement)

Lemma3.4/B.8

Read the formalized proofs

Sum the actual single-block estimates in the original coordinates

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Symmetry survives block assembly

2. Split the two quadratic forms

3. Sum the existing bounds and handle the tail

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?