Factor the actual precision as a positive square
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_factorization · theorem · Teaching coverage
Mathematical statement
For every natural n≥3, real kappa≥4 and real orthogonal n by n matrix O, put M=(sqrt(kappa)+1)I-(sqrt(kappa)-1)O. The literal precision A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T) equals (1/4) M^T M.
Lean statement · singleBlockPrecision_factorization
The source real precision is used literally; finite indices Fin n express the real n-dimensional matrix.
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_factorization {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
(hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
singleBlockPrecision κ O = (1 / 4 : ℝ) •
((((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).transpose) *
((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)))Proof roadmap
- 1Expand the orthogonal square
Write s=sqrt(kappa). Orthogonality gives O^T O=I. Expand the two factors, keeping O and O^T distinct.
- 2Use the nonnegative square root
The standing kappa≥4 implies kappa≥0, so s^2=kappa. The diagonal and cross coefficients then give the exact source precision.
Full assumptions and notation
All objects and hypotheses
- n is a natural number with n≥3, retaining the source standing block range.
- kappa is real with kappa≥4.
- O belongs to the full real orthogonal group O(n); determinant -1 and +1 are both included.
- All square roots are the nonnegative real square root. No Haar law, probabilistic average or integrability premise is part of these pointwise identities.
Mathematical proof
1. Expand the orthogonal square
Write s=sqrt(kappa). Orthogonality gives O^T O=I. Expand the two factors, keeping O and O^T distinct.
Corresponding Lean step
Use mem_orthogonalGroup_iff', transpose linearity and distributivity of matrix multiplication.
2. Use the nonnegative square root
The standing kappa≥4 implies kappa≥0, so s^2=kappa. The diagonal and cross coefficients then give the exact source precision.
Corresponding Lean step
After expanding matrix entries, ring normalization and Real.sq_sqrt prove the coefficients. The existing literal singleBlockPrecision is used unchanged.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · singleBlockPrecision_factorization
The adjacent checked Lean body supplies each actual algebraic and sign dependency internally.
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_factorization {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
(hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
singleBlockPrecision κ O = (1 / 4 : ℝ) •
((((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).transpose) *
((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ))) := by
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
simp only [Matrix.transpose_sub, Matrix.transpose_smul, Matrix.transpose_one,
Matrix.sub_mul, Matrix.mul_sub, Matrix.smul_mul, Matrix.mul_smul,
Matrix.one_mul, Matrix.mul_one, horth]
ext i j
simp only [singleBlockPrecision, Matrix.sub_apply, Matrix.add_apply,
Matrix.smul_apply, smul_eq_mul]
ring_nf
rw [Real.sq_sqrt (by linarith : 0 ≤ κ)]
ringSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| n>=3,kappa>=4 and an arbitrary real orthogonal O; the positive determinant branch is proved in the source. | Exactly these binders; positivity, invertibility and all estimates are derived inside the proof. | same | No convenience premise or restriction to SO(n) is introduced. The continuous path is represented on the same real interval; its nonsingularity uses squared norms rather than a separately stated reverse-triangle lower bound. |
Pointwise equations16-18 only. Haar probability and signed averaging, reflection/principal-minor cancellation and equation15, actual Gaussian laws/densities and Fubini, spherical Poisson identities, testing amplification, oracle indistinguishability, and both main lower bounds remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: The pointwise content is made explicit; no expectation theorem is being certified and no almost-everywhere exception is introduced. — A2.SS2.p1, Eq15, A2.SS2.SSS1.p2 versus module introduction, actual binders and lesson scope.
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
- Pointwise equations16-18 only. Haar probability and signed averaging, reflection/principal-minor cancellation and equation15, actual Gaussian laws/densities and Fubini, spherical Poisson identities, testing amplification, oracle indistinguishability, and both main lower bounds remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Matrix.mem_orthogonalGroup_iff'
- Real.sq_sqrt
- Matrix.transpose_sub
- Matrix.mul_sub
Mathematical sources
- Determinant normalization identities — Only the pointwise part through equation18, including its sign argument.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.