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

Add kl_compProd and relevant lemmas, update blueprint, refactor some variables #4

Merged
merged 94 commits into from
Apr 25, 2024

Conversation

LorenzoLuccioli
Copy link
Collaborator

@LorenzoLuccioli LorenzoLuccioli commented Apr 5, 2024

Add the statement and proof of kl_compProd, which is the chain rule for conditional KL divergence, add some lemmas useful to prove it in separate files, update the blueprint. Change the notation of some variables, in particular make sure that the variables in \alpha are called 'a' and not 'x' for consistency.

@RemyDegenne RemyDegenne added the awaiting-author Changes have being requested label Apr 5, 2024
@RemyDegenne
Copy link
Owner

Can you merge the main repository into this branch, to reduce the diff?

@LorenzoLuccioli LorenzoLuccioli changed the title Add conditional KL divergence and statement of chain rule (kernel version) Add kl_compProd and relevant lemmas, update blueprint, refactor some variables Apr 16, 2024
@LorenzoLuccioli LorenzoLuccioli added awaiting-review Ready to be reviewed and removed awaiting-author Changes have being requested labels Apr 16, 2024
TestingLowerBounds/ForMathlib/L1Space.lean Outdated Show resolved Hide resolved
TestingLowerBounds/ForMathlib/L1Space.lean Outdated Show resolved Hide resolved
TestingLowerBounds/ForMathlib/RnDeriv.lean Outdated Show resolved Hide resolved
TestingLowerBounds/ForMathlib/RnDeriv.lean Outdated Show resolved Hide resolved
TestingLowerBounds/KullbackLeibler.lean Outdated Show resolved Hide resolved
TestingLowerBounds/KullbackLeibler.lean Outdated Show resolved Hide resolved
TestingLowerBounds/KullbackLeibler.lean Outdated Show resolved Hide resolved
blueprint/src/sections/kl_divergence.tex Outdated Show resolved Hide resolved
TestingLowerBounds/KullbackLeibler.lean Show resolved Hide resolved
@RemyDegenne RemyDegenne added awaiting-author Changes have being requested and removed awaiting-review Ready to be reviewed labels Apr 18, 2024
@LorenzoLuccioli LorenzoLuccioli added awaiting-review Ready to be reviewed and removed awaiting-author Changes have being requested labels Apr 18, 2024
@RemyDegenne RemyDegenne merged commit 0f64f1a into RemyDegenne:master Apr 25, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-review Ready to be reviewed
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants