Samplinglib mathematical lesson

Reduce the signed Gaussian formula to the norm axis

AutoSamplingTheory.ExampleCases.GaussianComplexity.KernelAxis.signed_kernel_radial · theorem · Teaching coverage

Read this first

Mathematical statement

Let n≥3 and kappa≥4, let O have the existing normalized Borel Haar probability on full real O(n), and let A_O be the exact equation4 precision. Define the literal function p_O(v)=sqrt(det A_O)/(2pi)^(n/2) exp(-v^T A_O v/2), with a real dimension-half exponent. For every x in Euclidean real n-space, put U=O_11 and r_O(x)=sqrt(det A_O)/(2pi)^(n/2) exp(-(kappa+1-(kappa-1)U)||x||_2^2/4). Both O → det(O)p_O(x) and O → det(O)r_O(x) are absolutely integrable under that Haar probability, and their expectations are equal. All vectors, including zero and vectors already on the norm axis, are included. The claim is for these explicit functions; it does not identify p with a Gaussian probability density.

\[\mathbb E[\det(O)p_O(x)]=\mathbb E\!\left[\det(O)\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}\exp\!\left(-\frac{[\kappa+1-(\kappa-1)U]\|x\|_2^2}{4}\right)\right],\qquad U=O_{11}\]

Lean statement · signed_kernel_radial

Literal p and r local lets, actual Euclidean norm and coordinates; every vector and both Haar L1 conclusions are explicit.

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_radial {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) :
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let p : Matrix.orthogonalGroup (Fin n) ℝ → (Fin n → ℝ) → ℝ :=
      fun O v => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-(v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v)) / 2)
    let r : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
      fun O x => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-(κ + 1 - (κ - 1) * (O : Matrix (Fin n) (Fin n) ℝ) j0 j0) *
            ‖x‖ ^ 2 / 4)
    ∀ x : EuclideanSpace ℝ (Fin n),
      Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O (WithLp.ofLp x)) (orthogonalHaar n) ∧
      Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
        (O : Matrix (Fin n) (Fin n) ℝ).det * r O x) (orthogonalHaar n) ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O (WithLp.ofLp x) ∂orthogonalHaar n) =
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * r O x ∂orthogonalHaar n)

Exact module and namespace context

Proof roadmap

1Choose the true Euclidean norm-axis point
For any Euclidean x, take y=||x||_2 e1. Its Euclidean norm is ||x||_2 because that scalar is nonnegative. This holds also at zero and when x already equals y. Coordinates of y are exactly the single-coordinate vector with entry ||x||_2.
2Produce the orthogonal map internally
Equal-norm vectors are related by the reflection in the orthogonal complement of span(x-y). The existing canonical reflection theorem sends x to y uniformly, including x=y and x=y=0. The source uses transitivity implicitly; this is its explicit standard-background implementation.
3Connect the isometry to the actual matrix action
Use the canonical Euclidean orthonormal basis to represent that isometry as a matrix Q. The canonical isometry-to-matrix theorem proves Q belongs to full O(n), and the matrix-coordinate evaluation theorem gives Q times the coordinate vector of x equal to the coordinates of y. This is a proved adapter, not a changed action.
4Consume the identical fixed-Q Haar theorem
Apply the previously compiled rotation/reflection-invariance theorem to this produced Q and the coordinates of x. Its actual matrix action is y, so the signed average at x equals the signed average at the norm-axis point. The same full Haar law and precision are used.
5Evaluate the axis quadratic form exactly
For a single-coordinate vector t e1, the quadratic form is t^2 times the first diagonal entry of the literal precision. That diagonal entry is (kappa+1-(kappa-1)U)/2. The extra factor1/2 in the Gaussian exponent produces exactly the denominator4. The square-root determinant and real normalization power are unchanged.
6Retain genuine finiteness on both sides
The existing fixed-Q theorem already proves Haar L1 for every fixed coordinate vector. Apply it to x and to the produced y. Pointwise equality p_O(y)=r_O(x) transfers L1 to the displayed reduced formula, then integral equality follows. This concerns one fixed x at a time and exchanges no spatial integrals.

Full assumptions and notation

All objects and hypotheses

AppendixB2 standing n≥3 and kappa≥4 are retained. Every x belongs to the actual EuclideanSpace R (Fin n); its norm is the Euclidean norm, never the coordinate sup norm.
The law is the same actual canonical normalized full-O(n) Borel Haar probability, allowing reflections and both determinant signs. The matrix A_O is the unchanged literal source precision.
WithLp.ofLp converts a Euclidean vector to its real coordinates for dotProduct and mulVec. Source coordinate1 is the zero-based j0, whose validity follows from n≥3.
Both Haar L1 assertions are outputs. No orthogonal witness, equal-norm premise, covariance identity, integrability assumption, Gaussian density identification or spatial Fubini assumption is supplied by the caller. All dimension-half powers are real.

