Skip to content

Conversation

@affeldt-aist
Copy link
Member

Motivation for this change

this is an easy part of PR #1391

basically it replaces the lemma approximation (an existential statement)
into an explicit construction of its witness (because it is used in the proof of the expectation of a product)

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 requested a review from t6s December 3, 2024 06:48
@affeldt-aist affeldt-aist added this to the 1.8.0 milestone Dec 3, 2024
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Dec 3, 2024
Copy link
Member

@t6s t6s left a comment

Choose a reason for hiding this comment

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

Looks good in general. I can point out only a few naming issues.

@affeldt-aist affeldt-aist force-pushed the lebesgue_integral_20241203 branch from 84ff007 to 13ecdb6 Compare December 3, 2024 14:27
@affeldt-aist affeldt-aist merged commit 2b0ae21 into math-comp:master Dec 3, 2024
28 of 31 checks passed
@affeldt-aist affeldt-aist deleted the lebesgue_integral_20241203 branch December 3, 2024 14:53
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