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

MixtureFubini: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Compute the literal mixture transform by genuine joint Fubini
Samplinglib mathematical lesson

Compute the literal mixture transform by genuine joint Fubini

AutoSamplingTheory.ExampleCases.GaussianComplexity.MixtureFubini.literal_mixture_transform · theorem · Teaching coverage

Read this first

Mathematical statement

Let n≥3, kappa≥4 and ell≥0. On full real O(n), use the existing normalized Borel Haar probability mu; on Euclidean real n-space use its actual norm and volume. Let A_O be the literal Eq4 precision and p_O(x)=sqrt(det A_O)/(2pi)^(n/2) exp(-x^T A_O x/2), with real n/2. Put U=O_11 and a(O)=kappa+1+4ell-(kappa-1)U. Both joint functions f(O,x)=det(O)exp(-ell||x||_2^2)p_O(x) and g(O,x)=det(O)sqrt(det A_O)/(2pi)^(n/2) exp(-a(O)||x||_2^2/4) are absolutely Bochner L1 under mu times Euclidean volume. Moreover the literal nested transform E[det(O) integral exp(-ell||x||_2^2)p_O(x) dx] equals (-1)^(n-1)(sqrt(kappa)-1)^(n-1)/2^(n/2) times E[((sqrt(kappa)+1)U-(sqrt(kappa)-1))/a(O)^(n/2)]. This includes ell=0. It is an equality for explicit real formulas, without identifying p with an actual Gaussian density or the transform with target-mixture expectations.

\[H_{\mathrm{lit}}(\ell)=\mathbb E\!\left[\det(O)\int e^{-\ell\|x\|_2^2}p_O(x)\,dx\right]=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^{n/2}}\mathbb E\!\left[\frac{(\sqrt\kappa+1)U-(\sqrt\kappa-1)}{[\kappa+1+4\ell-(\kappa-1)U]^{n/2}}\right]\]
Lean statement · literal_mixture_transform

Literal local p/f/g, exact Euclidean norm and product measure; both joint L1 conclusions and literal transform equality with realn/2.

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

Exact module and namespace context

Proof roadmap

  1. 1Dominate the original joint integrand

    The existing exact precision theorem gives x^T A_O x≥||x||_2^2. Since ell≥0, adding the test exponent only increases decay. The determinant-normalization prefactor is continuous on compact full O(n), so its absolute value has a finite bound C. Thus the original joint integrand is bounded in absolute value by C exp(-||x||_2^2/2). This C is sufficient and is not claimed to equal the sharp source Ex59 prefactor.

  2. 2Dominate the radial joint integrand too

    Orthogonality bounds U≤1, hence a(O)≥2+4ell≥2. The radial exponent is bounded by -||x||_2^2/2, with the identical prefactor. The same genuine integrable majorant works on Haar times volume, including ell=0. Continuity supplies joint measurability, while the canonical Haar specification supplies probability.

  3. 3Perform the first legitimate Fubini swap

    Pull the determinant into each spatial integral and apply Fubini using the proved original joint L1. The original nested transform becomes a spatial integral of signed Haar averages. This step is an equality of actual finite integrals, rather than an identity between default nonintegrable Bochner values.

  4. 4Consume the identical norm-axis theorem inside the test

    For each fixed Euclidean x, the already compiled norm-axis theorem equates the signed original average with its exact O11 radial formula. The test exp(-ell||x||_2^2) is constant in O. Multiplying that equality by the test and combining exponents identifies the two Haar inner integrals. This is equality after averaging; the original and radial integrands need not agree pointwise in O.

  5. 5Use radial joint L1 for the second swap

    Apply Fubini in the reverse direction to the radial joint integrand. Pull the unchanged normalizer and determinant factors outside the spatial integral. This yields precisely the iterated expression already evaluated in the existing radial-integral theorem.

  6. 6Reuse the evaluated Gaussian and B6 node

    The canonical radial-integral theorem already evaluates the Gaussian spatial integral and applies actual determinant cancellation B6 with its genuine integrable weight. Apply that identical declaration, with unchanged U, a, dimension, condition number and test parameter. Its conclusion is exactly the displayed scalar expectation and sign coefficient.