Mathematical proof

1. Choose the true Euclidean norm-axis point

For any Euclidean x, take y=||x||_2 e1. Its Euclidean norm is ||x||_2 because that scalar is nonnegative. This holds also at zero and when x already equals y. Coordinates of y are exactly the single-coordinate vector with entry ||x||_2.

\[y=\|x\|_2e_1,\qquad\|y\|_2=\|x\|_2\]

Corresponding Lean step

The public proof uses PiLp.single 2 j0 and PiLp.norm_single. hy identifies its WithLp.ofLp coordinates with Pi.single. No sup-norm substitution or division by ||x|| occurs.

2. Produce the orthogonal map internally

Equal-norm vectors are related by the reflection in the orthogonal complement of span(x-y). The existing canonical reflection theorem sends x to y uniformly, including x=y and x=y=0. The source uses transitivity implicitly; this is its explicit standard-background implementation.

\[F=\operatorname{reflection}_{\operatorname{span}(x-y)^\perp},\qquad Fx=y\]

Corresponding Lean step

Private exists_orthogonal_map calls the actual Submodule.reflection_sub. The reflection is a real linear isometry equivalence, with no new public witness or regularity assumption.

3. Connect the isometry to the actual matrix action

Use the canonical Euclidean orthonormal basis to represent that isometry as a matrix Q. The canonical isometry-to-matrix theorem proves Q belongs to full O(n), and the matrix-coordinate evaluation theorem gives Q times the coordinate vector of x equal to the coordinates of y. This is a proved adapter, not a changed action.

\[Q\in O(n),\qquad Q\,\operatorname{coord}(x)=\operatorname{coord}(y)\]

Corresponding Lean step

The same private provider calls LinearIsometryEquiv.toMatrix_mem_unitaryGroup and LinearMap.toMatrix_mulVec_repr in EuclideanSpace.basisFun. Its witness is an actual orthogonal matrix.

4. Consume the identical fixed-Q Haar theorem

Apply the previously compiled rotation/reflection-invariance theorem to this produced Q and the coordinates of x. Its actual matrix action is y, so the signed average at x equals the signed average at the norm-axis point. The same full Haar law and precision are used.

\[\mathbb E[\det(O)p_O(x)]=\mathbb E[\det(O)p_O(Qx)]=\mathbb E[\det(O)p_O(\|x\|_2e_1)]\]

Corresponding Lean step

The public proof genuinely calls signed_kernel_rotation_invariant once, rewrites with the produced coordinate identity hQ, and reverses its equality. This is a real consumer of the unchanged canonical declaration.

5. Evaluate the axis quadratic form exactly

For a single-coordinate vector t e1, the quadratic form is t^2 times the first diagonal entry of the literal precision. That diagonal entry is (kappa+1-(kappa-1)U)/2. The extra factor1/2 in the Gaussian exponent produces exactly the denominator4. The square-root determinant and real normalization power are unchanged.

\[(te_1)^\top A_O(te_1)=\frac{[\kappa+1-(\kappa-1)U]t^2}{2},\qquad p_O(\|x\|_2e_1)=r_O(x)\]

Corresponding Lean step

Private axis_quadratic uses single_dotProduct, dotProduct_single and the literal singleBlockPrecision entry. The public hr identity substitutes t=||x|| and proves the exact exponent arithmetic.

6. Retain genuine finiteness on both sides

The existing fixed-Q theorem already proves Haar L1 for every fixed coordinate vector. Apply it to x and to the produced y. Pointwise equality p_O(y)=r_O(x) transfers L1 to the displayed reduced formula, then integral equality follows. This concerns one fixed x at a time and exchanges no spatial integrals.

\[\det(O)p_O(x),\ \det(O)r_O(x)\in L^1(\mu_n),\qquad\mathbb E[\det(O)p_O(x)]=\mathbb E[\det(O)r_O(x)]\]

Corresponding Lean step

h.1 supplies both genuine L1 providers; Integrable.congr and integral_congr_ae use the actual hr identity. The two L1 conclusions accompany the final equality; original Gaussian-law/Fubini obligations are excluded.

Lean verification

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

Lean proof · signed_kernel_radial

