Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Rotate the literal signed Gaussian kernel average

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. ASTIS isolates the explicit-formula fixed-Q invariance step; Gaussian-law identification and the norm-axis conclusion are separate.

arXiv:2610.20492v1 · AppendixB2 standing range; AppendixB2.2 p4.1 fixed-Q conjugation covariance and full-Haar change of variable underlying Ex58. Only the literal Gaussian-formula average is covered. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let n>=3 and kappa>=4. For O in the full real orthogonal group, let A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T) be the existing literal precision, and define the explicit real formula p_O(x)=sqrt(det A_O)/(2pi)^(n/2) exp(-x^T A_O x/2) on real coordinate n-space, with n/2 a real exponent. For every vector x, O -> det(O)p_O(x) is absolutely integrable under the actual canonical normalized full-O(n) Haar probability. For every fixed Q in full O(n), including reflections, E[det(O)p_O(Qx)]=E[det(O)p_O(x)]. This statement concerns the displayed formula itself and does not identify it with the density of an actual Gaussian probability law.

  • The AppendixB2 standing bounds n>=3 and kappa>=4 are retained, although the explicit algebraic invariance proof needs less. No L1, continuity or covariance hypothesis is added.
  • The law is the same actual canonical normalized Borel Haar probability on the full real O(n); both determinant components are allowed.
  • Vectors are real coordinates on Fin n, dotProduct is the Euclidean quadratic form and Q acts by matrix multiplication. The formula uses real exponent (n:R)/2 and the nonnegative real square root.
  • The local formula p is literal. This theorem defines no Gaussian probability measure and assumes no density identification, normalization or covariance fact. Those remain separate obligations.

Fixed-Q signed-formula invariance

\[\mathbb E_{O\sim\mu_n}\!\left[\det(O)p_O(Qx)\right]=\mathbb E_{O\sim\mu_n}\!\left[\det(O)p_O(x)\right],\qquad Q\in O(n),\quad x\in\mathbb R^n\]

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

Rotate the literal signed Gaussian kernel average

AutoSamplingTheory.ExampleCases.GaussianComplexity.KernelRotation.signed_kernel_rotation_invariant · theorem · Teaching coverage

Read this first

Mathematical statement

Let n≥3 and kappa≥4. For O in the full real orthogonal group, let A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T) be the existing literal precision, and define the explicit real formula p_O(x)=sqrt(det A_O)/(2pi)^(n/2) exp(-x^T A_O x/2) on real coordinate n-space, with n/2 a real exponent. For every vector x, O → det(O)p_O(x) is absolutely integrable under the actual canonical normalized full-O(n) Haar probability. For every fixed Q in full O(n), including reflections, E[det(O)p_O(Qx)]=E[det(O)p_O(x)]. This statement concerns the displayed formula itself and does not identify it with the density of an actual Gaussian probability law.

\[\mathbb E_{O\sim\mu_n}\!\left[\det(O)p_O(Qx)\right]=\mathbb E_{O\sim\mu_n}\!\left[\det(O)p_O(x)\right],\qquad Q\in O(n),\quad x\in\mathbb R^n\]
Lean statement · signed_kernel_rotation_invariant

The local let spells out the complete real Gaussian formula; absolute integrability and every fixed-Q identity are conclusions.

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 signed_kernel_rotation_invariant {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (_hκ : 4 ≤ κ) :
    let p : Matrix.orthogonalGroup (Fin n) ℝ → (Fin n → ℝ) → ℝ :=
      fun O x => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-(x ⬝ᵥ (singleBlockPrecision κ O *ᵥ x)) / 2)
    (∀ x : Fin n → ℝ, Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O x) (orthogonalHaar n)) ∧
    ∀ (Q : Matrix.orthogonalGroup (Fin n) ℝ) (x : Fin n → ℝ),
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det *
          p O ((Q : Matrix (Fin n) (Fin n) ℝ) *ᵥ x) ∂orthogonalHaar n) =
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O x ∂orthogonalHaar n)

Exact module and namespace context

