Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Kernels #749

Draft
wants to merge 34 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
3fff13d
tentative definition of kernel
affeldt-aist Jun 8, 2022
a35425c
tentative statement of lemma 3
affeldt-aist Jun 15, 2022
7b18cf1
complete infinite sum of kernels is a kernel
affeldt-aist Jun 22, 2022
e13c58f
prove that star_kernel is a measure
affeldt-aist Jun 22, 2022
0bfaf8a
proposition 1
affeldt-aist Jun 22, 2022
9de2757
tentative first part of lemma 3 (admit pending)
affeldt-aist Jul 11, 2022
cbd871c
complete lemma 3 and s-finite proofs
affeldt-aist Jul 22, 2022
c8e2268
nonneg 2/7
AyumuSaito Aug 8, 2022
29fc0f6
s-finite kernels for ite and examples
affeldt-aist Aug 8, 2022
477fcdd
factorization of code, normalize, cleaning
affeldt-aist Aug 18, 2022
259df8e
complete normalize, finite fubini, improve hier with pker
affeldt-aist Aug 19, 2022
061ad30
more uniform naming, kdirac is pker, etc.
affeldt-aist Aug 24, 2022
39b4d78
mscore using mscale and dirac
affeldt-aist Sep 1, 2022
c6901eb
generalize mscoreE
affeldt-aist Sep 2, 2022
42a2b9d
various minor simplifications and generalizations
affeldt-aist Sep 8, 2022
21eaa02
staton bus with exp
affeldt-aist Sep 13, 2022
8bbb9c9
wip (gauss)
affeldt-aist Sep 14, 2022
4833142
linearize hierarchy
affeldt-aist Sep 16, 2022
334ddba
subprob kernel
affeldt-aist Sep 17, 2022
c355470
cleaning
affeldt-aist Sep 21, 2022
d6f46b7
hard constraint example
affeldt-aist Sep 21, 2022
e8286be
minor cleaning
affeldt-aist Sep 22, 2022
8c8c018
gen sample
affeldt-aist Oct 7, 2022
0702f74
upd wrt master
affeldt-aist Oct 26, 2022
ac875e7
shorten measurable_fun_kprobability
affeldt-aist Oct 26, 2022
f34d6f1
upd with recent PRs
affeldt-aist Nov 15, 2022
78732a0
use reversible coercions
affeldt-aist Dec 12, 2022
f2103df
upd wrt recent PRs, compat with Coq 8.15
affeldt-aist Jan 9, 2023
c4768fa
simple example
affeldt-aist Jan 10, 2023
1b80f0e
letinA
affeldt-aist Jan 16, 2023
201f20d
minor cleaning
affeldt-aist Jan 17, 2023
e6dc481
rebase wrt branch on finite measures
affeldt-aist Feb 6, 2023
a241ec4
adapt to hierarchy with subprob
affeldt-aist Feb 12, 2023
f7e5826
upd
affeldt-aist Feb 22, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,9 @@ theories/derive.v
theories/measure.v
theories/numfun.v
theories/lebesgue_integral.v
theories/kernel.v
theories/prob_lang.v
theories/wip.v
theories/summability.v
theories/signed.v
theories/itv.v
Expand Down
Loading