Stat.Nonparametric.MomentProblems
Moment-problem substrate for nonparametric statistics: raw-moment algebra, L² projection residuals, constrained score programs, and sharp bounded-outcome residual envelopes.
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.
A probability law on the real line is a Gaussian law when it is a normal distribution: there is a mean and a (possibly zero) variance whose normal distribution is exactly this law. Allowing zero variance means the point masses (Diracs) count as degenerate Gaussians, so the negation "not a Gaussian law" is the strongest possible non-Gaussianity requirement.
Definition (Lean source)
The joint cumulant of two real random variables at bidegree (p, q): the cumulant of the first variable taken p times together with the second taken q times. It is obtained from the mixed moments by the classical set-partition (Möbius) inversion — sum over all partitions of the p + q slots of a signed factorial weight times the product, over the blocks of the partition, of the mixed moment matching how many first-variable and second-variable slots that block contains.
Definition (Lean source)
The cumulant of order r of a single real random variable: the joint cumulant of the variable with itself in which every slot is filled by that one variable. Order two is the variance, order three the centered third moment, order four the excess kurtosis.
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.
The order-r cumulant read off from a moment sequence: the set-partition (Möbius) formula that expresses the r-th cumulant as a signed, factorial-weighted sum over partitions of r slots of products of moments, one moment per block, at the block's size.
Definition (Lean source)
The lower-order remainder of the order-r cumulant formula: the same sum with the single one-block partition removed. Because every block of a multi-block partition is a proper subset, this depends only on moments of order strictly below r.
Definition (Lean source)
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)
The moment sequence reconstructed from a prescribed cumulant sequence, by inverting the triangular formula: total mass one, mean zero, and at each order at least two the moment is the prescribed cumulant minus the remainder assembled from the already-reconstructed lower 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.
The total weight that an indexed list of atoms places on a given point of the real line: the sum of the weights of all indices whose location is that point.
Definition (Lean source)
The finite atomic law determined by a list of real locations and a matching list of weights: the measure that puts each weight as a point mass at its own 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.
The L + 1 equally spaced symmetric atoms −L, −L + 2, …, L − 2, L: the i-th atom sits at twice i minus L. They are symmetric about the origin and pairwise distinct.
Definition (Lean source)
The uniform weight vector on the L + 1 atoms: each atom carries mass 1 / (L + 1).
Definition (Lean source)
The raw-moment sequence of the uniform-weight law on the symmetric atoms.
Definition (Lean source)
The cumulant sequence of the uniform-weight law on the symmetric atoms — the base point around which the truncated cumulant range is shown to have interior.
Definition (Lean source)
The Vandermonde matrix of the symmetric atoms: row i lists the powers of the i-th atom.
Definition (Lean source)
The weight vector solving the moment-matching system: given a target for the raw moments of orders 0 through L, the unique weights on the symmetric atoms reproducing them.
Definition (Lean source)
Extending a finite cumulant target of orders 0, …, L to a full sequence by zeros beyond order L.
Definition (Lean source)
The cumulant-to-weights map: from a prescribed truncated cumulant target, invert the triangular moment↔cumulant relation to get the target moments, then solve the Vandermonde system for the weights on the symmetric atoms.
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)
The base cumulant target: the cumulants, of orders 0 through L, of the uniform-weight 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 :ℕconclusion∀ i, 0 < 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)
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)
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.
Interior of the truncated cumulant range at order L. There is a cumulant target and a strictly positive radius such that every cumulant sequence within that radius of the target, in orders two through L, is realized by a probability law on the real line that is centered, is not a Gaussian law, and has finite L-th moment.
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.