Full assumptions and notation

All objects and hypotheses

  • Standing n≥3 and kappa≥4, and source ell≥0 including zero. All dimension-half powers use real division.
  • The same actual canonical normalized full O(n) Haar law is used, with both determinant signs, and the spatial measure is actual Euclidean volume. WithLp.ofLp supplies coordinates without replacing the Euclidean norm.
  • Original and radial joint absolute L1 are theorem conclusions. Spectral lower bounds, Haar probability, compact prefactor bounds, Gaussian decay integrability and both Fubini swaps are supplied internally. No L1, domination, density-identification or Fubini premise is added.
  • Source Ex59 has explicit sharp prefactor (kappa/(2pi))^(n/2). This proof uses a sufficient finite compact prefactor depending on n and kappa. It proves the same exact integration identity, without separately claiming the sharp Ex59 estimate.

Mathematical proof

1. Dominate the original joint integrand

The existing exact precision theorem gives x^T A_O x≥||x||_2^2. Since ell≥0, adding the test exponent only increases decay. The determinant-normalization prefactor is continuous on compact full O(n), so its absolute value has a finite bound C. Thus the original joint integrand is bounded in absolute value by C exp(-||x||_2^2/2). This C is sufficient and is not claimed to equal the sharp source Ex59 prefactor.

\[x^\top A_Ox\geq\|x\|_2^2,\qquad |f(O,x)|\leq C e^{-\|x\|_2^2/2}\]
Corresponding Lean step

hq consumes the exact singleBlockPrecision_regular and identifies coordinate dotProduct with true Euclidean squared norm. hk and private joint_integrable produce the compact bound and actual product L1 using GaussianFourier integrability.

2. Dominate the radial joint integrand too

Orthogonality bounds U≤1, hence a(O)≥2+4ell≥2. The radial exponent is bounded by -||x||_2^2/2, with the identical prefactor. The same genuine integrable majorant works on Haar times volume, including ell=0. Continuity supplies joint measurability, while the canonical Haar specification supplies probability.

\[a(O)\geq 2+4\ell\geq2,\qquad |g(O,x)|\leq C e^{-\|x\|_2^2/2}\]
Corresponding Lean step

ha uses entry_norm_bound_of_unitary. The private product provider combines compact continuity with actual Haar probability and GaussianFourier decay; hf and hg are genuine joint Integrable proofs.

3. Perform the first legitimate Fubini swap

Pull the determinant into each spatial integral and apply Fubini using the proved original joint L1. The original nested transform becomes a spatial integral of signed Haar averages. This step is an equality of actual finite integrals, rather than an identity between default nonintegrable Bochner values.

\[H_{\mathrm{lit}}(\ell)=\int\!\left[\int f(O,x)\,d\mu(O)\right]dx\]
Corresponding Lean step

The main calc uses integral_const_mul and integral_integral_swap hf. No spatial integrability hypothesis is supplied by the caller.

4. Consume the identical norm-axis theorem inside the test

For each fixed Euclidean x, the already compiled norm-axis theorem equates the signed original average with its exact O11 radial formula. The test exp(-ell||x||_2^2) is constant in O. Multiplying that equality by the test and combining exponents identifies the two Haar inner integrals. This is equality after averaging; the original and radial integrands need not agree pointwise in O.

\[\int f(O,x)\,d\mu(O)=e^{-\ell\|x\|_2^2}\mathbb E[\det(O)p_O(x)]=\int g(O,x)\,d\mu(O)\]
Corresponding Lean step

haxis directly calls canonical signed_kernel_radial. hgr proves exact exponent addition; havg pulls the test through the Haar integral and consumes haxis. There is no asserted pointwise f=g.

