[Merged by Bors] - feat(Probability/Kernel): disintegration of finite kernels #10603
Conversation
This file contains 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
RemyDegenne
added
WIP
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
Outdated
Show resolved
Hide resolved
RemyDegenne
added
awaiting-review
|
The refactor is done and this is ready for review. The PR is big, but if I dismantle the old disintegration file I have to have all the replacements in the PR (which means I can't PR the files about integrals and uniqueness later). |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
added
merge-conflict
sgouezel
reviewed
Apr 16, 2024
| This theorem in the case of finite kernels is weaker than `eq_condKernel_of_measure_eq_compProd` | ||
| which asserts that the kernels are equal almost everywhere and not just on a given measurable | ||
| set. -/ | ||
| theorem eq_condKernel_of_measure_eq_compProd' (κ : kernel α Ω) [IsSFiniteKernel κ] |
There was a problem hiding this comment.
I think I am unhappy with the assumptions in this theorem and in the next ones: if ρ = ρ.fst ⊗ₘ κ and ρ is a finite measure, then κ a should have finite mass almost everywhere wrt ρ.fst, and I feel that this should be sufficient to carry out the arguments in the lemma without the assumptions of s-finiteness or of finiteness. However, the lemmas were already there (at least in the measure version) and you just copied them, so this shouldn't hold the PR back. I'll investigate that once this one is merged, if you agree.
|
✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
leanprover-community-mathlib4-bot
removed
the
merge-conflict
RemyDegenne
added
delegated
and removed
awaiting-review
|
Thanks for all the reviews and for your help on the disintegration PRs. No worries about the review time: I don't expect a quick review for a 1000 lines PR :) bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 16, 2024
Let `κ : kernel α (β × Ω)` be a finite kernel, where `Ω` is a standard Borel space. Then if `α` is countable or `β` has a countably generated σ-algebra (for example if it is standard Borel), then there exists a `kernel (α × β) Ω` called conditional kernel and denoted by `condKernel κ` such that `κ = fst κ ⊗ₖ condKernel κ`. Properties of integrals involving `condKernel` are collated in the file `Integral.lean`. The conditional kernel is unique (almost everywhere w.r.t. `fst κ`): this is proved in the file `Unique.lean`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
Let `κ : kernel α (β × Ω)` be a finite kernel, where `Ω` is a standard Borel space. Then if `α` is countable or `β` has a countably generated σ-algebra (for example if it is standard Borel), then there exists a `kernel (α × β) Ω` called conditional kernel and denoted by `condKernel κ` such that `κ = fst κ ⊗ₖ condKernel κ`. Properties of integrals involving `condKernel` are collated in the file `Integral.lean`. The conditional kernel is unique (almost everywhere w.r.t. `fst κ`): this is proved in the file `Unique.lean`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
Let `κ : kernel α (β × Ω)` be a finite kernel, where `Ω` is a standard Borel space. Then if `α` is countable or `β` has a countably generated σ-algebra (for example if it is standard Borel), then there exists a `kernel (α × β) Ω` called conditional kernel and denoted by `condKernel κ` such that `κ = fst κ ⊗ₖ condKernel κ`. Properties of integrals involving `condKernel` are collated in the file `Integral.lean`. The conditional kernel is unique (almost everywhere w.r.t. `fst κ`): this is proved in the file `Unique.lean`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
Let `κ : kernel α (β × Ω)` be a finite kernel, where `Ω` is a standard Borel space. Then if `α` is countable or `β` has a countably generated σ-algebra (for example if it is standard Borel), then there exists a `kernel (α × β) Ω` called conditional kernel and denoted by `condKernel κ` such that `κ = fst κ ⊗ₖ condKernel κ`. Properties of integrals involving `condKernel` are collated in the file `Integral.lean`. The conditional kernel is unique (almost everywhere w.r.t. `fst κ`): this is proved in the file `Unique.lean`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Jun2M
pushed a commit
that referenced
this pull request
Apr 24, 2024
Let `κ : kernel α (β × Ω)` be a finite kernel, where `Ω` is a standard Borel space. Then if `α` is countable or `β` has a countably generated σ-algebra (for example if it is standard Borel), then there exists a `kernel (α × β) Ω` called conditional kernel and denoted by `condKernel κ` such that `κ = fst κ ⊗ₖ condKernel κ`. Properties of integrals involving `condKernel` are collated in the file `Integral.lean`. The conditional kernel is unique (almost everywhere w.r.t. `fst κ`): this is proved in the file `Unique.lean`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Let
κ : kernel α (β × Ω)be a finite kernel, whereΩis a standard Borel space. Then ifαis countable orβhas a countably generated σ-algebra (for example if it is standard Borel), then there exists akernel (α × β) Ωcalled conditional kernel and denoted bycondKernel κsuch thatκ = fst κ ⊗ₖ condKernel κ.Properties of integrals involving
condKernelare collated in the fileIntegral.lean.The conditional kernel is unique (almost everywhere w.r.t.
fst κ): this is proved in the fileUnique.lean.