[Merged by Bors] - feat(Probability/Kernel): `Kernel.sectL` and `sectR` by LorenzoLuccioli · Pull Request #15466 · leanprover-community/mathlib4

LorenzoLuccioli · 2024-08-03T15:27:43Z

Define a Kernel α γ and a Kernel β γ from a Kernel (α × β) γ by taking the comap of fun a ↦ (a, b) and fun b ↦ (a, b) respectively.

Add definitions of Kernel.sectL and Kernel.sectR.
Add some API lemmas: sectL_apply, sectL_zero, comap_sectL, sectL_prodMkLeft, sectL_prodMkRight and the equivalent lemmas for sectR.
Add instances for IsMarkovKernel, IsFiniteKernel, IsSFiniteKernel and NeZero.
Add sectL_swapRight and sectR_swapRight.
Add compProd_apply_eq_compProd_sectR.

github-actions · 2024-08-03T15:28:20Z

PR summary 3c46787a4d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR
+ comap_sectL
+ comap_sectR
+ instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectL κ b)] :
+ instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectR κ b)] :
+ instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectL κ b) a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectR κ a) b) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (sectR κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (sectR κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (sectR κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] :
+ instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (sectL κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (sectL κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (sectL κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsZeroOrMarkovKernel κ] :
+ sectL
+ sectL_apply
+ sectL_prodMkLeft
+ sectL_prodMkRight
+ sectL_swapRight
+ sectL_zero
+ sectR
+ sectR_apply
+ sectR_prodMkLeft
+ sectR_prodMkRight
+ sectR_swapRight
+ sectR_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

LorenzoLuccioli · 2024-08-03T15:29:36Z

The names are Kernel.fst' and Kernel.snd', since Kernel.fst and Kernel.snd are already taken for the case where the codomain is a product space. Suggestions for a better name are welcome.

urkud · 2024-09-05T07:08:05Z

About names: there are Function.Embedding.sectl and MonoidHom.inl. Probably, the former is closer to this case. Also, please ask on Zulip for other suggestions.

Mathlib/Probability/Kernel/Composition.lean

YaelDillies · 2024-11-12T11:15:49Z

Can you please update the PR description?

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2024-11-17T09:32:18Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Mathlib/Probability/Kernel/Composition.lean

… and `sectR`

YaelDillies · 2025-01-04T21:37:30Z

Looks like this is ready to be merged again?

maintainer merge

github-actions · 2025-01-04T21:37:52Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

RemyDegenne · 2025-01-07T16:44:48Z

bors r+

Define a `Kernel α γ` and a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` and `fun b ↦ (a, b)` respectively. - Add definitions of `Kernel.sectL` and `Kernel.sectR`. - Add some API lemmas: `sectL_apply`, `sectL_zero`, `comap_sectL`, `sectL_prodMkLeft`, `sectL_prodMkRight` and the equivalent lemmas for `sectR`. - Add instances for `IsMarkovKernel`, `IsFiniteKernel`, `IsSFiniteKernel` and `NeZero`. - Add `sectL_swapRight` and `sectR_swapRight`. - Add `compProd_apply_eq_compProd_sectR`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Remy Degenne <remydegenne@gmail.com>

mathlib-bors · 2025-01-07T16:54:34Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (642 commits) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) feat(Analysis/Analytic): lemmas about `smul` for power series (#19816) chore: don't import algebra in `Data.Multiset.Basic` (#19775) ...

* origin/master: (80 commits) chore(CategoryTheory): remove data produced by tactic block (#20565) feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) ...

LorenzoLuccioli added 2 commits August 3, 2024 17:04

apply changes

852453f

Add compProd_apply_eq_compProd_snd'

573979c

LorenzoLuccioli added the t-measure-probability Measure theory / Probability theory label Aug 3, 2024

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 17, 2024

Merge branch 'master' into LL/KernelFst'Snd'

e9a8eda

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 17, 2024

Merge branch 'master' into LL/KernelFst'Snd'

61c817e

YaelDillies reviewed Oct 31, 2024

View reviewed changes

Mathlib/Probability/Kernel/Composition.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 31, 2024

rename Fst' and Snd' to domFst and domSnd

8a3e826

LorenzoLuccioli removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 8, 2024

LorenzoLuccioli added 3 commits November 8, 2024 01:15

fix bug

f0770e5

fix lint warning

30ec8f8

rename Fst to sectl and Snd to sectr

3d13c57

YaelDillies changed the title ~~feat (Probability.Kernel): Add definitions and API for Kernel.fst' and snd'~~ feat(Probability/Kernel): Add definitions and API for Kernel.sectl and sectr Nov 12, 2024

change sectl and sectr to sectL and sectR

904d9e3

YaelDillies changed the title ~~feat(Probability/Kernel): Add definitions and API for Kernel.sectl and sectr~~ feat(Probability/Kernel): Add definitions and API for Kernel.sectL and sectR Nov 17, 2024

YaelDillies changed the title ~~feat(Probability/Kernel): Add definitions and API for Kernel.sectL and sectR~~ feat(Probability/Kernel): Kernel.sectL and sectR Nov 17, 2024

YaelDillies approved these changes Nov 17, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 17, 2024

sgouezel reviewed Nov 18, 2024

View reviewed changes

Mathlib/Probability/Kernel/Composition.lean Show resolved Hide resolved

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Nov 18, 2024

LorenzoLuccioli added 2 commits November 21, 2024 16:25

add IsZeroOrMarkovKernel.comap

1ca0764

apply suggestion: add instances of IsZeroOrMarkovKernel for sectL…

856d1fb

… and `sectR`

LorenzoLuccioli removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 26, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 5, 2024

RemyDegenne added 2 commits January 3, 2025 09:18

Merge remote-tracking branch 'origin/master' into LL/KernelFst'Snd'

1976dc3

fix

3c46787

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 3, 2025

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 4, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 7, 2025

mathlib-bors bot changed the title ~~feat(Probability/Kernel): Kernel.sectL and sectR~~ [Merged by Bors] - feat(Probability/Kernel): Kernel.sectL and sectR Jan 7, 2025

mathlib-bors bot closed this Jan 7, 2025

mathlib-bors bot deleted the LL/KernelFst'Snd' branch January 7, 2025 16:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Probability/Kernel): `Kernel.sectL` and `sectR`#15466

[Merged by Bors] - feat(Probability/Kernel): `Kernel.sectL` and `sectR`#15466
LorenzoLuccioli wants to merge 13 commits intomasterfrom
LL/KernelFst'Snd'

LorenzoLuccioli commented Aug 3, 2024 •

edited by YaelDillies

Loading

Uh oh!

github-actions bot commented Aug 3, 2024 •

edited

Loading

Declarations diff

Uh oh!

LorenzoLuccioli commented Aug 3, 2024

Uh oh!

urkud commented Sep 5, 2024

Uh oh!

Uh oh!

YaelDillies commented Nov 12, 2024

Uh oh!

YaelDillies left a comment

Uh oh!

github-actions bot commented Nov 17, 2024

Uh oh!

Uh oh!

YaelDillies commented Jan 4, 2025

Uh oh!

github-actions bot commented Jan 4, 2025

Uh oh!

RemyDegenne commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

LorenzoLuccioli commented Aug 3, 2024 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 3, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3c46787a4d

Import changes for modified files

Declarations diff

Uh oh!

LorenzoLuccioli commented Aug 3, 2024

Uh oh!

urkud commented Sep 5, 2024

Uh oh!

Uh oh!

YaelDillies commented Nov 12, 2024

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Nov 17, 2024

Uh oh!

Uh oh!

YaelDillies commented Jan 4, 2025

Uh oh!

github-actions bot commented Jan 4, 2025

Uh oh!

RemyDegenne commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

LorenzoLuccioli commented Aug 3, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Aug 3, 2024 •

edited

Loading