10 Pull requests merged by 4 people

• preimage_set_system lemmas

  #1524 merged Mar 13, 2025

• integral of (1 + x^2)^-1 over [0, +oo[

  #1492 merged Mar 12, 2025

• generalize measurable_funP, integral_pushforward and similar lemmas

  #1522 merged Mar 12, 2025

• replace some `|Num.floor _|%N with Num.trunc _

  #1432 merged Mar 11, 2025

• Mark a few lemmas as available in MC 2.3

  #1521 merged Mar 11, 2025

• Simplify proof

  #1520 merged Mar 11, 2025

• Cleanup mathcomp_extra.v

  #1517 merged Mar 11, 2025

• Mark things as backported

  #1515 merged Mar 10, 2025

• Mark interval_inference.v as backported

  #1516 merged Mar 10, 2025

• fix lemma dependency on local hypothesis

  #1511 merged Mar 8, 2025

1 Issue closed by 1 person

• What `D` in `measurable_fun D f` is useful for?

  #1519 closed Mar 12, 2025

5 Issues opened by 4 people

• Revise the occurrences of `|Num.floor _|%N

  #1523 opened Mar 11, 2025

• measurable_sfunP does not refer to sfun

  #1518 opened Mar 11, 2025

• Rename "prod" to "pair" to avoid confusion with "\prod"?

  #1514 opened Mar 10, 2025

• Documentation content background not expanding outside the visible frame

  #1513 opened Mar 10, 2025

• Poor image contrast in dark mode for html-rendered documentation

  #1512 opened Mar 10, 2025

6 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• typo in the header of measure.v

  #1510 commented on Mar 11, 2025 • 0 new comments

• Application of s-finite kernels to program semantics

  #912 commented on Mar 12, 2025 • 0 new comments

• Bernoulli sampling lemma

  #1240 commented on Mar 12, 2025 • 0 new comments

• expectation of product

  #1391 commented on Mar 11, 2025 • 0 new comments

• finite transition kernels

  #1444 commented on Mar 12, 2025 • 0 new comments

• define cdf (cumulative distributive function)

  #1502 commented on Mar 10, 2025 • 0 new comments