feat: Schoenberg helpers + ConvolutionSemigroup structure#3
Merged
Conversation
Fix sign error in schoenberg_exp_of_cnd to match the project's CND convention (form >= 0 for zero-sum weights). With this convention, exp(t*psi) is PD, not exp(-t*psi). Add five fully proved helper lemmas for positive definite functions: - isPositiveDefinite_one (constant 1 is PD) - isPositiveDefinite_smul (nonneg scalar * PD is PD) - isPositiveDefinite_pow (PD^k is PD via Schur product) - isPositiveDefinite_add (sum of PD is PD) - isPositiveDefinite_exp_mul_sub_one (exp(t(phi-1)) is PD) Update downstream levyKhintchine_of_cnd for corrected sign.
Define ConvolutionSemigroup structure capturing the family {μ_t} of
probability measures with charFun(μ_t)(ξ) = exp(t·ψ(ξ)). Prove the
semigroup law (charFun_mul) and construct the semigroup from a CND
exponent via Schoenberg + Bochner (convolutionSemigroupOfCND).
Refactor levyKhintchine_of_cnd to use the semigroup structure,
isolating the remaining sorry to the measure differentiation step
(extracting the Lévy triple from the semigroup at t→0).
slink
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Commit 1 (Unit C): Fix sign convention in
schoenberg_exp_of_cndand add 5 helper lemmasexp(t*ψ)is PD (notexp(-t*ψ)) matching project's CND conventionisPositiveDefinite_one,_smul,_pow,_add,_exp_mul_sub_one(all fully proved)Commit 2 (Unit E): Add
ConvolutionSemigroupstructureConvolutionSemigroupcapturing{μ_t}withcharFun(μ_t)(ξ) = exp(t·ψ(ξ))charFun_mul)convolutionSemigroupOfCND)levyKhintchine_of_cndto use semigroup, isolating sorry to measure differentiationSorry audit
schoenberg_exp_of_cnd(line 647) — needs PSD matrix characterizationlevyKhintchine_of_cnd(line 737) — measure differentiation (research-level)Test plan
lake buildsucceeds (full project, 6148 jobs)