Skip to content

feat: a sum of independent Bernoulli random variables is a binomial random variable - #37794

Open
EtienneC30 wants to merge 103 commits into
leanprover-community:masterfrom
EtienneC30:ber_bin
Open

feat: a sum of independent Bernoulli random variables is a binomial random variable#37794
EtienneC30 wants to merge 103 commits into
leanprover-community:masterfrom
EtienneC30:ber_bin

Conversation

@EtienneC30

@EtienneC30 EtienneC30 commented Apr 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

EtienneC30 added 30 commits April 2, 2026 10:04
@EtienneC30
feat: integral of the binomial distribution
d1e6ff2
@EtienneC30
wip
fa5b4c1
@EtienneC30
feat: cardinality of subsets of a given cardinality
bf05a43
@EtienneC30
naming
46e0488
@EtienneC30
Merge branch 'powersetncard' into binomial
609eac9
@EtienneC30
fix linter
d705029
@EtienneC30
feat: another version of the cardinality of the difference
ba9d68f
@EtienneC30
Merge branch 'ncard_diff' into binomial
6c9794f
@EtienneC30
wip
8266ae6
@EtienneC30
feat: lemmas related to setBernoulli
33a6e82
@EtienneC30
Merge branch 'setBer' into binomial
8433256
@EtienneC30
wip
8094db3
@EtienneC30
feat: any set is pairwise disjoint under the singleton function
1271cd4
@EtienneC30
Merge branch 'pd_singleton' into binomial
daff212
@EtienneC30
wip
7cd46f1
@EtienneC30
Merge branch 'master' of https://github.com/leanprover-community/math…
1330b7f 
…lib4 into binomial
@EtienneC30
cleanup
d218f9c
@EtienneC30
move
fdd50af
@EtienneC30
feat: mapping a finite sum of measures
2c032a5
@EtienneC30
Merge branch 'map_sum' into binomial2
e51c08f
@EtienneC30
deprecate PMF.binomial
5c6c767
@EtienneC30
same
0db5b97
@EtienneC30
lint
a83ff5c
@EtienneC30
feat: define Bernoulli distribution
150012a
@EtienneC30
feat: scalar multiplication of an NNReal against 1 : ENNReal
3093c5c
@EtienneC30
fix
554f5be
@EtienneC30
remove set_option
57cf556
@EtienneC30
Merge branch 'smul_one' into bernoulli
0fd281b
@EtienneC30
useless lemma
f665b84
@EtienneC30
mk_all
1fa2e9b
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 11, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented Jun 11, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@EtienneC30 EtienneC30 mentioned this pull request Jul 2, 2026
Open
1 task
@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2026
@mathlib-dependent-issues mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 3, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 17, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented Jul 17, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@CoolRmal CoolRmal mentioned this pull request Aug 12, 2026
Closed
@github-actions github-actions Bot 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 12, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented Aug 14, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts Bot 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 14, 2026
@github-actions github-actions Bot 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 19, 2026
@EtienneC30 EtienneC30 mentioned this pull request Aug 21, 2026
Open
2 tasks
@EtienneC30
EtienneC30 marked this pull request as ready for review August 21, 2026 08:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@EtienneC30