Stat.Nonparametric.MomentProblems
Moment-problem substrate for nonparametric statistics: raw-moment algebra, L² projection residuals, constrained score programs, and sharp bounded-outcome residual envelopes.
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 given by integrating the corresponding power. This is the real-valued Bochner integral, which is zero when the power is not integrable, so it is the moment only when the moment exists.
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 3 core · 0 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
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".
These are the plain textbook objects: the second cumulant is the variance, the third is the
centered third moment, the fourth is the excess kurtosis, and a Gaussian law is exactly a law
whose cumulants above order two all vanish. The Gaussian predicate here is the distributional
one — being some gaussianReal with a mean and a variance, degenerate Diracs included — and is
the form in which non-Gaussianity assumptions (as in linear non-Gaussian causal discovery) are
stated.
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 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, a real-valued random variable, and a nonnegative integer order, the cumulant of that order is the joint cumulant obtained by placing that same variable in every slot.
Definition (Lean source)
MomentCumulantInversion 6 core · 8 supporting Cumulants 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 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.
That triangularity 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 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)
8 supporting declarations (lemmas, instances)
-
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, 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, ← 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 unfold cumFromMom 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
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 prescribed vector of cumulants of orders zero through L, the zero-padded cumulant sequence agrees with that vector through order L and equals zero at every higher order.
Definition (Lean source)
For a nonnegative integer L and a prescribed vector of cumulants of orders zero through L, the cumulant-to-weights map first reconstructs the corresponding raw moments and then returns the symmetric-atom weights obtained by solving their Vandermonde moment-matching system.
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, 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_finset_sum 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 ★ truncatedMomentInterior
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.
References: Akhiezer (1965), The Classical Moment Problem; Curto–Fialkow (1991) on truncated moment problems and flat extensions; Schmüdgen (2017), The Moment Problem, Theorem 10.7.
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.