Proof roadmap

  1. 1Conjugate the actual precision

    Let C_Q(O)=QOQ^T. Expanding the existing literal precision, transpose reverses products and QQ^T=I. Thus conjugating O conjugates A_O by the same Q. This calculation is internal, not an extra covariance premise.

  2. 2Preserve both determinant factors

    Taking determinants in QQ^T=I gives (det Q)^2=1. Therefore conjugation preserves det(O), as a signed real number, and det(A_O). The square-root normalization in the literal kernel is consequently unchanged. No det Q=+1 restriction is imposed.

  3. 3Transport the quadratic exponent

    The conjugated precision and Q^T Q=I imply (Qx)^T A_{C_Q(O)}(Qx)=x^T A_Ox. Combining this with determinant preservation yields pointwise covariance for the literal kernel and its determinant weight.

  4. 4Keep exactly the same full Haar law

    The right translate of the actual Haar probability is still a Haar probability, so its uniqueness characterization identifies it with the original law. Compose that right translation with the existing canonical fixed-left invariance theorem. Their composition is C_Q, hence conjugation preserves the actual normalized full Haar law.

  5. 5Prove every fixed-vector average finite

    For fixed x, the precision entries, determinant and square root are continuous functions of O. The finite quadratic form and exponential preserve continuity. On compact O(n), this determinant-weighted formula has compact support and is integrable under the actual finite Haar probability. This proves the L1 output, including x=0.

  6. 6Change variables inside the genuine Haar average

    Apply the measure-preserving conjugation substitution to the integrand O → det(O)p_O(Qx), then use the pointwise covariance. The same normalized law appears on both sides and no exchange of spatial integrals occurs.

Full assumptions and notation

All objects and hypotheses

  • The AppendixB2 standing bounds n≥3 and kappa≥4 are retained, although the explicit algebraic invariance proof needs less. No L1, continuity or covariance hypothesis is added.
  • The law is the same actual canonical normalized Borel Haar probability on the full real O(n); both determinant components are allowed.
  • Vectors are real coordinates on Fin n, dotProduct is the Euclidean quadratic form and Q acts by matrix multiplication. The formula uses real exponent (n:R)/2 and the nonnegative real square root.
  • The local formula p is literal. This theorem defines no Gaussian probability measure and assumes no density identification, normalization or covariance fact. Those remain separate obligations.

Mathematical proof

1. Conjugate the actual precision

Let C_Q(O)=QOQ^T. Expanding the existing literal precision, transpose reverses products and QQ^T=I. Thus conjugating O conjugates A_O by the same Q. This calculation is internal, not an extra covariance premise.

\[A_{C_Q(O)}=QA_OQ^\top,\qquad Q^\top Q=QQ^\top=I\]
Corresponding Lean step

Private conjugation_algebra proves hA by the exact source precision body, transpose/matrix distributivity and both orthogonality identities.

2. Preserve both determinant factors

Taking determinants in QQ^T=I gives (det Q)^2=1. Therefore conjugation preserves det(O), as a signed real number, and det(A_O). The square-root normalization in the literal kernel is consequently unchanged. No det Q=+1 restriction is imposed.

\[\det C_Q(O)=\det O,\qquad\det A_{C_Q(O)}=\det A_O\]
Corresponding Lean step

The same private provider derives hd and hdet from Matrix.det_mul and Matrix.det_transpose, then obtains the exact determinant equalities.

3. Transport the quadratic exponent

The conjugated precision and Q^T Q=I imply (Qx)^T A_{C_Q(O)}(Qx)=x^T A_Ox. Combining this with determinant preservation yields pointwise covariance for the literal kernel and its determinant weight.

\[p_{C_Q(O)}(Qx)=p_O(x),\qquad\det C_Q(O)\,p_{C_Q(O)}(Qx)=\det O\,p_O(x)\]
Corresponding Lean step

conjugation_algebra proves the quadratic identity by actual mulVec and dotProduct transpose identities. The public proof combines it with the determinant facts in hcov.

4. Keep exactly the same full Haar law

The right translate of the actual Haar probability is still a Haar probability, so its uniqueness characterization identifies it with the original law. Compose that right translation with the existing canonical fixed-left invariance theorem. Their composition is C_Q, hence conjugation preserves the actual normalized full Haar law.

\[(C_Q)_*\mu_n=\mu_n,\qquad C_Q(O)=QOQ^{-1}\]
Corresponding Lean step

