Skip to content

[Merged by Bors] - chore(Probability): typeclass generalizations#24474

Closed
RemyDegenne wants to merge 5 commits intomasterfrom
RD_generalize
Closed

[Merged by Bors] - chore(Probability): typeclass generalizations#24474
RemyDegenne wants to merge 5 commits intomasterfrom
RD_generalize

Conversation

@RemyDegenne
Copy link
Copy Markdown
Contributor

These typeclass generalizations are extracted from a list generated by a linter written by @JovanGerb .
See #mathlib4 > Linter for generalizing type class hypotheses @ 💬


Open in Gitpod

@RemyDegenne RemyDegenne added the t-measure-probability Measure theory / Probability theory label Apr 30, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 30, 2025

PR summary 6bbde83575

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

++-- inv

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).

Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks innocuous (and good) - but as not a probability theorist, I'd like a more familiar user's opinion.

Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+
Thanks!

Comment thread Mathlib/Probability/StrongLaw.lean Outdated
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 2, 2025

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 2, 2025
@RemyDegenne
Copy link
Copy Markdown
Contributor Author

bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label May 2, 2025
mathlib-bors bot pushed a commit that referenced this pull request May 2, 2025
These typeclass generalizations are extracted from a list generated by a linter written by @JovanGerb .
See [#mathlib4 > Linter for generalizing type class hypotheses @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Linter.20for.20generalizing.20type.20class.20hypotheses/near/507247536)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 2, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Probability): typeclass generalizations [Merged by Bors] - chore(Probability): typeclass generalizations May 2, 2025
@mathlib-bors mathlib-bors bot closed this May 2, 2025
@mathlib-bors mathlib-bors bot deleted the RD_generalize branch May 2, 2025 17:36
pfaffelh pushed a commit that referenced this pull request May 2, 2025
These typeclass generalizations are extracted from a list generated by a linter written by @JovanGerb .
See [#mathlib4 > Linter for generalizing type class hypotheses @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Linter.20for.20generalizing.20type.20class.20hypotheses/near/507247536)
riccardobrasca pushed a commit that referenced this pull request May 7, 2025
These typeclass generalizations are extracted from a list generated by a linter written by @JovanGerb .
See [#mathlib4 > Linter for generalizing type class hypotheses @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Linter.20for.20generalizing.20type.20class.20hypotheses/near/507247536)
tannerduve pushed a commit that referenced this pull request May 13, 2025
These typeclass generalizations are extracted from a list generated by a linter written by @JovanGerb .
See [#mathlib4 > Linter for generalizing type class hypotheses @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Linter.20for.20generalizing.20type.20class.20hypotheses/near/507247536)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants