Skip to content

Bernoulli sampling lemma #1240

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.

Sign up for GitHub

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

Jump to bottom
Draft
hoheinzollern wants to merge 73 commits into
base: master
Choose a base branch
from
Draft

Bernoulli sampling lemma #1240

hoheinzollern wants to merge 73 commits into from

Conversation

@hoheinzollern
Copy link
Member

@hoheinzollern hoheinzollern commented Jun 7, 2024

Motivation for this change

Draft PR containing the Bernoulli sampling theorem

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

@affeldt-aist affeldt-aist mentioned this pull request Jun 7, 2024
Closed
2 tasks
@hoheinzollern hoheinzollern force-pushed the sampling branch 3 times, most recently from f3f5e5e to 97a84fd Compare November 13, 2024 16:44
@t6s
Copy link
Member

t6s commented Nov 14, 2024

(Can I push to this repository once I drop a comment here?)

@t6s t6s assigned t6s and unassigned t6s Nov 14, 2024
@t6s
Copy link
Member

t6s commented Nov 14, 2024

(nope)

@hoheinzollern hoheinzollern force-pushed the sampling branch 2 times, most recently from e9f8230 to 67a7d07 Compare November 15, 2024 11:30
@affeldt-aist affeldt-aist force-pushed the sampling branch 6 times, most recently from 206806e to add35c8 Compare December 4, 2024 09:35
@affeldt-aist affeldt-aist force-pushed the sampling branch 2 times, most recently from ba72adb to 8c33df2 Compare February 25, 2025 16:00
@affeldt-aist affeldt-aist mentioned this pull request Mar 17, 2025
Open
@hoheinzollern hoheinzollern force-pushed the sampling branch 2 times, most recently from e26434d to 2490231 Compare April 28, 2025 07:36
affeldt-aist and others added 5 commits May 2, 2025 14:11
@affeldt-aist
tentative definition of Lp-spaces
466ad81
@hoheinzollern @affeldt-aist
extended reals
4eda318 
- compilation, CI fixes
@CohenCyril @affeldt-aist
WIP
8b722e8
@hoheinzollern @affeldt-aist
norms
7e49d4b 
- lspace.v headers
@CohenCyril @affeldt-aist
ae improvements
0046487 
- making ae work as a filter
- Adding notations for ae
- generalizing ae_eq
hoheinzollern and others added 21 commits May 7, 2025 18:20
@hoheinzollern
one admit in bernoulli_trial_mmt_gen_fun
4dc4c5f
@affeldt-aist @hoheinzollern
integrable_sum_ord, integral_sum (wip)
ab2d37f
@hoheinzollern
independence of product
9808281 
- fixed admit on bernoulli_trial_mmt_gen_fun
- solved bernoulli_trial_mmt_gen_fun
@affeldt-aist @t6s @hoheinzollern
integral_mpro
ceec16c 
Co-authored-by: Takafumi Saikawa <[email protected]>
@affeldt-aist @hoheinzollern
move expectation of product out of Bernoulli section
e0d596b 
- exploit boolean RVs
- uncomment expectation_prod2
@hoheinzollern
attempt at product of random variables using pushforward
2eb1481 
- prod RVs
- alternative sampling formulation
@t6s @hoheinzollern
Lemma expR2_le8
1ea19df
@affeldt-aist @hoheinzollern
memo, renaming
4f4e745
@t6s @hoheinzollern
HARD part done
1881174
@affeldt-aist @hoheinzollern
splitting sampling_wip.v
85a85d7
@hoheinzollern
introduced type bernoulliRV
dcef898
@affeldt-aist @hoheinzollern
rm tuple_sum, tuple_prod
8060dc9
@affeldt-aist @hoheinzollern
bernoulli_trial -> bool_trial_value
6cd9524
@affeldt-aist @hoheinzollern
split the sampling theorem in two sections
72036d8 
- no mtuple anymore
@hoheinzollern
exp2_le8 simplified
11d4bab
@affeldt-aist @hoheinzollern
remove unused lemmas from probability.v
cbcf1ea
@t6s @hoheinzollern
analytical argument
5d1b43a 
- rename analytical arguments to xlnx_lbound_i01 and xlnx_lbound_i12
@hoheinzollern
progress
3664ed8 
- wip sampling
- start of product expectation
- qed expectation_prod_nondep
- product using lfun
@affeldt-aist @hoheinzollern
add integral_pushforward
2ea4490
@hoheinzollern
doc and nix
460b5b6 
- docs for sampling.v
- add overlay
- nix actions
@hoheinzollern
removing independence.v
6c08999
@affeldt-aist affeldt-aist mentioned this pull request May 12, 2025
Merged
2 tasks
@hoheinzollern hoheinzollern mentioned this pull request Jun 19, 2025
Open
@affeldt-aist affeldt-aist added the wontfix/merge 🚫 We wont fix this issue/merge this PR, we will close it soon label Jun 19, 2025
@affeldt-aist affeldt-aist mentioned this pull request Dec 22, 2025
Open
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

wontfix/merge 🚫 We wont fix this issue/merge this PR, we will close it soon

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@hoheinzollern @t6s @affeldt-aist @CohenCyril @proux01