Private haar_conjugation consumes orthogonalHaar_spec, the canonical Mathlib Haar right-translation instance and Measure.isProbabilityMeasure_map, then genuinely calls orthogonalHaar_map_mul_left. No arbitrary invariant law or assumed conjugation identity is supplied.

5. Prove every fixed-vector average finite

For fixed x, the precision entries, determinant and square root are continuous functions of O. The finite quadratic form and exponential preserve continuity. On compact O(n), this determinant-weighted formula has compact support and is integrable under the actual finite Haar probability. This proves the L1 output, including x=0.

\[\left[O\mapsto\det(O)p_O(x)\right]\in L^1(\mu_n),\qquad x\in\mathbb R^n\]
Corresponding Lean step

hAc and hcont establish actual continuity; hL1 uses orthogonalHaar_spec and Continuous.integrable_of_hasCompactSupport. This is fixed-x Haar L1 only, not joint spatial domination or Fubini.

6. Change variables inside the genuine Haar average

Apply the measure-preserving conjugation substitution to the integrand O → det(O)p_O(Qx), then use the pointwise covariance. The same normalized law appears on both sides and no exchange of spatial integrals occurs.

\[\mathbb E[\det(O)p_O(Qx)]=\mathbb E[\det C_Q(O)\,p_{C_Q(O)}(Qx)]=\mathbb E[\det(O)p_O(x)]\]
Corresponding Lean step

The public proof builds the actual conjugation measurable embedding and MeasurePreserving map, applies MeasurePreserving.integral_comp, and finishes by integral_congr_ae with hcov. Orthogonal transitivity to the norm-axis point is not asserted here.

Lean verification

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

Lean proof · signed_kernel_rotation_invariant