5. Use radial joint L1 for the second swap

Apply Fubini in the reverse direction to the radial joint integrand. Pull the unchanged normalizer and determinant factors outside the spatial integral. This yields precisely the iterated expression already evaluated in the existing radial-integral theorem.

\[H_{\mathrm{lit}}(\ell)=\frac{1}{(2\pi)^{n/2}}\mathbb E\!\left[\det(O)\sqrt{\det A_O}\int e^{-a(O)\|x\|_2^2/4}\,dx\right]\]
Corresponding Lean step

The calc uses (integral_integral_swap hg).symm, integral_const_mul and integral_div. Both swaps have their own proved joint L1 provider, on the same actual measures.

6. Reuse the evaluated Gaussian and B6 node

The canonical radial-integral theorem already evaluates the Gaussian spatial integral and applies actual determinant cancellation B6 with its genuine integrable weight. Apply that identical declaration, with unchanged U, a, dimension, condition number and test parameter. Its conclusion is exactly the displayed scalar expectation and sign coefficient.

\[\frac{\mathbb E[\det(O)\sqrt{\det A_O}\int e^{-a(O)\|x\|_2^2/4}dx]}{(2\pi)^{n/2}}=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^{n/2}}\mathbb E\!\left[\frac{(\sqrt\kappa+1)U-(\sqrt\kappa-1)}{a(O)^{n/2}}\right]\]
Corresponding Lean step

heval is the exact equality projection of radialized_test_integral hn hκ hℓ. The existing Gaussian/B6 proof is consumed without a copied route, new premise or inference about actual Gaussian-mixture laws.

Lean verification

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

Lean proof · literal_mixture_transform

