Move the determinant sign inside the normalization factor
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_signed_sqrt_det · theorem · Teaching coverage
Mathematical statement
For every natural n≥3, real kappa≥4 and real orthogonal n by n matrix O of either determinant sign, det(O) sqrt(det(A_O)) equals 2^(-n) det((sqrt(kappa)+1)O-(sqrt(kappa)-1)I).
Lean statement · singleBlockPrecision_signed_sqrt_det
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_signed_sqrt_det {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
(hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
(O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det =
(1 / (2 : ℝ) ^ n) *
(((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).det)Proof roadmap
- 1Multiply by the transpose inside the determinant
The exact matrix identity O^T M=(sqrt(kappa)+1)O^T-(sqrt(kappa)-1)I follows from O^T O=I. Determinant multiplicativity and det(O^T)=det(O) bring the sign inside.
- 2Transpose once more
A determinant equals that of its transpose. Combine the preceding identity with the actual square-root theorem, leaving O rather than O^T in the final formula. This works for both determinant components.
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. Multiply by the transpose inside the determinant
The exact matrix identity O^T M=(sqrt(kappa)+1)O^T-(sqrt(kappa)-1)I follows from O^T O=I. Determinant multiplicativity and det(O^T)=det(O) bring the sign inside.
Corresponding Lean step
hmatrix proves the matrix equality from orthogonality; hdet is its determinant image, using det_mul and det_transpose.
2. Transpose once more
A determinant equals that of its transpose. Combine the preceding identity with the actual square-root theorem, leaving O rather than O^T in the final formula. This works for both determinant components.
Corresponding Lean step
The proof calls singleBlockPrecision_sqrt_det, not an assumed Gaussian normalization law or a sign-restricted orthogonal subgroup.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · singleBlockPrecision_signed_sqrt_det
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_signed_sqrt_det {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
(hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
(O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det =
(1 / (2 : ℝ) ^ n) *
(((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).det) := 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
have hmatrix : (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) ℝ)) =
((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).transpose := by
simp only [Matrix.mul_sub, Matrix.mul_smul, Matrix.mul_one, horth,
Matrix.transpose_sub, Matrix.transpose_smul, Matrix.transpose_one]
have hdet := congrArg Matrix.det hmatrix
rw [Matrix.det_mul, Matrix.det_transpose, Matrix.det_transpose] at hdet
rw [singleBlockPrecision_sqrt_det hn hκ O]
calc
_ = (1 / (2 : ℝ) ^ n) *
((O : Matrix (Fin n) (Fin n) ℝ).det *
((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
(Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).det) := by ring
_ = _ := by rw [hdet]
end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamilySource 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.
- scopes: A disclosed proof-route change establishes the required positive determinant conclusion without separately formalizing the quantitative source norm estimate. No semantic weakening of Eq17 or Eq18 results. — The source proves ||(aI−tO)v||≥(a−t)||v||≥2||v|| on 0≤t≤sqrt(κ)−1, then uses invertibility and continuity. Lean proves the same required nonsingularity by a squared-coordinate-norm kernel contradiction and continuity. This is a valid alternate route to the sign conclusion; the quantitative norm inequality itself is not a separately formalized theorem in the supplied module. The English lesson explicitly discloses this distinction. Its claim that the estimate is retained elsewhere in the source graph is outside these permitted review inputs and is not independently certified here. I checked the full packet module, including private shiftedOrthogonal_det_pos: from 0≤b<a and t∈[0,b], a>0 and a²−t²>0. Orthogonality gives (Ov)·(Ov)=v·v. A zero determinant yields a nonzero kernel vector, av=tOv, and hence (a²−t²)(v·v)=0, contradicting v·v>0. The continuous determinant path starts at det(aI)=a^n>0; an endpoint ≤0 would cross zero by IVT. Thus its endpoint is positive for every orthogonal O, without any determinant-component restriction. Instantiating a=sqrt(κ)+1,b=sqrt(κ)−1 uses κ≥4 to obtain sqrt(κ)≥2; these are derived facts, not additional source binders.
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
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecisionAutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_sqrt_det
Mathlib API called (external library)
- Matrix.mem_orthogonalGroup_iff'
- Matrix.det_mul
- Matrix.det_transpose
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.