Kernels#749

Draft

affeldt-aist wants to merge 34 commits intomath-comp:masterfrom

affeldt-aist:kernels

Commits on Mar 19, 2023

tentative definition of kernel
affeldt-aist
committed
tentative statement of lemma 3
affeldt-aist
committed
complete infinite sum of kernels is a kernel
affeldt-aist
committed
prove that star_kernel is a measure
affeldt-aist
committed
proposition 1
affeldt-aist
committed
tentative first part of lemma 3 (admit pending)
affeldt-aist
committed
complete lemma 3 and s-finite proofs
affeldt-aist
committed
nonneg 2/7

AyumuSaito
authored and
affeldt-aist
committed
s-finite kernels for ite and examples
affeldt-aist
committed
factorization of code, normalize, cleaning
affeldt-aist
committed
complete normalize, finite fubini, improve hier with pker
affeldt-aist
committed
more uniform naming, kdirac is pker, etc.
affeldt-aist
committed
mscore using mscale and dirac
affeldt-aist
committed
generalize mscoreE
affeldt-aist
committed
various minor simplifications and generalizations
affeldt-aist
committed
staton bus with exp
affeldt-aist
committed
wip (gauss)
affeldt-aist
committed
linearize hierarchy
affeldt-aist
committed
subprob kernel
affeldt-aist
committed
cleaning
affeldt-aist
committed
hard constraint example
affeldt-aist
committed
minor cleaning
affeldt-aist
committed
gen sample
affeldt-aist
committed
upd wrt master
affeldt-aist
committed
shorten measurable_fun_kprobability
affeldt-aist
committed
upd with recent PRs
affeldt-aist
committed
use reversible coercions
affeldt-aist
committed
upd wrt recent PRs, compat with Coq 8.15
affeldt-aist
committed
simple example
affeldt-aist
committed
letinA
affeldt-aist
committed
minor cleaning
affeldt-aist
committed
rebase wrt branch on finite measures
affeldt-aist
committed
adapt to hierarchy with subprob
affeldt-aist
committed
upd
affeldt-aist
committed