Two reachable private providers produce the orthogonal coordinate witness and exact axis quadratic evaluation. The public proof consumes the existing fixed-Q invariant/L1 theorem and discharges the full literal norm-axis identity.

Download module (.lean)

theorem signed_kernel_radial {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) :
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let p : Matrix.orthogonalGroup (Fin n) ℝ → (Fin n → ℝ) → ℝ :=
      fun O v => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-(v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v)) / 2)
    let r : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
      fun O x => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-(κ + 1 - (κ - 1) * (O : Matrix (Fin n) (Fin n) ℝ) j0 j0) *
            ‖x‖ ^ 2 / 4)
    ∀ x : EuclideanSpace ℝ (Fin n),
      Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O (WithLp.ofLp x)) (orthogonalHaar n) ∧
      Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
        (O : Matrix (Fin n) (Fin n) ℝ).det * r O x) (orthogonalHaar n) ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O (WithLp.ofLp x) ∂orthogonalHaar n) =
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * r O x ∂orthogonalHaar n) := by
  classical
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  let p : Matrix.orthogonalGroup (Fin n) ℝ → (Fin n → ℝ) → ℝ :=
    fun O v => Real.sqrt (singleBlockPrecision κ O).det /
      (2 * Real.pi) ^ ((n : ℝ) / 2) *
        Real.exp (-(v ⬝ᵥ (singleBlockPrecision κ O *ᵥ v)) / 2)
  let r : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
    fun O x => Real.sqrt (singleBlockPrecision κ O).det /
      (2 * Real.pi) ^ ((n : ℝ) / 2) *
        Real.exp (-(κ + 1 - (κ - 1) * (O : Matrix (Fin n) (Fin n) ℝ) j0 j0) *
          ‖x‖ ^ 2 / 4)
  change ∀ x : EuclideanSpace ℝ (Fin n),
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O (WithLp.ofLp x)) (orthogonalHaar n) ∧
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * r O x) (orthogonalHaar n) ∧ _
  intro x
  let y : EuclideanSpace ℝ (Fin n) := PiLp.single 2 j0 ‖x‖
  have hnorm : ‖x‖ = ‖y‖ := by simp [y, PiLp.norm_single]
  obtain ⟨Q, hQ⟩ := exists_orthogonal_map x y hnorm
  have hy : WithLp.ofLp y = Pi.single j0 ‖x‖ := rfl
  have hr (O : Matrix.orthogonalGroup (Fin n) ℝ) : p O (WithLp.ofLp y) = r O x := by
    dsimp only [p, r]
    rw [hy, axis_quadratic]
    congr 2
    ring
  have h := signed_kernel_rotation_invariant hn hκ
  change (∀ v : Fin n → ℝ, Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * p O v) (orthogonalHaar n)) ∧ _ at h
  have hrad : Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * r O x) (orthogonalHaar n) :=
    (h.1 (WithLp.ofLp y)).congr (Filter.Eventually.of_forall fun O =>
      congrArg (fun z : ℝ => (O : Matrix (Fin n) (Fin n) ℝ).det * z) (hr O))
  refine ⟨h.1 (WithLp.ofLp x), hrad, ?_⟩
  have he := h.2 Q (WithLp.ofLp x)
  rw [hQ] at he
  calc
    _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O (WithLp.ofLp y) ∂orthogonalHaar n := he.symm
    _ = _ := by
      apply integral_congr_ae
      exact Filter.Eventually.of_forall fun O =>
        congrArg (fun z : ℝ => (O : Matrix (Fin n) (Fin n) ℝ).det * z) (hr O)

end AutoSamplingTheory.ExampleCases.GaussianComplexity.KernelAxis

Exact module and namespace context

Scope and omitted-condition boundaries

The literal-function Ex58 norm-axis average and its following O11 exponent are proved, including both fixed-vector Haar L1 outputs. Actual N(0,A_O^-1) law/density identification, probability normalization/covariance, joint spatial/Haar domination and Fubini, original H(lambda) identification, Ex59 sharp domination, sphere/Poisson, TV/amplification/transcript/eigenbasis and both main lower bounds remain open. No Gaussian probability measure is defined by the local formulas.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Submodule.reflection_sub
LinearIsometryEquiv.toMatrix_mem_unitaryGroup
LinearMap.toMatrix_mulVec_repr
EuclideanSpace.basisFun
PiLp.norm_single
single_dotProduct
dotProduct_single
Integrable.congr
integral_congr_ae

Mathematical sources

Ex58 and exact axis exponent — Literal-function norm-axis Haar average and O11 evaluation; actual Gaussian law/density and spatial Fubini are separate.

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