LF4 plan B, Part 2, Slice 1 (L5.1): the single-block squared-norm law is Exp(1/2)

Category: 3-Local (the single-block squared-norm law is Exp(1/2)).

sqNorm_map_gaussian2 : Measure.map (fun p => p.1^2 + p.2^2) gaussian2 = expHalf, where gaussian2 is the 2-D standard Gaussian on ℝ × ℝ (explicit Lebesgue density (1/2π)·exp(-(x²+y²)/2)) and expHalf is the exponential measure with rate 1/2 on ℝ (density (1/2)·exp(-s/2)·𝟙_{s>0}).

This is the radial-marginal computation ‖·‖²∗ N(0,I₂) = Exp(1/2), the entry slice of the route discharging CSD.LF4.fs_moment_pushforward_uniform. Worked on plain ℝ × ℝ (not EuclideanSpace/stdGaussian) to keep polarCoord friction free. See specs/plan-b-detail.md Part 2, Slice 1.

The proof is a Lebesgue-integral characterisation (Measure.ext_of_lintegral): push the measure through the squared-norm map, expose the Gaussian density, change to polar coordinates (lintegral_comp_polarCoord_symm), kill the angular factor (a constant integral over Ioo (-π) π of length 2π cancelling the 1/2π), and substitute s = r² via the 1-D Jacobian change of variables (lintegral_image_eq_lintegral_abs_deriv_mul, f r = r², f' r = 2r, f '' Ioi 0 = Ioi 0).

noncomputable def CSD.LF4.gaussian2 : MeasureTheory.Measure (ℝ × ℝ)

The 2-D standard Gaussian on ℝ × ℝ, with explicit Lebesgue density (1/2π)·exp(-(x²+y²)/2) (= gaussianPDFReal 0 1 x · gaussianPDFReal 0 1 y).

Equations

• CSD.LF4.gaussian2 = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ENNReal.ofReal (1 / (2 * Real.pi) * Real.exp (-(p.1 ^ 2 + p.2 ^ 2) / 2))

noncomputable def CSD.LF4.expHalf : MeasureTheory.Measure ℝ

The exponential measure with rate 1/2 on ℝ: density (1/2)·exp(-s/2)·𝟙_{s>0}. This is Exp(1/2), equivalently the chi-squared law with two degrees of freedom; it is the radial-marginal target of the 2-D Gaussian.

Equations

• CSD.LF4.expHalf = MeasureTheory.volume.withDensity fun (s : ℝ) => ENNReal.ofReal (if 0 < s then 1 / 2 * Real.exp (-s / 2) else 0)

theorem CSD.LF4.measurable_gaussian2_density : Measurable fun (p : ℝ × ℝ) => ENNReal.ofReal (1 / (2 * Real.pi) * Real.exp (-(p.1 ^ 2 + p.2 ^ 2) / 2))

The Gaussian density (1/2π)·exp(-(x²+y²)/2) is measurable.

theorem CSD.LF4.measurable_expHalf_density : Measurable fun (s : ℝ) => ENNReal.ofReal (if 0 < s then 1 / 2 * Real.exp (-s / 2) else 0)

The expHalf density (1/2)·exp(-s/2)·𝟙_{s>0} is measurable.

theorem CSD.LF4.sqNorm_map_gaussian2 : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => p.1 ^ 2 + p.2 ^ 2) gaussian2 = expHalf

L5.1. The squared-norm pushes the 2-D standard Gaussian to Exp(1/2): (fun p => p.1² + p.2²)∗ gaussian2 = expHalf.

Slice 2 (L5.2): block product = independence

gaussian2 is the product of two 1-D standard Gaussians (gaussianReal 0 1), and the joint law of the two block squared-norms of a 4-D standard Gaussian is expHalf.prod expHalf — the joint law factors, which is exactly the independence statement (no separate IndepFun needed; the product measure carries it). See specs/plan-b-detail.md Part 2, Slice 2.

theorem CSD.LF4.gaussianPDFReal_zero_one (x : ℝ) : ProbabilityTheory.gaussianPDFReal 0 1 x = (√(2 * Real.pi))⁻¹ * Real.exp (-x ^ 2 / 2)

gaussianPDFReal 0 1 in explicit form: (√(2π))⁻¹·exp(-x²/2).

theorem CSD.LF4.gaussian2_eq_prod : gaussian2 = (ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)

L5.2a (2-D bridge). The explicit-density gaussian2 is the product of two 1-D standard Gaussians gaussianReal 0 1.

theorem CSD.LF4.blockSqNorm_map_gaussian2_prod : MeasureTheory.Measure.map (Prod.map (fun (p : ℝ × ℝ) => p.1 ^ 2 + p.2 ^ 2) fun (p : ℝ × ℝ) => p.1 ^ 2 + p.2 ^ 2) (gaussian2.prod gaussian2) = expHalf.prod expHalf

L5.2b (block product = independence). The joint law of the two block squared-norms factors: (Prod.map ‖·‖² ‖·‖²)∗ (gaussian2 × gaussian2) = expHalf × expHalf. This is the independence statement — the product measure on the right carries it, so no separate IndepFun lemma is required.

Slice C (Part 2a, general N): the N-fold block law

The general-N analogue of blockSqNorm_map_gaussian2_prod: the joint law of the N block squared-norms of an N-fold product of 2-D Gaussians factors as the N-fold product of Exp(1/2) measures. Clean Measure.pi_map_pi application, each factor closed by Slice 1 (sqNorm_map_gaussian2). The EuclideanSpace ℝ (Fin N × Fin 2) ↔ Measure.pi (Fin N) gaussian2 bridge (the stdGaussian reindex plumbing) is deferred to the assembly slice, exactly as the qubit deferred its EuclideanSpace bridge from Slice 2 to Slice 4.

instance CSD.LF4.instProbGaussian2 : MeasureTheory.IsProbabilityMeasure gaussian2

gaussian2 is a probability measure (explicit Gaussian density integrates to 1).

instance CSD.LF4.instProbExpHalf : MeasureTheory.IsProbabilityMeasure expHalf

expHalf is a probability measure (it is the squared-norm pushforward of gaussian2, a probability measure).

theorem CSD.LF4.blockSqNorm_map_gaussianN_pi {N : ℕ} : MeasureTheory.Measure.map (fun (q : Fin N → ℝ × ℝ) (i : Fin N) => (q i).1 ^ 2 + (q i).2 ^ 2) (MeasureTheory.Measure.pi fun (x : Fin N) => gaussian2) = MeasureTheory.Measure.pi fun (x : Fin N) => expHalf

Slice C (general N): the N-fold block law. The joint law of the N block squared-norms factors as the N-fold product Exp(1/2)^{⊗N}: (fun q i => (q i).1² + (q i).2²)∗ (pi gaussian2) = pi expHalf. The independence statement at general N — the product measure carries it.