Compute the literal mixture transform by genuine joint Fubini
AutoSamplingTheory.ExampleCases.GaussianComplexity.MixtureFubini.literal_mixture_transform · theorem · Teaching coverage
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.
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.
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)Proof roadmap
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
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.
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.
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.
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.
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.
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.
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.MixtureFubiniSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Standing n>=3,kappa>=4, ell>=0, full Haar O(n), Euclidean volume and source Ex58/Ex59/Fubini/Gaussian/B6 calculation. | Same range and measures, no caller joint L1/majorant premise. Explicit literal-formula transform only. Finite compact prefactor supplies sufficient domination rather than separately proving sharp Ex59 constant. | same | The exact scalar identity is unchanged for the isolated literal functions. Alternative finite domination proves the required absolute joint L1 without new hypotheses. Actual Gaussian-density and mixture/TV identifications are explicit exclusions, not claimed formalized. |
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.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- assumptions: Uniform finite compact-prefactor domination replaces the numerical Ex59 prefactor for proving the same integrability and integration identity. — Source Ex59 states (kappa/(2pi))^(n/2) exp(-||x||^2/2). Main hk and private joint_integrable instead establish ||k(O)||<=C and C exp(-||x||^2/2), sufficient under Haar probability. Neither theorem nor lesson claims the sharp estimate as a separately formalized conclusion.
- scopes: The reviewed theorem isolates the literal analytic identity from Gaussian-law, target-mixture and TV interpretations in the surrounding paper. — The pinned statement expressly excludes density/law identification. Raw B.2 density wording and Ex57/Eq20 require additional identifications. The current theorem has only explicit functions and ordinary integrals; all six lesson steps respect that boundary.
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
- 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
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecisionAutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_regularAutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.orthogonalHaarAutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.orthogonalHaar_specAutoSamplingTheory.ExampleCases.GaussianComplexity.KernelAxis.signed_kernel_radialAutoSamplingTheory.ExampleCases.GaussianComplexity.RadialIntegral.radialized_test_integral
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.