Orthogonality and Cauchy–Schwarz give the single-block spectral bounds
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_regular · theorem · Teaching coverage
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).
Lean statement · singleBlockPrecision_regular
The statement uses IsHermitian over ℝ and explicit universal dot-product inequalities, avoiding entrywise matrix order and the default Pi norm.
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.
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)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.
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.
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.
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.
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.
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.
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.DeterminantFamilySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Real orthogonal matrix, literal coefficients and full coordinate-vector quantifier. | Matrix.orthogonalGroup (Fin n) ℝ; literal scalar/matrix formula; IsHermitian over ℝ and dotProduct. | same | Real Hermitian means symmetric, and dotProduct v v is the Euclidean squared norm; no entrywise matrix order or Pi norm is used. |
Only the single-block equation (26). Full block diagonal assembly, Gaussian normalization, unique minimizer and both query-complexity lower bounds remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: Ambient d and n<=d are eliminated for the isolated single-block theorem; this is not a strengthened assumption or full-block conclusion. — The source proof through (26) uses no d; choose d=n to realize any n>=3. The English lesson consistently claims only a single block.
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 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.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.