Two reachable private providers produce actual Haar conjugation preservation and all precision/determinant/quadratic covariance facts; the public proof proves L1 and consumes both providers in the final average identity.

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 signed_kernel_rotation_invariant {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (_hκ : 4 ≤ κ) :
    let p : Matrix.orthogonalGroup (Fin n) ℝ → (Fin n → ℝ) → ℝ :=
      fun O x => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-(x ⬝ᵥ (singleBlockPrecision κ O *ᵥ x)) / 2)
    (∀ x : Fin n → ℝ, Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O x) (orthogonalHaar n)) ∧
    ∀ (Q : Matrix.orthogonalGroup (Fin n) ℝ) (x : Fin n → ℝ),
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det *
          p O ((Q : Matrix (Fin n) (Fin n) ℝ) *ᵥ x) ∂orthogonalHaar n) =
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O x ∂orthogonalHaar n) := by
  classical
  let p : Matrix.orthogonalGroup (Fin n) ℝ → (Fin n → ℝ) → ℝ :=
    fun O x => Real.sqrt (singleBlockPrecision κ O).det /
      (2 * Real.pi) ^ ((n : ℝ) / 2) *
        Real.exp (-(x ⬝ᵥ (singleBlockPrecision κ O *ᵥ x)) / 2)
  change (∀ x : Fin n → ℝ, Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O x) (orthogonalHaar n)) ∧ _
  have hAc : Continuous (fun O : Matrix.orthogonalGroup (Fin n) ℝ => singleBlockPrecision κ O) := by
    unfold singleBlockPrecision
    exact continuous_const.sub
      ((continuous_subtype_val.add continuous_subtype_val.matrix_transpose).const_smul ((κ - 1) / 4))
  have hcont (x : Fin n → ℝ) : Continuous (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O x) := by
    dsimp only [p]
    fun_prop
  have hL1 (x : Fin n → ℝ) : Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O x) (orthogonalHaar n) := by
    let := (orthogonalHaar_spec n).1
    exact (hcont x).integrable_of_hasCompactSupport (isClosed_tsupport _).isCompact
  refine ⟨hL1, ?_⟩
  intro Q x
  have hcov (O : Matrix.orthogonalGroup (Fin n) ℝ) :
      ((Q * O * Q⁻¹ : Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ).det *
        p (Q * O * Q⁻¹) ((Q : Matrix (Fin n) (Fin n) ℝ) *ᵥ x) =
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O x := by
    obtain ⟨_, hd, hA, hquad⟩ := conjugation_algebra κ Q O
    dsimp only [p]
    rw [hd, hA, hquad]
  have hemb : MeasurableEmbedding (fun O : Matrix.orthogonalGroup (Fin n) ℝ => Q * O * Q⁻¹) :=
    ((Homeomorph.mulLeft Q).trans (Homeomorph.mulRight Q⁻¹)).measurableEmbedding
  calc
    _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        ((Q * O * Q⁻¹ : Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ).det *
          p (Q * O * Q⁻¹) ((Q : Matrix (Fin n) (Fin n) ℝ) *ᵥ x) ∂orthogonalHaar n := by
      have hmp : MeasurePreserving
          (fun O : Matrix.orthogonalGroup (Fin n) ℝ => Q * O * Q⁻¹)
          (orthogonalHaar n) (orthogonalHaar n) :=
        ⟨hemb.measurable, haar_conjugation Q⟩
      exact (hmp.integral_comp hemb (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
        (O : Matrix (Fin n) (Fin n) ℝ).det *
          p O ((Q : Matrix (Fin n) (Fin n) ℝ) *ᵥ x))).symm
    _ = _ := by apply integral_congr_ae; exact Filter.Eventually.of_forall hcov

end AutoSamplingTheory.ExampleCases.GaussianComplexity.KernelRotation

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
AppendixB2 standing n>=3,kappa>=4; full Haar O(n), every Q and x. p4.1 uses the Gaussian density p_O and its conjugation covariance.Same standing range and full Haar; the real formula p_O is explicit. Fixed-x Haar L1 and covariance/measure preservation are internal outputs. Identification with a Gaussian probability density remains a separate excluded source obligation.sameThe binding is scoped solely to the fixed-Q calculation on the literal formula. No Gaussian law is chosen, no extra premise is added, and no claim of full Ex58/norm-axis/Fubini completion is made.

Only fixed-Q invariance of the signed Haar average of the literal Gaussian formula. Identifying that formula with the actual N(0,A_O^-1) density, probability normalization/covariance, orthogonal transitivity and the full x -> ||x||e1 statement Ex58, joint spatial/Haar integrability and Fubini, original H(lambda) identification, sphere/Poisson evaluation, TV/amplification/transcript/eigenbasis and both main lower bounds remain open. The source uses the Gaussian density notation; the present scoped statement makes the formula explicit and retains the missing law-identification edge.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • scopes: The pinned source paragraph concerns an actual Gaussian density and proceeds to norm-axis Ex58; this publication expressly isolates the literal-formula fixed-Q average step. Acceptance does not discharge density identification, transitivity, spatial Fubini, H(λ), or separation bounds. — Raw A2.SS2.p2; A2.SS2.SSS2.p4.1/Ex58, p4.2/Ex59 and p4.3/Ex60; packet original_text and candidate lesson scope statements; no such stronger conclusion appears in the public signature.
  • assumptions: The fixed-Q literal-formula proof uses less than the retained source standing bounds, which remain exactly n≥3 and κ≥4. This is not an added premise or a claim of a stronger published theorem. — Raw A2.SS2.p2 and public _hn/_hκ binders agree; the two private providers and continuity/compactness proof do not consume those bounds.

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 fixed-Q invariance of the signed Haar average of the literal Gaussian formula. Identifying that formula with the actual N(0,A_O^-1) density, probability normalization/covariance, orthogonal transitivity and the full x → ||x||e1 statement Ex58, joint spatial/Haar integrability and Fubini, original H(lambda) identification, sphere/Poisson evaluation, TV/amplification/transcript/eigenbasis and both main lower bounds remain open. The source uses the Gaussian density notation; the present scoped statement makes the formula explicit and retains the missing law-identification edge.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Matrix.det_mul
  • Matrix.det_transpose
  • Matrix.transpose_mul
  • Matrix.mulVec_mulVec
  • Matrix.dotProduct_transpose_mulVec
  • Measure.isHaarMeasure_map_mul_right
  • Measure.isProbabilityMeasure_map
  • Measure.map_map
  • Continuous.integrable_of_hasCompactSupport
  • MeasurePreserving.integral_comp
  • integral_congr_ae

Mathematical sources

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

Which proof obligations and prerequisites are covered?

  • TODO — not closed by these contributions Finite signed full-Haar formula average invariant under every fixed orthogonal action