LF4 general-N DH, Slice D (the crux): the ratio map sends expHalf^{⊗N} to Dirichlet

Category: 3-Local (the ratio map sends expHalf^{⊗N} to Dirichlet).

The general-N analogue of MomentRatioUniform.lean (the qubit's ratioSqNorm_map_expHalf_prod, Beta(1,1)=Uniform[0,1]): the N-fold ratio map R_N(s) = (s_0/∑s, …, s_{N-2}/∑s) pushes expHalf^{⊗N} to the Dirichlet(1,…,1) law, expressed (to dodge the missing Mathlib simplex surface measure) as the constant (N−1)! density on the open simplex in free coordinates ℝ^{N-1}.

This file builds the slice incrementally; see specs/general-n-dh-plan.md Slice D for the full DAG (D.1 radial constant → D.3 the determinant det = S^{N-1} → D.2 diffeo → D.4 inj/image → D.5 assembly).

D.1 (this commit): the radial moment constant. ∫⁻_{S>0} Sⁿ e^{−S/2} = 2^{n+1}·n! — the n-th moment base (n = N−1) that the substituted S-integral collapses to. Generalises lintegral_radial_const (N=2: n=1, ∫ S e^{−S/2} = 4 = 2²·1!).

theorem CSD.LF4.lintegral_radial_moment (n : ℕ) : ∫⁻ (S : ℝ) in Set.Ioi 0, ENNReal.ofReal (S ^ n * Real.exp (-S / 2)) = ENNReal.ofReal (2 ^ (n + 1) * ↑n.factorial)

D.1 (radial moment, general N). ∫⁻_{S>0} Sⁿ·e^{−S/2} dS = 2^{n+1}·n!. The n-th moment of the Exp(1/2) shape; with n = N−1 it is the normalisation the post-substitution S-integral collapses to in the Gamma→Dirichlet change of variables. Routes through integral_rpow_mul_exp_neg_mul_Ioi (a = n+1, r = 1/2, giving 2^{n+1}·Γ(n+1)) + Real.Gamma_nat_eq_factorial + the ofReal↔lintegral bridge, mirroring lintegral_radial_const.

D.3 — the Jacobian determinant det = S^M

The stick-breaking substitution Ψ_N(t, S) = (t_0·S, …, t_{M-1}·S, (1−∑t)·S) on ℝ^M × ℝ (here N = M+1) has Jacobian the bordered matrix psiMat S t: the top-left M×M block is S·I, the last column is (t_0,…,t_{M-1}, 1−∑t), the last row is (−S,…,−S, 1−∑t). Its determinant is S^M, proved by the row operation "add every castSucc row into the last row": the last row becomes (0,…,0,1) because each castSucc-column sums to S + (−S) = 0 and the last column sums to ∑t + (1−∑t) = 1. The result is then block-triangular.

This is the genuine general-N content (no direct Mathlib lemma); see specs/general-n-dh-plan.md Slice D.3.

noncomputable def CSD.LF4.psiMat {M : ℕ} (S : ℝ) (t : Fin M → ℝ) : Matrix (Fin (M + 1)) (Fin (M + 1)) ℝ

The Jacobian matrix of the stick-breaking substitution Ψ_{M+1} at (t, S), indexed by Fin (M+1) (first M directions are the t-coordinates, the last is S). Bordered: S·I block, last column t/1−∑t, last row −S/1−∑t.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.LF4.psiMat_col_sum {M : ℕ} (S : ℝ) (t : Fin M → ℝ) (j : Fin (M + 1)) : ∑ i : Fin (M + 1), psiMat S t i j = if j = Fin.last M then 1 else 0

Column-sum of psiMat: every column sums (over all rows) to [j = last]. On a castSucc column the diagonal S and the last-row −S cancel; on the last column ∑t + (1−∑t) = 1. This is the content of the row operation.

theorem CSD.LF4.psiMat_det {M : ℕ} (S : ℝ) (t : Fin M → ℝ) : (psiMat S t).det = S ^ M

D.3: the Jacobian determinant is S^M. Via the row operation "add every castSucc row into the last row" (det_updateRow_sum, coefficient 1), after which the matrix is two-block-triangular (last row zero off the corner) with diagonal blocks S·I_M and [1].

D.2 — the stick-breaking diffeo Ψ_N and its derivative

Ψ_N : (Fin (M+1) → ℝ) → (Fin (M+1) → ℝ), y ↦ (k ↦ y(castSucc k)·y(last)) on the first M coordinates and (1−∑_k y(castSucc k))·y(last) on the last. On the domain openSimplex ×ˢ Ioi 0 (reading y(last) = S, y(castSucc ·) = t) this is the inverse substitution of the Gamma→Dirichlet change of variables; its Jacobian is psiMat S t (D.3), det S^M.

noncomputable def CSD.LF4.PsiN {M : ℕ} (y : Fin (M + 1) → ℝ) : Fin (M + 1) → ℝ

The stick-breaking substitution map on Fin (M+1) → ℝ.

Equations

• CSD.LF4.PsiN y i = Fin.lastCases ((1 - ∑ k : Fin M, y k.castSucc) * y (Fin.last M)) (fun (k : Fin M) => y k.castSucc * y (Fin.last M)) i

noncomputable def CSD.LF4.psiFDerivN {M : ℕ} (y : Fin (M + 1) → ℝ) : (Fin (M + 1) → ℝ) →L[ℝ] Fin (M + 1) → ℝ

The candidate Fréchet derivative of Ψ_N at y: the linear map of the Jacobian matrix psiMat (y last) (y ∘ castSucc) (D.3).

Equations

• CSD.LF4.psiFDerivN y = LinearMap.toContinuousLinearMap (Matrix.toLin' (CSD.LF4.psiMat (y (Fin.last M)) fun (k : Fin M) => y k.castSucc))

theorem CSD.LF4.psiFDerivN_det {M : ℕ} (y : Fin (M + 1) → ℝ) : (psiFDerivN y).det = y (Fin.last M) ^ M

Jacobian determinant of Ψ_N. det (psiFDerivN y) = (y last)^M. Immediate from psiMat_det (D.3) via LinearMap.det_toLin'.

theorem CSD.LF4.hasFDerivAt_PsiN {M : ℕ} (y : Fin (M + 1) → ℝ) : HasFDerivAt PsiN (psiFDerivN y) y

Ψ_N is Fréchet differentiable everywhere with derivative psiFDerivN. Proved componentwise (hasFDerivAt_pi): each output coordinate is a product/affine polynomial in the y-coordinates; the assembled derivative's matrix is psiMat.

D.4 — injectivity and image of Ψ_N

Ψ_N is a bijection from the domain (open simplex in free coordinates × Ioi 0) onto the open positive quadrant {s | ∀ i, 0 < s i}. The inverse sends s to S := ∑ s, t_k := s(castSucc k)/S.

def CSD.LF4.domainN {M : ℕ} : Set (Fin (M + 1) → ℝ)

The domain of the substitution, in Fin (M+1) → ℝ coordinates: the first M coordinates form the open simplex (t_k > 0, ∑ t < 1), the last is S > 0.

Equations

• CSD.LF4.domainN = {y : Fin (M + 1) → ℝ | (∀ (k : Fin M), 0 < y k.castSucc) ∧ ∑ k : Fin M, y k.castSucc < 1 ∧ 0 < y (Fin.last M)}

def CSD.LF4.posQuadrant {M : ℕ} : Set (Fin (M + 1) → ℝ)

The open positive quadrant in Fin (M+1) → ℝ.

Equations

• CSD.LF4.posQuadrant = {s : Fin (M + 1) → ℝ | ∀ (i : Fin (M + 1)), 0 < s i}

theorem CSD.LF4.measurableSet_domainN {M : ℕ} : MeasurableSet domainN

theorem CSD.LF4.measurableSet_posQuadrant {M : ℕ} : MeasurableSet posQuadrant

theorem CSD.LF4.PsiN_sum {M : ℕ} (y : Fin (M + 1) → ℝ) : ∑ i : Fin (M + 1), PsiN y i = y (Fin.last M)

Total-sum recovery. ∑ i, Ψ_N(y) i = y last = S. The inverse-map crux: (∑_k t_k)·S + (1−∑t)·S = S.

theorem CSD.LF4.injOn_PsiN {M : ℕ} : Set.InjOn PsiN domainN

D.4a: Ψ_N is injective on the domain. From Ψ_N y = Ψ_N y', summing recovers S = S' (PsiN_sum); then each castSucc coordinate cancels S > 0, and the last coordinate is S.

theorem CSD.LF4.image_PsiN {M : ℕ} : PsiN '' domainN = posQuadrant

D.4b: the image of Ψ_N over the domain is the positive quadrant.

D.5c — assembly: the ratio map sends expHalf^{⊗N} to Dirichlet(1,…,1)

The capstone of Slice D, generalising the qubit ratioSqNorm_map_expHalf_prod.

noncomputable def CSD.LF4.ratioN {M : ℕ} (s : Fin (M + 1) → ℝ) : Fin M → ℝ

The free-coordinate ratio map s ↦ (k ↦ s(castSucc k)/∑s).

Equations

• CSD.LF4.ratioN s k = s k.castSucc / ∑ i : Fin (M + 1), s i

def CSD.LF4.openSimplexFree {M : ℕ} : Set (Fin M → ℝ)

The open simplex in free coordinates {t : Fin M → ℝ | (∀ k, 0 < t k) ∧ ∑ t < 1}.

Equations

• CSD.LF4.openSimplexFree = {t : Fin M → ℝ | (∀ (k : Fin M), 0 < t k) ∧ ∑ k : Fin M, t k < 1}

theorem CSD.LF4.measurableSet_openSimplexFree {M : ℕ} : MeasurableSet openSimplexFree

noncomputable def CSD.LF4.dExp (s : ℝ) : ENNReal

The single-coordinate Exp(1/2) density.

Equations

• CSD.LF4.dExp s = ENNReal.ofReal (if 0 < s then 1 / 2 * Real.exp (-s / 2) else 0)

theorem CSD.LF4.measurable_dExp : Measurable dExp

theorem CSD.LF4.expHalf_eq_withDensity_dExp : expHalf = MeasureTheory.volume.withDensity dExp

theorem CSD.LF4.ratioSqNorm_map_expHalf_pi {M : ℕ} : MeasureTheory.Measure.map ratioN (MeasureTheory.Measure.pi fun (x : Fin (M + 1)) => expHalf) = ↑M.factorial • MeasureTheory.volume.restrict openSimplexFree

D.5c (the general-N Dirichlet law). The free-coordinate ratio map pushes the N-fold product Exp(1/2)^{⊗N} (N = M+1) to M! times the uniform measure on the open simplex — the Dirichlet(1,…,1) law. The qubit ratioSqNorm_map_expHalf_prod is the M = 1 case (1! = 1, uniform on (0,1)).