List view

pseudometric alias

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

Status: Merged (completed).

math-comp/analysisnumber 1628

#1628 In math-comp/analysis;

· by affeldt-aist was closed on Jun 5, 2025

exponential distribution

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

Status: Merged (completed).

math-comp/analysisnumber 1635

#1635 In math-comp/analysis;

· by affeldt-aist was closed on Jun 5, 2025

is_deriveX: is that a generalization?

question ❓There is an unanswered question hereThere is an unanswered question here

Status: Merged (completed).

math-comp/analysisnumber 1637

#1637 In math-comp/analysis;

· by affeldt-aist was closed on Jun 5, 2025

fixes #1632

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Merged (completed).

math-comp/analysisnumber 1633

#1633 In math-comp/analysis;

· by affeldt-aist was closed on May 26, 2025

add variant of Fubini lemmas and rename to clarify

Status: Merged (completed).

math-comp/analysisnumber 1651

#1651 In math-comp/analysis;

· by affeldt-aist was closed on Jul 1, 2025

alternative proof of gauss integral

Status: Closed (abandoned).

math-comp/analysisnumber 1584

#1584 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Jun 20, 2025

fixes #1463

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Merged (completed).

math-comp/analysisnumber 1663

#1663 In math-comp/analysis;

· by affeldt-aist was closed on Jul 1, 2025

integral_sum and fix integrable_sum

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

Status: Merged (completed).

math-comp/analysisnumber 1650

#1650 In math-comp/analysis;

· by affeldt-aist was closed on Jun 26, 2025

Lfun1_integrable turned into an equivalence

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

Status: Merged (completed).

math-comp/analysisnumber 1655

#1655 In math-comp/analysis;

· by affeldt-aist was closed on Jun 26, 2025

adapt to rocq-prover/rocq#20707

Status: Merged (completed).

math-comp/analysisnumber 1641

#1641 In math-comp/analysis;

· by gares was closed on Jun 27, 2025

ports from the sampling branch

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

Status: Merged (completed).

math-comp/analysisnumber 1657

#1657 In math-comp/analysis;

· by affeldt-aist was closed on Jun 28, 2025

fixes #1659

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Merged (completed).

math-comp/analysisnumber 1660

#1660 In math-comp/analysis;

· by affeldt-aist was closed on Jun 28, 2025

lemma generalization

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

Status: Merged (completed).

math-comp/analysisnumber 1648

#1648 In math-comp/analysis;

· by affeldt-aist was closed on Jun 24, 2025

almost everywhere equality

Status: Merged (completed).

math-comp/analysisnumber 1600

#1600 In math-comp/analysis;

· by hoheinzollern was closed on May 12, 2025

ereal inverse + simplification mule and mule_def

Status: Merged (completed).

math-comp/analysisnumber 1494

#1494 In math-comp/analysis;

· by CohenCyril was closed on Jun 3, 2025

expR_ge1Dxn

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

Status: Merged (completed).

math-comp/analysisnumber 1638

#1638 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Jun 14, 2025

measurability for tuples

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

Status: Merged (completed).

math-comp/analysisnumber 1618

#1618 In math-comp/analysis;

· by affeldt-aist was closed on Jun 17, 2025

lemmas for integrals on increasing set sequences

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

Status: Merged (completed).

math-comp/analysisnumber 1579

#1579 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Jun 17, 2025

instead of lspace_master

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

Status: Merged (completed).

math-comp/analysisnumber 1624

#1624 In math-comp/analysis;

· by affeldt-aist was closed on Jun 19, 2025

Lspace master

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

Status: Closed (abandoned).

math-comp/analysisnumber 1506

#1506 In math-comp/analysis;

· by affeldt-aist was closed on Jun 19, 2025

Add section: cdf of lebesgue stieltjes measure

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

Status: Merged (completed).

math-comp/analysisnumber 1639

#1639 In math-comp/analysis;

· by Yosuke-Ito-345 was closed on Jul 3, 2025

Cleanup

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Merged (completed).

math-comp/analysisnumber 1567

#1567 In math-comp/analysis;

· by pi8027 was closed on Jul 2, 2025

Conv convention

Status: Merged (completed).

math-comp/analysisnumber 1630

#1630 In math-comp/analysis;

· by t6s was closed on May 29, 2025

name: cvgeMl -> cvgeMr?

question ❓There is an unanswered question hereThere is an unanswered question here

Status: Closed (completed).

#1463 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Jul 1, 2025

Implicit argument of probability_setT

Status: Closed (completed).

#1653 In math-comp/analysis;

· by affeldt-aist was closed on Jun 26, 2025