Stat.MomentProblems
The classical moment problem: which sequences of raw moments come from a probability law, and what the moments pin down about the law.
RawMoment 2 core · 0 supporting This module fixes the single raw-moment notation shared by the MomentProblems developments: the order-k raw moment of a measure on the real line is the Bochner integral of the k-th power. ★ rawMoment_eq_integral
Raw moments of a measure on the real line
This module fixes the single raw-moment notation shared by the MomentProblems developments: the
order-k raw moment of a measure on the real line is the Bochner integral of the k-th power.
Both the finite-moment near-Gaussian perturbation construction and the measure bridge for the
quadratic projection residual are stated in terms of it.
Given a real measure and a nonnegative integer order, the raw moment is Mathlib's moment of the identity random variable. This argument-order adapter is reducible to ProbabilityTheory.moment id k ν, whose value is the integral of the corresponding power.
Definition (Lean source)
For a real measure at a nonnegative integer order, the raw-moment notation equals the integral of the corresponding power.
Proof (Lean source)
Cumulant 4 core · 1 supporting This module provides the general moment-to-cumulant coordinates used throughout the moment-problem layer: the joint cumulant of a pair of real random variables at a given bidegree (defined by the set-partition Möbius for ★ jointCumulant_zero_zero
Cumulants of real random variables, and the Gaussian-law predicate
This module provides the general moment-to-cumulant coordinates used throughout the moment-problem layer: the joint cumulant of a pair of real random variables at a given bidegree (defined by the set-partition Möbius formula on mixed moments), the univariate cumulant of a single real random variable obtained by specializing it, and the predicate "this law on the real line is a Gaussian law".
The total-order-zero cumulant is defined to be zero, matching the constant term of the cumulant-generating function. At every positive total order, the usual set-partition formula is used.
For variables with the needed moments, the second cumulant is the variance, the third is the
centered third moment, and the fourth is the unnormalized fourth cumulant. The standardized ratio
of the fourth cumulant to the variance squared is excess kurtosis when the variance is positive.
This file does not prove that vanishing higher cumulants characterizes Gaussian laws; such a
characterization needs additional moment-existence and determinacy assumptions. The Gaussian
predicate here is the distributional property of being some gaussianReal, including degenerate
Dirac laws.
For a measure on the real line, the Gaussian-law property holds exactly when there exist a real mean and a nonnegative variance parameter such that the measure is the associated normal distribution. The variance parameter may be zero, so point masses count as degenerate Gaussian laws.
Definition (Lean source)
Given a sample space equipped with a σ-algebra, a measure on that space, two real-valued random variables, and two nonnegative integer orders, the joint cumulant at the specified bidegree is zero when both orders are zero; otherwise it is the sum over every partition of the combined slots, with the first slots assigned to the first variable and the remaining slots assigned to the second, of a signed factorial weight times the product, across its blocks, of the mixed moment whose exponents equal that block's counts of first- and second-variable slots.
Definition (Lean source)
Given a sample space equipped with a σ-algebra, a measure on that space, and two real-valued random variables, their joint cumulant at bidegree (0, 0) is zero.
Formal statement
Proof (Lean source)
Given a sample space equipped with a σ-algebra, a measure on that space, a real-valued random variable, and a nonnegative integer order, the cumulant of that order is zero at order zero and otherwise is the joint cumulant obtained by placing that same variable in every slot.
Definition (Lean source)
1 supporting declaration (lemmas, instances)
-
sourceCumulant_zerotheorem — Given a sample space equipped with a σ-algebra, a measure on that space, and a real-valued random variable, its order-zero cumulant is zero.Proof (Lean source)
@[simp] theorem sourceCumulant_zero (μ : Measure Ω) (S : Ω → ℝ) : sourceCumulant μ S 0 = 0 := by simp [sourceCumulant]
MomentCumulantInversion 6 core · 9 supporting Cumulants of positive order are polynomials in the moments, and the polynomial of order r involves the moment of order r linearly (with coefficient one) plus a remainder built only from strictly lower moments. ★ sourceCumulant_eq_cumFromMom★ cumFromMom_momFromCum★ continuous_momFromCum
The triangular moment ↔ cumulant change of coordinates
Cumulants of positive order are polynomials in the moments, and the polynomial of order r
involves the moment of order r linearly (with coefficient one) plus a remainder built only from
strictly lower moments. The order-zero cumulant is set to zero. Triangularity at positive orders
means the change of coordinates inverts: prescribing a cumulant sequence determines a moment
sequence, recursively and uniquely, among sequences normalized to have total mass one and mean
zero.
This module sets up both directions on abstract sequences of reals — no measure is needed to state them — and connects the forward direction to the measure-theoretic cumulant of a real random variable. It also records the two structural facts the inversion is used for downstream: each reconstructed moment depends only on the prescribed cumulants up to the same order (locality), and depends continuously on them.
For a nonnegative order and a real moment sequence, the cumulant read from that moment sequence is zero at order zero; at positive orders it is the signed, factorial-weighted sum over all partitions of a set of that many elements, with each partition contributing the product of the moments indexed by its block sizes.
For a nonnegative order and a real moment sequence, the lower-order remainder of the cumulant formula is the same partition sum with the sole one-block partition omitted; hence it uses only moments of order strictly below that order.
For a real random variable with law ν and any order r, the order-r cumulant of ν equals the abstract combinatorial cumulant formula evaluated at ν's own raw-moment sequence: the measure-theoretic and combinatorial definitions agree.
Formal statement
Proof (Lean source)
For a real sequence of prescribed cumulants, the reconstructed moment sequence is defined by giving its zeroth moment the value one, giving its first moment the value zero, and at every order at least two, subtracting from the prescribed cumulant the lower-order remainder computed from the already reconstructed moments.
Definition (Lean source)
Correctness of the inversion. Reading the cumulants back off the reconstructed moment sequence returns the prescribed cumulants, at every order r at least two.
Formal statement
Proof (Lean source)
Continuity of the inversion. At any fixed order r, the reconstructed moment of that order is a continuous function of the prescribed cumulant sequence, so small perturbations of the target cumulants move the moments only slightly — the key to the openness arguments that use this inversion.
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
cumFromMom_zerotheorem — For a real moment sequence, its order-zero combinatorial cumulant is zero.Proof (Lean source)
-
cumFromMom_eqtheorem — Triangularity. At any positive order the cumulant equals the moment of that same order plus a remainder assembled only from strictly lower moments. This is what makes the moment-to-cumulant map invertible by recursion.Proof (Lean source)
theorem cumFromMom_eq (r : ℕ) (hr : 1 ≤ r) (m : ℕ → ℝ) : cumFromMom r m = m r + restFromMom r m := by let P₀ : Finpartition (Finset.univ : Finset (Fin r)) := Finpartition.indiscrete (by intro hempty have hx : (⟨0, hr⟩ : Fin r) ∈ (Finset.univ : Finset (Fin r)) := Finset.mem_univ _ have hempty' : (Finset.univ : Finset (Fin r)) = ∅ := by simpa using hempty rw [hempty'] at hx exact notMem_empty _ hx) have hfiber : Finset.univ.filter (fun π : Finpartition (Finset.univ : Finset (Fin r)) => π.parts.card = 1) = {P₀} := by ext π simp only [mem_filter, Finset.mem_univ, true_and, Finset.mem_singleton] constructor · intro hp obtain ⟨B, hparts⟩ := Finset.card_eq_one.mp hp have hB : B = (Finset.univ : Finset (Fin r)) := by have := π.sup_parts simpa [hparts] using this apply Finpartition.ext simp [P₀, hparts, hB] · rintro rfl simp [P₀] rw [cumFromMom, if_neg (by omega), ← Finset.sum_filter_add_sum_filter_not (s := Finset.univ) (p := fun π : Finpartition (Finset.univ : Finset (Fin r)) => π.parts.card = 1)] rw [hfiber, Finset.sum_singleton] simp [P₀, restFromMom] -
cumFromMom_congrtheorem — The order-r cumulant depends only on the moments up to order r: changing higher moments leaves it unchanged.hypothesesr :ℕm m' :ℕ → ℝh :∀ kif1 ≤ kandk ≤ rthenm k = m' kconclusioncumFromMom r m = cumFromMom r m'Proof (Lean source)
theorem cumFromMom_congr (r : ℕ) {m m' : ℕ → ℝ} (h : ∀ k, 1 ≤ k → k ≤ r → m k = m' k) : cumFromMom r m = cumFromMom r m' := by by_cases hr : r = 0 · simp [hr] rw [cumFromMom, if_neg hr, cumFromMom, if_neg hr] apply Finset.sum_congr rfl intro π _ congr 1 apply Finset.prod_congr rfl intro B hB exact h B.card (block_card_pos π hB) (block_card_le π hB) -
restFromMom_congrtheorem — The lower-order remainder at order r depends only on the moments strictly below r: changing the order-r moment, or any higher one, leaves it unchanged.hypothesesr :ℕm m' :ℕ → ℝh :∀ kif1 ≤ kandk < rthenm k = m' kconclusionrestFromMom r m = restFromMom r m'Proof (Lean source)
theorem restFromMom_congr (r : ℕ) {m m' : ℕ → ℝ} (h : ∀ k, 1 ≤ k → k < r → m k = m' k) : restFromMom r m = restFromMom r m' := by unfold restFromMom apply Finset.sum_congr rfl intro π hπ have hcard : π.parts.card ≠ 1 := (Finset.mem_filter.mp hπ).2 congr 1 apply Finset.prod_congr rfl intro B hB exact h B.card (block_card_pos π hB) (block_card_lt_of_card_ne_one π hcard hB) -
momFromCum_zerotheorem — The reconstructed moment sequence has total mass one.Proof (Lean source)
-
momFromCum_onetheorem — The reconstructed moment sequence is centered: its mean is zero.Proof (Lean source)
-
momFromCum_succtheorem — The defining recursion: at every order at least two, the reconstructed moment is the target cumulant of that order minus the remainder built from the lower reconstructed moments.hypothesesc :ℕ → ℝr :ℕhr :2 ≤ rconclusionProof (Lean source)
theorem momFromCum_succ (c : ℕ → ℝ) (r : ℕ) (hr : 2 ≤ r) : momFromCum c r = c r - restFromMom r (momFromCum c) := by cases r with | zero => omega | succ r => cases r with | zero => omega | succ n => rw [momFromCum] congr 1 apply restFromMom_congr intro k _ hk simp [hk] -
momFromCum_congrtheorem — Locality of the inversion. The reconstructed moment of order r depends only on the prescribed cumulants of orders two through r, so truncating the cumulant target beyond r is harmless.hypothesesc c' :ℕ → ℝr :ℕh :∀ kif2 ≤ kandk ≤ rthenc k = c' kconclusionmomFromCum c r = momFromCum c' rProof (Lean source)
theorem momFromCum_congr {c c' : ℕ → ℝ} (r : ℕ) (h : ∀ k, 2 ≤ k → k ≤ r → c k = c' k) : momFromCum c r = momFromCum c' r := by induction r using Nat.strong_induction_on with | h r ih => by_cases hr : 2 ≤ r · rw [momFromCum_succ c r hr, momFromCum_succ c' r hr, h r hr le_rfl] congr 1 apply restFromMom_congr intro k hkpos hkr exact ih k hkr (fun j hj hjk => h j hj (hjk.trans (le_of_lt hkr))) · interval_cases r <;> simp -
momFromCum_eq_of_cumtheorem — Uniqueness of the inversion. Any moment sequence with total mass one and mean zero whose cumulants are the prescribed ones is exactly the sequence produced by the recursion.hypothesesconclusionmomFromCum c r = m rProof (Lean source)
theorem momFromCum_eq_of_cum (m : ℕ → ℝ) (hm0 : m 0 = 1) (hm1 : m 1 = 0) (c : ℕ → ℝ) (hc : ∀ r, 2 ≤ r → c r = cumFromMom r m) (r : ℕ) : momFromCum c r = m r := by induction r using Nat.strong_induction_on with | h r ih => by_cases hr : 2 ≤ r · rw [momFromCum_succ c r hr, hc r hr, cumFromMom_eq r (by omega)] have hrest : restFromMom r (momFromCum c) = restFromMom r m := by apply restFromMom_congr intro k _ hkr exact ih k hkr rw [hrest] ring · interval_cases r <;> simp [hm0, hm1]
AtomicLaw 4 core · 4 supporting This module builds the finitely supported probability laws used as explicit witnesses in truncated moment problems: a finite list of distinct real atom locations carrying a matching list of weights. ★ isProbabilityMeasure_atomicLaw★ not_isGaussianLaw_atomicLaw
Finite atomic laws on the real line
This module builds the finitely supported probability laws used as explicit witnesses in truncated moment problems: a finite list of distinct real atom locations carrying a matching list of weights. It records how such a law integrates an arbitrary function (a weighted sum over the atoms), when it is a probability measure, how much mass it puts on each atom, that all of its moments are finite (the support is bounded), and that it is never Gaussian as soon as two atoms carry strictly positive mass.
The last fact is what makes finite atomic laws usable as non-Gaussian witnesses: a nondegenerate normal law has no atoms at all, and a degenerate one is a single point mass, so two distinct atoms of positive mass rule out both cases.
For a natural number of atoms, a list of their real locations, and a matching list of real weights, the weight assigned to a real point is the sum of the weights of precisely those atoms located at that point.
For a natural number of atoms, a list of their real locations, and a matching list of real weights, the finite atomic law is the measure that puts each weight as point mass at its corresponding location.
Definition (Lean source)
A finite atomic law on the real line, built from n pairwise distinct atom locations carrying nonnegative weights that sum to one, is a probability measure.
Formal statement
Proof (Lean source)
A finite atomic probability law with at least two locations that are pairwise distinct and each carry strictly positive mass is not a Gaussian law: a normal law with positive variance has no point masses at all, and one with zero variance is a single point mass.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
atomicWeight_applytheorem — When the atom locations are pairwise distinct, the total weight sitting at one of them is exactly that atom's own weight — no two indices collide.hypothesesconclusionatomicWeight n x p (x j) = p jProof (Lean source)
theorem atomicWeight_apply {n : ℕ} {x : Fin n → ℝ} {p : Fin n → ℝ} (hx : Injective x) (j : Fin n) : atomicWeight n x p (x j) = p j := by classical simp [atomicWeight, hx.eq_iff] -
integral_atomicLawtheorem — Integrating a function against a finite atomic law with distinct locations and nonnegative weights gives the weighted sum of the function's values at the atoms.hypothesesProof (Lean source)
theorem integral_atomicLaw {n : ℕ} {x : Fin n → ℝ} {p : Fin n → ℝ} (hx : Injective x) (hp : ∀ i, 0 ≤ p i) (f : ℝ → ℝ) : ∫ t, f t ∂(atomicLaw n x p) = ∑ i : Fin n, p i * f (x i) := by classical rw [atomicLaw, integral_discreteMeasure] · rw [Finset.sum_image hx.injOn] apply Finset.sum_congr rfl intro i hi rw [atomicWeight_apply hx] simp [smul_eq_mul] · intro t ht obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp ht rw [atomicWeight_apply hx] exact hp i -
atomicLaw_singletontheorem — A finite atomic law with distinct locations and nonnegative weights puts exactly its own weight of mass on each single atom.hypothesesProof (Lean source)
theorem atomicLaw_singleton {n : ℕ} {x : Fin n → ℝ} {p : Fin n → ℝ} (hx : Injective x) (hp : ∀ i, 0 ≤ p i) (j : Fin n) : atomicLaw n x p {x j} = ofReal (p j) := by classical have hpj := hp j rw [atomicLaw, discreteMeasure_singleton] · rw [atomicWeight_apply hx] · exact Finset.mem_image.mpr ⟨j, Finset.mem_univ j, rfl⟩ -
memLp_id_atomicLawtheorem — A finite atomic probability law has finite moments of every order: its support is a bounded finite set, so the identity function is bounded almost everywhere and hence in every Lᵖ.hypothesesProof (Lean source)
theorem memLp_id_atomicLaw {n : ℕ} {x : Fin n → ℝ} {p : Fin n → ℝ} (hx : Injective x) (hp : ∀ i, 0 ≤ p i) (hsum : ∑ i, p i = 1) (q : ℝ≥0∞) : MemLp (id : ℝ → ℝ) q (atomicLaw n x p) := by classical let C : ℝ := ∑ i : Fin n, |x i| letI : IsProbabilityMeasure (atomicLaw n x p) := isProbabilityMeasure_atomicLaw hx hp hsum apply memLp_of_bounded · rw [ae_iff] change atomicLaw n x p (Icc (-C) C)ᶜ = 0 apply discreteMeasure_apply_compl_of_subset intro t ht obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp ht have hxi : |x i| ≤ C := by dsimp [C] exact Finset.single_le_sum (fun j hj ↦ abs_nonneg (x j)) (Finset.mem_univ i) exact (abs_le.mp hxi) · exact continuous_id.aestronglyMeasurable
ScoreProgram 4 core · 3 supporting This file solves the optimization problem that uses the projection residual from ResidualQuadratic.ProjectionResidual. ★ scoreCost_eq
Constrained quadratic score program dual to the L² projection residual
This file solves the optimization problem that uses the projection residual from
ResidualQuadratic.ProjectionResidual. For a probability measure μ on ℝ with finite fourth
moment and positive variance, consider the constrained minimum-norm score program: among all
scores
s ∈ L²(μ) that are moment-orthogonal to 1 and y and carry a prescribed y²-moment x,
minimize ∫ s² dμ subject to ∫ s dμ = 0, ∫ y·s dμ = 0, ∫ y²·s dμ = x,
what is the least achievable L²(μ) norm² of s?
The answer is the duality identity
scoreCost μ x = x² / r, where r = l2ResidualQuadratic μ
is the (positive) L² residual of regressing y² on span{1, y} (ProjectionResidual.lean). This
is the classic Lagrangian / minimum-norm-interpolation duality: the constrained least-norm value is
(prescribed moment)² / (residual variance of the constrained direction).
Contents
* FeasibleScore μ x s — feasibility: s ∈ L²(μ) with the three moment constraints.
* optScore μ x — the optimal score s*(y) = (x/r)·q(y), q the projection residual.
* optScore_feasible, optScore_cost — s* is feasible and achieves cost x²/r (attainment).
* feasibleScore_cost_lower_bound — every feasible s has ∫ s² ≥ x²/r (completing the square:
∫ (s − (x/r)q)² = ∫ s² − x²/r ≥ 0, using ∫ q·s = x and ∫ q² = r).
* scoreCost, scoreCost_eq — the program value and the headline duality scoreCost μ x = x²/r.
Reuse
The identity is the reusable score-cost primitive for arm-specific moment problems: once an arm law
has residual variance r_{a,ν}, a target moment displacement x has least score norm
J_{a,ν}(x) = x² / r_{a,ν}.
Feasibility of a score. s : ℝ → ℝ is feasible for target x if it lies in L²(μ) and is moment-orthogonal to 1 and y while carrying prescribed y²-moment x: s ∈ L²(μ), ∫ s dμ = 0, ∫ y·s dμ = 0, ∫ y²·s dμ = x.
Definition (Lean source)
s is orthogonal to the constant 1: ∫ s dμ = 0.
s is orthogonal to y: ∫ y·s dμ = 0.
s carries the prescribed y²-moment: ∫ y²·s dμ = x.
For a measure on the real line and a real target moment, the optimal score assigns to each real value the projection residual of its square multiplied by the target moment divided by the closed-form residual scalar calculated from the first four raw moments of the measure.
Definition (Lean source)
For a measure on the real line and a real target moment, the score-program value is the infimum, over all square-integrable real-valued functions whose mean and first moment-weighted mean are zero and whose second-moment-weighted mean equals the target, of their integrated square.
Definition (Lean source)
The score-program duality (headline). For a probability measure μ on ℝ with a finite fourth moment and first moment squared strictly below the second moment (positive variance), if moreover the closed-form residual l2ResidualQuadratic μ is positive, then for every target y²-moment x, the value of the constrained minimum-norm score program equals x² / l2ResidualQuadratic μ:
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
optScore_feasibletheorem — Feasibility of the optimal score. s* = (x/r)·q is a feasible score for target x: it lies in L²(μ) and satisfies the three moment constraints. The y²-moment constraint uses ∫ y²·q = r and (x/r)·r = x (needs r ≠ 0).Proof (Lean source)
theorem optScore_feasible (μ : Measure ℝ) [IsProbabilityMeasure μ] (h : FiniteMoment4 μ) (hnd : rawMoment μ 1 ^ 2 < rawMoment μ 2) (hr : 0 < l2ResidualQuadratic μ) (x : ℝ) : FeasibleScore μ x (optScore μ x) := by refine ⟨?_, ?_, ?_, ?_⟩ · exact (projResidual_memL2 μ h).const_mul (x / l2ResidualQuadratic μ) · simp [optScore, integral_const_mul, integral_projResidual μ h hnd] · calc ∫ y, y * optScore μ x y ∂μ = ∫ y, (x / l2ResidualQuadratic μ) * (y * projResidual μ y) ∂μ := by apply integral_congr_ae filter_upwards with y simp [optScore] ring _ = 0 := by simp [integral_const_mul, integral_id_mul_projResidual μ h hnd] · calc ∫ y, y ^ 2 * optScore μ x y ∂μ = ∫ y, (x / l2ResidualQuadratic μ) * (y ^ 2 * projResidual μ y) ∂μ := by apply integral_congr_ae filter_upwards with y simp [optScore] ring _ = x := by rw [integral_const_mul, integral_sq_mul_projResidual μ h hnd] exact div_mul_cancel₀ x (ne_of_gt hr) -
optScore_costtheorem — Attainment. The optimal score s* achieves cost exactly x² / r: ∫ (s*)² dμ = ∫ (x/r)²·q² dμ = (x/r)²·r = x²/r.hypothesesconclusion∫ y, optScore μ x y ^ 2 ∂μ = x ^ 2 / l2ResidualQuadratic μProof (Lean source)
theorem optScore_cost (μ : Measure ℝ) [IsProbabilityMeasure μ] (h : FiniteMoment4 μ) (hnd : rawMoment μ 1 ^ 2 < rawMoment μ 2) (hr : 0 < l2ResidualQuadratic μ) (x : ℝ) : ∫ y, optScore μ x y ^ 2 ∂μ = x ^ 2 / l2ResidualQuadratic μ := by calc ∫ y, optScore μ x y ^ 2 ∂μ = ∫ y, (x / l2ResidualQuadratic μ) ^ 2 * projResidual μ y ^ 2 ∂μ := by apply integral_congr_ae filter_upwards with y simp [optScore, mul_pow] _ = x ^ 2 / l2ResidualQuadratic μ := by rw [integral_const_mul, integral_sq_projResidual μ h hnd] field_simp [ne_of_gt hr] -
feasibleScore_cost_lower_boundtheorem — Lower bound (duality ≤). Every feasible score has cost at least x² / r.hypothesesconclusionx ^ 2 / l2ResidualQuadratic μ ≤ ∫ y, s y ^ 2 ∂μProof (Lean source)
theorem feasibleScore_cost_lower_bound (μ : Measure ℝ) [IsProbabilityMeasure μ] (h : FiniteMoment4 μ) (hnd : rawMoment μ 1 ^ 2 < rawMoment μ 2) (hr : 0 < l2ResidualQuadratic μ) (x : ℝ) {s : ℝ → ℝ} (hs : FeasibleScore μ x s) : x ^ 2 / l2ResidualQuadratic μ ≤ ∫ y, s y ^ 2 ∂μ := by let r := l2ResidualQuadratic μ let c := x / r let q := projResidual μ have hq_mem : MemLp q 2 μ := by simpa [q] using projResidual_memL2 μ h have hs_int : Integrable s μ := hs.memL2.integrable (by norm_num) have hys_int : Integrable (fun y : ℝ => y * s y) μ := (memL2_id μ h).integrable_mul hs.memL2 have hy2s_int : Integrable (fun y : ℝ => y ^ 2 * s y) μ := (memL2_sq μ h).integrable_mul hs.memL2 have hqs_int : Integrable (fun y : ℝ => q y * s y) μ := hq_mem.integrable_mul hs.memL2 have hq2_int : Integrable (fun y : ℝ => q y ^ 2) μ := hq_mem.integrable_sq have hs2_int : Integrable (fun y : ℝ => s y ^ 2) μ := hs.memL2.integrable_sq have hqs : ∫ y, q y * s y ∂μ = x := by calc ∫ y, q y * s y ∂μ = ∫ y, y ^ 2 * s y - optIntercept μ * s y - optSlope μ * (y * s y) ∂μ := by apply integral_congr_ae filter_upwards with y simp [q, projResidual] ring _ = (∫ y, y ^ 2 * s y - optIntercept μ * s y ∂μ) - (∫ y, optSlope μ * (y * s y) ∂μ) := by exact integral_sub (hy2s_int.sub (hs_int.const_mul _)) (hys_int.const_mul _) _ = ((∫ y, y ^ 2 * s y ∂μ) - (∫ y, optIntercept μ * s y ∂μ)) - (∫ y, optSlope μ * (y * s y) ∂μ) := by rw [integral_sub hy2s_int (hs_int.const_mul _)] _ = (∫ y, y ^ 2 * s y ∂μ) - (∫ y, optIntercept μ * s y ∂μ) - (∫ y, optSlope μ * (y * s y) ∂μ) := by ring _ = x := by simp [integral_const_mul, hs.cov_sq, hs.mean_zero, hs.cov_id_zero] have hnn : 0 ≤ ∫ y, (s y - c * q y) ^ 2 ∂μ := integral_nonneg (fun y => sq_nonneg (s y - c * q y)) have hexpand : ∫ y, (s y - c * q y) ^ 2 ∂μ = (∫ y, s y ^ 2 ∂μ) - 2 * c * (∫ y, q y * s y ∂μ) + c ^ 2 * (∫ y, q y ^ 2 ∂μ) := by calc ∫ y, (s y - c * q y) ^ 2 ∂μ = ∫ y, s y ^ 2 - 2 * c * (q y * s y) + c ^ 2 * q y ^ 2 ∂μ := by apply integral_congr_ae filter_upwards with y ring _ = (∫ y, s y ^ 2 - 2 * c * (q y * s y) ∂μ) + (∫ y, c ^ 2 * q y ^ 2 ∂μ) := by exact integral_add (hs2_int.sub (hqs_int.const_mul _)) (hq2_int.const_mul _) _ = ((∫ y, s y ^ 2 ∂μ) - (∫ y, 2 * c * (q y * s y) ∂μ)) + (∫ y, c ^ 2 * q y ^ 2 ∂μ) := by rw [integral_sub hs2_int (hqs_int.const_mul _)] _ = (∫ y, s y ^ 2 ∂μ) - (∫ y, 2 * c * (q y * s y) ∂μ) + (∫ y, c ^ 2 * q y ^ 2 ∂μ) := by ring _ = (∫ y, s y ^ 2 ∂μ) - 2 * c * (∫ y, q y * s y ∂μ) + c ^ 2 * (∫ y, q y ^ 2 ∂μ) := by rw [integral_const_mul, integral_const_mul] have hnonneg : 0 ≤ (∫ y, s y ^ 2 ∂μ) - 2 * c * x + c ^ 2 * r := by rw [hexpand, hqs] at hnn simpa [q, r, integral_sq_projResidual μ h hnd] using hnn have halg : 2 * c * x - c ^ 2 * r = x ^ 2 / r := by subst c subst r field_simp [ne_of_gt hr] ring linarith
SymmetricAtomSolve 11 core · 15 supporting Fix L + 1 equally spaced atoms placed symmetrically about the origin. ★ continuous_cumulantToWeights★ cumulantToWeights_uniformCumulantPoint
Solving for atom weights that match a prescribed cumulant target
Fix L + 1 equally spaced atoms placed symmetrically about the origin. Matching the raw moments
of orders 0, 1, …, L of a weight vector supported on those atoms to a prescribed moment target is
a square linear system whose matrix is a transposed Vandermonde matrix in the atom locations. The
atoms being distinct, that matrix is invertible, so the weights are recovered from the moment
target by a linear — in particular continuous — solve.
Composing this solve with the triangular moment↔cumulant inversion gives the map this module exports: prescribed truncated cumulants ↦ atom weights, which is continuous, and which sends the cumulants of the uniform-weight law back to the uniform weights. That is exactly what is needed to conclude, by openness of the strict-positivity constraint, that a whole neighborhood of cumulant targets is matched by genuine (positive-weight) probability laws.
Nothing here yet asserts positivity of the solved weights: it is a pure linear-algebra and
continuity layer. The realizability conclusion is drawn in TruncatedCumulantInterior.
For a nonnegative integer L, the symmetric atom locations are the L + 1 real numbers −L, −L + 2, …, L, indexed in increasing order; equivalently, the location with index i is twice i minus L.
Definition (Lean source)
For a nonnegative integer L, the uniform weight vector assigns mass to each of the L + 1 symmetric atoms.
Definition (Lean source)
For a nonnegative integer L, the raw-moment sequence of the uniform law on the symmetric atoms assigns to every nonnegative order the equally weighted average of that power of the L + 1 symmetric atom locations.
Definition (Lean source)
For a nonnegative integer L, the cumulant sequence of the uniform law on the symmetric atoms is the cumulant sequence calculated from that law's raw moments.
Definition (Lean source)
For a nonnegative integer L, the Vandermonde matrix of the symmetric atoms is the square real matrix whose row for each atom lists successive powers of that atom, from power zero through power L.
Definition (Lean source)
For a nonnegative integer L and a prescribed vector of real raw moments of orders zero through L, the moment-matching weight vector is the result of applying the inverse transpose of the Vandermonde matrix of the symmetric atoms to that vector.
Definition (Lean source)
For a nonnegative integer L and a finite coordinate vector whose entries at orders two through L are prescribed cumulants, the zero-padded coordinate sequence agrees with that vector through order L and equals zero at every higher order. Entries zero and one are normalization placeholders and are ignored by the centered moment reconstruction.
Definition (Lean source)
For a nonnegative integer L and a coordinate vector prescribing cumulants at orders two through L, the cumulant-to-weights map reconstructs the centered raw moments and returns the symmetric-atom weights solving their Vandermonde moment-matching system. The entries at orders zero and one are ignored because the reconstructed mass and mean are fixed to one and zero.
Definition (Lean source)
The cumulant-to-weights map is continuous. For any truncation order L, the map sending a truncated cumulant target to the recovered symmetric-atom weights is continuous, since both the moment↔cumulant inversion and the Vandermonde solve it composes are continuous.
Formal statement
Proof (Lean source)
For a nonnegative integer L, the base cumulant target is the vector of cumulants of orders zero through L of the uniform probability law on the symmetric atoms.
Definition (Lean source)
The base point maps to the uniform weights. For any truncation order L, feeding the cumulants of the uniform-weight law on the symmetric atoms into the cumulant-to-weights map returns exactly the uniform weights — all strictly positive, hence strictly inside the positivity constraints.
Formal statement
Proof (Lean source)
15 supporting declarations (lemmas, instances)
-
symmetricAtoms_injectivetheorem — The symmetric atoms are pairwise distinct.Proof (Lean source)
theorem symmetricAtoms_injective (L : ℕ) : Injective (symmetricAtoms L) := by intro i j hij apply Fin.ext dsimp [symmetricAtoms] at hij have : (i.val : ℝ) = j.val := by linarith exact_mod_cast this -
symmetricAtoms_sumtheorem — The symmetric atoms sum to zero — they are balanced about the origin.Proof (Lean source)
theorem symmetricAtoms_sum (L : ℕ) : ∑ i : Fin (L + 1), symmetricAtoms L i = 0 := by change ∑ i : Fin (L + 1), (2 * (i.val : ℝ) - (L : ℝ)) = 0 rw [Fin.sum_univ_eq_sum_range (fun i => 2 * (i : ℝ) - (L : ℝ))] have hs : (∑ i ∈ range (L + 1), (i : ℝ)) * 2 = (L + 1 : ℝ) * L := by have hn : (∑ i ∈ range (L + 1), i) * 2 = (L + 1) * L := by simpa using Finset.sum_range_id_mul_two (L + 1) have hr := congrArg (fun n : ℕ => (n : ℝ)) hn simpa only [Nat.cast_mul, Nat.cast_ofNat, Nat.cast_sum, Nat.cast_add, Nat.cast_one] using hr calc ∑ i ∈ range (L + 1), (2 * (i : ℝ) - (L : ℝ)) = 2 * (∑ i ∈ range (L + 1), (i : ℝ)) - (L + 1 : ℝ) * L := by rw [Finset.sum_sub_distrib] simp [Finset.mul_sum] _ = 0 := by linarith -
uniformWeights_postheorem — Every uniform weight is strictly positive.hypothesesL :ℕi :conclusion0 < uniformWeights L iProof (Lean source)
theorem uniformWeights_pos (L : ℕ) : ∀ i, 0 < uniformWeights L i := by intro i dsimp [uniformWeights] positivity -
uniformWeights_sumtheorem — The uniform weights sum to one, so the uniform-weight atomic law is a probability law.hypothesesL :ℕconclusion∑ i, uniformWeights L i = 1Proof (Lean source)
theorem uniformWeights_sum (L : ℕ) : ∑ i, uniformWeights L i = 1 := by simp [uniformWeights] field_simp -
uniformWeights_meantheorem — The uniform-weight law on the symmetric atoms has mean zero.Proof (Lean source)
theorem uniformWeights_mean (L : ℕ) : ∑ i, uniformWeights L i * symmetricAtoms L i = 0 := by change ∑ i, (1 / (L + 1 : ℝ)) * symmetricAtoms L i = 0 rw [← Finset.mul_sum] exact mul_eq_zero_of_right _ (symmetricAtoms_sum L) -
uniformMoments_zerotheorem — The uniform-weight law has total mass one.Proof (Lean source)
theorem uniformMoments_zero (L : ℕ) : uniformMoments L 0 = 1 := by simpa [uniformMoments] using uniformWeights_sum L -
uniformMoments_onetheorem — The uniform-weight law is centered.Proof (Lean source)
theorem uniformMoments_one (L : ℕ) : uniformMoments L 1 = 0 := by simpa [uniformMoments] using uniformWeights_mean L -
momFromCum_uniformCumulantstheorem — Inverting the cumulants of the uniform-weight law returns its moments: the base point is a fixed point of the moment↔cumulant round trip.Proof (Lean source)
theorem momFromCum_uniformCumulants (L k : ℕ) : momFromCum (uniformCumulants L) k = uniformMoments L k := by apply momFromCum_eq_of_cum (uniformMoments L) (uniformMoments_zero L) (uniformMoments_one L) intro r hr rfl -
atomVandermonde_transpose_isUnittheorem — The transposed Vandermonde matrix of the symmetric atoms is invertible, because the atoms are pairwise distinct.Proof (Lean source)
theorem atomVandermonde_transpose_isUnit (L : ℕ) : IsUnit (atomVandermonde L).transpose.det := by rw [Matrix.det_transpose, isUnit_iff_ne_zero] exact Matrix.det_vandermonde_ne_zero_iff.mpr (symmetricAtoms_injective L) -
atomSolve_spectheorem — The solved weights do reproduce the target: the weighted sum of the k-th powers of the atoms is the k-th target moment, for every order k from 0 to L.hypothesesconclusion∑ i, atomSolve L b i * symmetricAtoms L i ^ (k : ℕ) = b kProof (Lean source)
theorem atomSolve_spec (L : ℕ) (b : Fin (L + 1) → ℝ) (k : Fin (L + 1)) : ∑ i, atomSolve L b i * symmetricAtoms L i ^ (k : ℕ) = b k := by have h := congrFun (Matrix.mulVec_mulVec b (atomVandermonde L).transpose (atomVandermonde L).transpose⁻¹) k rw [Matrix.mul_nonsing_inv _ (atomVandermonde_transpose_isUnit L), Matrix.one_mulVec] at h calc ∑ i, atomSolve L b i * symmetricAtoms L i ^ (k : ℕ) = ∑ i, symmetricAtoms L i ^ (k : ℕ) * atomSolve L b i := by apply Finset.sum_congr rfl intro i hi rw [mul_comm] _ = ((atomVandermonde L).transpose.mulVec (atomSolve L b)) k := by simp [atomVandermonde, mulVec, dotProduct, Matrix.vandermonde_apply] _ = b k := by simpa [atomSolve] using h -
atomSolve_mulVectheorem — The solve is a left inverse of taking moments: solving for the weights from the moments that a given weight vector produces returns that same weight vector.hypothesesL :ℕq :Fin (L + 1) → ℝconclusionatomSolve L ((atomVandermonde L).transpose.mulVec q) = qProof (Lean source)
theorem atomSolve_mulVec (L : ℕ) (q : Fin (L + 1) → ℝ) : atomSolve L ((atomVandermonde L).transpose.mulVec q) = q := by funext k have h := congrFun (Matrix.mulVec_mulVec q (atomVandermonde L).transpose⁻¹ (atomVandermonde L).transpose) k rw [Matrix.nonsing_inv_mul _ (atomVandermonde_transpose_isUnit L), Matrix.one_mulVec] at h exact h -
atomSolve_uniformMomentstheorem — Solving at the moments of the uniform-weight law returns the uniform weights.Proof (Lean source)
theorem atomSolve_uniformMoments (L : ℕ) : atomSolve L (fun k => uniformMoments L k.val) = uniformWeights L := by rw [← atomSolve_mulVec L (uniformWeights L)] congr 1 funext k simp [atomVandermonde, uniformMoments, mulVec, dotProduct, Matrix.vandermonde_apply, mul_comm] -
continuous_atomSolvetheorem — The moment-matching solve depends continuously on the target moments — it is linear.Proof (Lean source)
@[fun_prop] theorem continuous_atomSolve (L : ℕ) : Continuous (atomSolve L) := by apply continuous_pi intro i unfold atomSolve mulVec dotProduct apply continuous_finsetSum intro j hj exact continuous_const.mul (continuous_apply j) -
continuous_padCumulantstheorem — Zero-extension of a finite cumulant target is continuous in the target.Proof (Lean source)
@[fun_prop] theorem continuous_padCumulants (L : ℕ) : Continuous (padCumulants L) := by apply continuous_pi intro k by_cases h : k < L + 1 · simpa [padCumulants, h] using (continuous_apply (⟨k, h⟩ : Fin (L + 1))) · simpa [padCumulants, h] using (continuous_const : Continuous (fun _ : Fin (L + 1) → ℝ => (0 : ℝ))) -
momFromCum_padCumulants_uniformtheorem — Inverting the base cumulant target order by order returns the moments of the uniform-weight law.Proof (Lean source)
theorem momFromCum_padCumulants_uniform (L : ℕ) (k : Fin (L + 1)) : momFromCum (padCumulants L (uniformCumulantPoint L)) k.val = uniformMoments L k.val := by rw [← momFromCum_uniformCumulants L k.val] apply momFromCum_congr intro j hj hjk simp [padCumulants, uniformCumulantPoint, show j < L + 1 by omega]
TruncatedCumulantInterior 2 core · 0 supporting The main result of this module says that the truncated cumulant sequences of orders two through L attainable by *centered, non-Gaussian* probability laws on the real line with finite L-th moment fill up a set with nonemp ★ truncatedCumulantInterior
The truncated cumulant range has nonempty interior
The main result of this module says that the truncated cumulant sequences of orders two through
L attainable by centered, non-Gaussian probability laws on the real line with finite L-th
moment fill up a set with nonempty interior: there is one attainable cumulant vector all of whose
sufficiently small perturbations are again attainable by such a law.
The proof is constructive rather than an appeal to the general (truncated Hamburger) moment
problem. Put L + 1 distinct equally spaced symmetric atoms on the line. Matching the first
L + 1 raw moments of a weight vector to a target is then a linear system with a transposed
Vandermonde matrix, hence invertible, and the moment target itself is obtained from the cumulant
target by the triangular moment↔cumulant inversion — so weights depend continuously on the
prescribed cumulants (SymmetricAtomSolve). At the uniform weight vector all weights are strictly
positive, and positivity is an open condition, so every nearby cumulant target still solves to
strictly positive weights, i.e. to a genuine probability law. That law is centered (the atoms are
symmetric and the first-moment equation is part of the solved system), has all moments finite
(finite support), and is non-Gaussian (at least two atoms carry positive mass).
The order L = 0 case is degenerate — a single atom would be a point mass, i.e. a degenerate
Gaussian — and is handled separately by an explicit fair two-point law on ±1.
Background references: Akhiezer (1965), The Classical Moment Problem; Curto–Fialkow (1991), Recursiveness, Positivity, and Truncated Moment Problems; and Schmüdgen (2017), The Moment Problem, Chapter 10. The result below is the separate constructive centered-cumulant specialization described above; it does not use a flat-extension theorem.
For a nonnegative truncation order, the interior-of-the-truncated-cumulant-range condition says that there exist a real cumulant sequence and a strictly positive real radius such that every real sequence whose entries of every order from two through the truncation order differ from the corresponding target entries by less than that radius is the cumulant sequence, at each of those orders, of some centered non-Gaussian probability law on the real line with finite moment of the truncation order.
Definition (Lean source)
The truncated cumulant range has nonempty interior. For every truncation order L, there is a cumulant vector, of orders two through L, together with a strictly positive radius, such that every cumulant vector within that radius is the truncated cumulant vector of some centered, non-Gaussian probability law on the real line with finite L-th moment.