Two reachable private providers establish Gaussian decay and uniform compact-prefactor joint L1; the main theorem consumes exact regularity, norm-axis and radial/B6 nodes with two legitimate Fubini swaps.

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 literal_mixture_transform {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) :
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
    let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
    let p : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
      fun O x => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-((WithLp.ofLp x) ⬝ᵥ
            (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2)
    let f : (Matrix.orthogonalGroup (Fin n) ℝ × EuclideanSpace ℝ (Fin n)) → ℝ :=
      fun z => (z.1 : Matrix (Fin n) (Fin n) ℝ).det *
        (Real.exp (-ℓ * ‖z.2‖ ^ 2) * p z.1 z.2)
    let g : (Matrix.orthogonalGroup (Fin n) ℝ × EuclideanSpace ℝ (Fin n)) → ℝ :=
      fun z => (z.1 : Matrix (Fin n) (Fin n) ℝ).det *
        Real.sqrt (singleBlockPrecision κ z.1).det /
          (2 * Real.pi) ^ ((n : ℝ) / 2) * Real.exp (-a z.1 * ‖z.2‖ ^ 2 / 4)
    Integrable f ((orthogonalHaar n).prod volume) ∧
    Integrable g ((orthogonalHaar n).prod volume) ∧
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det *
        (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-ℓ * ‖x‖ ^ 2) * p O x)
        ∂orthogonalHaar n) =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) /
        (2 : ℝ) ^ ((n : ℝ) / 2)) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)) /
            (a O) ^ ((n : ℝ) / 2) ∂orthogonalHaar n) := by
  classical
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
  let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
  let p : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
    fun O x => Real.sqrt (singleBlockPrecision κ O).det /
      (2 * Real.pi) ^ ((n : ℝ) / 2) *
        Real.exp (-((WithLp.ofLp x) ⬝ᵥ
          (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2)
  let f : (Matrix.orthogonalGroup (Fin n) ℝ × EuclideanSpace ℝ (Fin n)) → ℝ :=
    fun z => (z.1 : Matrix (Fin n) (Fin n) ℝ).det *
      (Real.exp (-ℓ * ‖z.2‖ ^ 2) * p z.1 z.2)
  let g : (Matrix.orthogonalGroup (Fin n) ℝ × EuclideanSpace ℝ (Fin n)) → ℝ :=
    fun z => (z.1 : Matrix (Fin n) (Fin n) ℝ).det *
      Real.sqrt (singleBlockPrecision κ z.1).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) * Real.exp (-a z.1 * ‖z.2‖ ^ 2 / 4)
  let q (O : Matrix.orthogonalGroup (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) :=
    (WithLp.ofLp x) ⬝ᵥ (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)
  let k (O : Matrix.orthogonalGroup (Fin n) ℝ) :=
    (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det /
      (2 * Real.pi) ^ ((n : ℝ) / 2)
  let r (O : Matrix.orthogonalGroup (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) :=
    Real.sqrt (singleBlockPrecision κ O).det / (2 * Real.pi) ^ ((n : ℝ) / 2) *
      Real.exp (-(κ + 1 - (κ - 1) * U O) * ‖x‖ ^ 2 / 4)
  change Integrable f ((orthogonalHaar n).prod volume) ∧
    Integrable g ((orthogonalHaar n).prod volume) ∧ _
  let := (orthogonalHaar_spec n).1
  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 hk : Continuous k := by dsimp only [k]; fun_prop
  have hUc : Continuous U := continuous_subtype_val.matrix_elem j0 j0
  have hac : Continuous a := by dsimp only [a]; fun_prop
  have hqc : Continuous (fun z : Matrix.orthogonalGroup (Fin n) ℝ × EuclideanSpace ℝ (Fin n) =>
      q z.1 z.2) := by dsimp only [q]; fun_prop
  have hq (O : Matrix.orthogonalGroup (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) :
      ‖x‖ ^ 2 ≤ q O x := by
    have h := ((singleBlockPrecision_regular hn hκ O).2 (WithLp.ofLp x)).1
    have he : (WithLp.ofLp x) ⬝ᵥ WithLp.ofLp x = ‖x‖ ^ 2 := by
      rw [EuclideanSpace.real_norm_sq_eq]
      simp only [dotProduct, pow_two]
    simpa only [he] using h
  have ha (O : Matrix.orthogonalGroup (Fin n) ℝ) : 2 ≤ a O := by
    have hu : U O ≤ 1 := le_trans (le_abs_self _) (by
      simpa only [U, Real.norm_eq_abs] using entry_norm_bound_of_unitary O.property j0 j0)
    have hm := mul_le_mul_of_nonneg_left hu (show 0 ≤ κ - 1 by linarith)
    dsimp only [a]
    linarith
  have hf : Integrable f ((orthogonalHaar n).prod volume) := by
    have hi := joint_integrable k (fun z => -ℓ * ‖z.2‖ ^ 2 + -(q z.1 z.2) / 2) hk
      (by fun_prop) (fun z => by
        have h1 := hq z.1 z.2
        have h2 := mul_nonneg hℓ (sq_nonneg ‖z.2‖)
        linarith)
    convert hi using 1
    funext z
    dsimp only [f, p, k, q]
    rw [Real.exp_add]
    ring
  have hg : Integrable g ((orthogonalHaar n).prod volume) := by
    have hi := joint_integrable k (fun z => -a z.1 * ‖z.2‖ ^ 2 / 4) hk
      (by fun_prop) (fun z => by
        have hm := mul_le_mul_of_nonneg_right (ha z.1) (sq_nonneg ‖z.2‖)
        nlinarith)
    exact hi
  refine ⟨hf, hg, ?_⟩
  have haxis (x : EuclideanSpace ℝ (Fin n)) :
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * p O x ∂orthogonalHaar n) =
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * r O x ∂orthogonalHaar n) :=
    (signed_kernel_radial hn hκ x).2.2
  have hgr (O : Matrix.orthogonalGroup (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) :
      g (O, x) = Real.exp (-ℓ * ‖x‖ ^ 2) *
        ((O : Matrix (Fin n) (Fin n) ℝ).det * r O x) := by
    dsimp only [g, r, a]
    rw [show Real.exp (-ℓ * ‖x‖ ^ 2) *
        ((O : Matrix (Fin n) (Fin n) ℝ).det *
          (Real.sqrt (singleBlockPrecision κ O).det / (2 * Real.pi) ^ ((n : ℝ) / 2) *
            Real.exp (-(κ + 1 - (κ - 1) * U O) * ‖x‖ ^ 2 / 4))) =
      ((O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2)) *
          (Real.exp (-ℓ * ‖x‖ ^ 2) * Real.exp (-(κ + 1 - (κ - 1) * U O) * ‖x‖ ^ 2 / 4)) by ring]
    rw [← Real.exp_add]
    congr 1
    congr 1
    ring
  have havg (x : EuclideanSpace ℝ (Fin n)) :
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, f (O, x) ∂orthogonalHaar n) =
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, g (O, x) ∂orthogonalHaar n) := by
    calc
      _ = Real.exp (-ℓ * ‖x‖ ^ 2) *
          (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
            (O : Matrix (Fin n) (Fin n) ℝ).det * p O x ∂orthogonalHaar n) := by
        rw [← integral_const_mul]
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun O => by dsimp only [f]; ring
      _ = Real.exp (-ℓ * ‖x‖ ^ 2) *
          (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
            (O : Matrix (Fin n) (Fin n) ℝ).det * r O x ∂orthogonalHaar n) := by rw [haxis]
      _ = _ := by
        rw [← integral_const_mul]
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun O => (hgr O x).symm
  have heval := (radialized_test_integral hn hκ hℓ).2.2.2
  calc
    _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (∫ x : EuclideanSpace ℝ (Fin n), f (O, x)) ∂orthogonalHaar n := by
      apply integral_congr_ae
      exact Filter.Eventually.of_forall fun O => (integral_const_mul _ _).symm
    _ = ∫ x : EuclideanSpace ℝ (Fin n),
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, f (O, x) ∂orthogonalHaar n) :=
      integral_integral_swap hf
    _ = ∫ x : EuclideanSpace ℝ (Fin n),
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, g (O, x) ∂orthogonalHaar n) := by
      apply integral_congr_ae
      exact Filter.Eventually.of_forall havg
    _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (∫ x : EuclideanSpace ℝ (Fin n), g (O, x)) ∂orthogonalHaar n :=
      (integral_integral_swap hg).symm
    _ = (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
          (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-a O * ‖x‖ ^ 2 / 4))
          ∂orthogonalHaar n) / (2 * Real.pi) ^ ((n : ℝ) / 2) := by
      simp only [g, integral_const_mul]
      rw [← integral_div]
      apply integral_congr_ae
      exact Filter.Eventually.of_forall fun O => by ring
    _ = _ := heval

end AutoSamplingTheory.ExampleCases.GaussianComplexity.MixtureFubini

Exact module and namespace context

Scope and omitted-condition boundaries
  • Joint original/radial Haar-spatial L1 and the literal H integral through Eq21 are proved. Actual Gaussian law/density identification, normalization/covariance of that law and resulting target-mixture/TV meanings remain open. The sharp Ex59 constant remains source-only; a finite compact prefactor suffices here. Sphere/Poisson, parameter choice, TV/separation/amplification/transcript/eigenbasis and both main lower bounds remain open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • GaussianFourier.integrable_cexp_neg_mul_sq_norm_add
  • IsCompact.exists_bound_of_continuousOn
  • Integrable.mul_prod
  • Integrable.mono'
  • integral_integral_swap
  • integral_const_mul
  • integral_div
  • entry_norm_bound_of_unitary
  • EuclideanSpace.real_norm_sq_eq

Mathematical sources

  • H definition through Eq21 — Literal formula joint integrability and Fubini composition only; actual Gaussian-law/mixture/TV interpretation 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.