Samplinglib mathematical lesson

The quadratic potential has its unique minimum at zero

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

Read this first

Mathematical statement

Under the same n≥3,n≤d,kappa≥4 and orthogonal tuple assumptions, the actual potential f_A(x)=(1/2)x^T A x has f_A(0)=0, is nonnegative for every x, and equals zero if and only if x=0. Thus its unique minimizer is0 and its minimum value is0.

\[f_A(0)=0,\qquad f_A(x)\ge0,\qquad f_A(x)=0\iff x=0\]

Lean statement · blockPrecision_unique_minimizer

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_unique_minimizer {d n : ℕ} (hn : 3 ≤ n) (hnd : n ≤ d)
    {κ : ℝ} (hκ : 4 ≤ κ)
    (O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) :
    let f : (Fin d → ℝ) → ℝ := fun x => (1 / 2 : ℝ) * (x ⬝ᵥ (blockPrecision κ O *ᵥ x))
    f 0 = 0 ∧ ∀ x, 0 ≤ f x ∧ (f x = 0 ↔ x = 0)

Exact module and namespace context

Proof roadmap

1The origin has value zero
The literal quadratic expression vanishes at the zero vector.
2The lower spectral bound gives nonnegativity
Apply the actual full-precision theorem to the same x. Since its coordinate squared sum is nonnegative, so is the potential.
3Zero energy forces every coordinate to vanish
If f_A(x)=0, the lower bound forces the sum of squared coordinates to be0. Each nonnegative summand is at most this sum, hence each coordinate is0. Conversely x=0 has zero energy. Combined with nonnegativity, this gives strict positivity for x≠0 and the unique minimum.

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. The origin has value zero

The literal quadratic expression vanishes at the zero vector.

\[f_A(0)=\tfrac12 0^\top A0=0\]

Corresponding Lean step

The first conjunct unfolds the displayed potential and simplifies zero matrix-vector and dot products.

2. The lower spectral bound gives nonnegativity

Apply the actual full-precision theorem to the same x. Since its coordinate squared sum is nonnegative, so is the potential.

\[f_A(x)=\tfrac12x^\top Ax\ge\tfrac12\|x\|_2^2\ge0\]

Corresponding Lean step

hlow is produced by blockPrecision_regular, with the same hn,hnd,hκ and O. hnonneg is the finite sum of coordinate squares.

3. Zero energy forces every coordinate to vanish

If f_A(x)=0, the lower bound forces the sum of squared coordinates to be0. Each nonnegative summand is at most this sum, hence each coordinate is0. Conversely x=0 has zero energy. Combined with nonnegativity, this gives strict positivity for x≠0 and the unique minimum.

\[f_A(x)=0\Longrightarrow\sum_i x_i^2=0\Longrightarrow (\forall i,\ x_i=0)\Longrightarrow x=0\]

Corresponding Lean step

The proof uses Finset.single_le_sum and mul_self_eq_zero. The theorem packages nonnegativity and the exact zero set; this is equivalent to the source unique-minimizer conclusion.

Lean verification

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

Lean proof · blockPrecision_unique_minimizer

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

Download module (.lean)

theorem blockPrecision_unique_minimizer {d n : ℕ} (hn : 3 ≤ n) (hnd : n ≤ d)
    {κ : ℝ} (hκ : 4 ≤ κ)
    (O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) :
    let f : (Fin d → ℝ) → ℝ := fun x => (1 / 2 : ℝ) * (x ⬝ᵥ (blockPrecision κ O *ᵥ x))
    f 0 = 0 ∧ ∀ x, 0 ≤ f x ∧ (f x = 0 ↔ x = 0) := by
  dsimp
  constructor
  · simp
  intro x
  have hlow := ((blockPrecision_regular hn hnd hκ O).2 x).1
  have hnonneg : 0 ≤ x ⬝ᵥ x :=
    Finset.sum_nonneg (fun i _ => mul_self_nonneg (x i))
  constructor
  · nlinarith
  constructor
  · intro h
    have hzero : x ⬝ᵥ x = 0 := by nlinarith
    ext i
    change x i = 0
    have hi := Finset.single_le_sum (fun j (_ : j ∈ (Finset.univ : Finset (Fin d))) =>
      mul_self_nonneg (x j)) (Finset.mem_univ i)
    change x i * x i ≤ x ⬝ᵥ x at hi
    rw [hzero] at hi
    exact mul_self_eq_zero.mp (le_antisymm hi (mul_self_nonneg (x i)))
  · intro h
    subst x
    simp

end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily

Exact module and namespace context

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)

Finset.single_le_sum
mul_self_eq_zero

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.