LF4 plan B, Part 2, Slice 3 (L5.3): the ratio map sends expHalf × expHalf to uniform

Category: 3-Local (the ratio map sends expHalf × expHalf to uniform).

ratioSqNorm_map_expHalf_prod : R∗ (expHalf.prod expHalf) = volume.restrict (Ioo 0 1), where R q = q.1 / (q.1 + q.2).

This is the crux of the moment-marginal route discharging CSD.LF4.fs_moment_pushforward_uniform. The proof is a 2-D change of variables through the diffeomorphism Ψ(T,S) = (T·S, (1−T)·S) from Ioo 0 1 ×ˢ Ioi 0 onto the open quadrant Q = Ioi 0 ×ˢ Ioi 0, with Jacobian determinant S. After the substitution the S-integral factors out as the radial constant ∫_{S>0} (1/4)·S·e^{−S/2} dS = 1 (a Gamma 2 = 1 computation), leaving the bare g(T) integral over Ioo 0 1.

This file builds the four independent ingredients (radial constant, the fderiv and its determinant, injectivity, image) and assembles them into ratioSqNorm_map_expHalf_prod. Foundational-triple-only. See specs/plan-b-detail.md Part 2, Slice 3.

theorem CSD.LF4.lintegral_radial_const : ∫⁻ (S : ℝ) in Set.Ioi 0, ENNReal.ofReal (1 / 4 * S * Real.exp (-S / 2)) = 1

L5.3 radial constant. ∫⁻_{S>0} (1/4)·S·e^{−S/2} dS = 1. This is the normalisation that makes the substituted S-integral collapse to 1; it is the chi-squared(2) total mass, a Gamma 2 = 1! computation.

The substitution diffeomorphism Ψ(T,S) = (T·S, (1−T)·S)

noncomputable def CSD.LF4.Psi (p : ℝ × ℝ) : ℝ × ℝ

The inverse substitution Ψ(T,S) = (T·S, (1−T)·S). It carries Ioo 0 1 ×ˢ Ioi 0 bijectively onto the open quadrant Ioi 0 ×ˢ Ioi 0, with constant-sign Jacobian determinant S.

Equations

• CSD.LF4.Psi p = (p.1 * p.2, (1 - p.1) * p.2)

noncomputable def CSD.LF4.psiFDeriv (p : ℝ × ℝ) : ℝ × ℝ →L[ℝ] ℝ × ℝ

The Fréchet derivative of Ψ at (T,S), as the explicit continuous linear map v ↦ (S·v.1 + T·v.2, (−S)·v.1 + (1−T)·v.2) (matrix [[S,T],[−S,1−T]]).

Equations

• CSD.LF4.psiFDeriv p = (p.1 • ContinuousLinearMap.snd ℝ ℝ ℝ + p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ).prod ((1 - p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + p.2 • (0 - ContinuousLinearMap.fst ℝ ℝ ℝ))

theorem CSD.LF4.hasFDerivAt_Psi (p : ℝ × ℝ) : HasFDerivAt Psi (psiFDeriv p) p

Ψ is Fréchet differentiable everywhere with derivative psiFDeriv. The derivative is taken in the exact shape produced by HasFDerivAt.mul/.prodMk, so the construction is a single exact.

theorem CSD.LF4.psiFDeriv_det (p : ℝ × ℝ) : (psiFDeriv p).det = p.2

Jacobian determinant. det (psiFDeriv (T,S)) = S.

theorem CSD.LF4.injOn_Psi : Set.InjOn Psi (Set.Ioo 0 1 ×ˢ Set.Ioi 0)

Ψ is injective on Ioo 0 1 ×ˢ Ioi 0: from Ψ(T,S) = (TS,(1−T)S), the sum of components recovers S, and then T (since S > 0).

theorem CSD.LF4.image_Psi : Psi '' Set.Ioo 0 1 ×ˢ Set.Ioi 0 = Set.Ioi 0 ×ˢ Set.Ioi 0

The image of Ψ over Ioo 0 1 ×ˢ Ioi 0 is the open quadrant Ioi 0 ×ˢ Ioi 0; the preimage of (A,B) is (A/(A+B), A+B).

L5.3: the ratio map sends expHalf × expHalf to uniform on (0,1)

theorem CSD.LF4.ratioSqNorm_map_expHalf_prod : MeasureTheory.Measure.map (fun (q : ℝ × ℝ) => q.1 / (q.1 + q.2)) (expHalf.prod expHalf) = MeasureTheory.volume.restrict (Set.Ioo 0 1)

L5.3 (the crux). The ratio R q = q.1/(q.1+q.2) pushes expHalf × expHalf to the uniform measure on (0,1). The change of variables through Ψ turns the density into (1/4)·S·e^{−S/2} and the radial S-integral collapses to 1 (lintegral_radial_const), leaving the bare g(T) integral over (0,1).