Skip to content

normal_prob cont./reproductive property#1955

Merged
affeldt-aist merged 6 commits into
math-comp:masterfrom
affeldt-aist:normal_20260426
Jun 29, 2026
Merged

normal_prob cont./reproductive property#1955
affeldt-aist merged 6 commits into
math-comp:masterfrom
affeldt-aist:normal_20260426

Conversation

@affeldt-aist

@affeldt-aist affeldt-aist commented Apr 27, 2026

Copy link
Copy Markdown
Member
Motivation for this change

This PR provides a proof of the continuity of normal_prob and of the reproductive
property of normal distribution:
Screenshot 2026-04-27 at 11 00 37

This is taken from the PR #1712
and it relies on the field tactic (fyi: @proux01 )

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

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist added this to the 1.17.0 milestone Apr 27, 2026
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Apr 27, 2026

@IshiguroYoshihiro IshiguroYoshihiro left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

It looks good for me.
I think there is some room for generalization on auxiliary lemmas, but I don't think it need to block this PR.

Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v
@affeldt-aist

Copy link
Copy Markdown
Member Author

@IshiguroYoshihiro Thank you very much for the comments!

@affeldt-aist affeldt-aist merged commit 40abdc2 into math-comp:master Jun 29, 2026
45 checks passed
Brixfoly pushed a commit to Brixfoly/analysis that referenced this pull request Jun 30, 2026
* normal_prob cont./reproductive property

---------

Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants