1.20.0

New issue

Open

Due by November 27, 2026

•Last updated Nov 11, 2026

11% complete

Organization of the files in lebesgue_integral_theory
math-comp/analysis#1549 · opened on Apr 2, 2025 · 1.20.0
Redundancies between realseq.v and sequences.v
math-comp/analysis#255 · opened on Sep 4, 2020 · 1.20.0
4
WIP: eudoxus reals
Unread
#116 opened Oct 17, 2018 · Updated Oct 1, 2026Draft
4
move dyadic intervals in a more appropriate file
math-comp/analysis#1553 · opened on Apr 2, 2025 · 1.20.0
Put iavg in its own file
math-comp/analysis#1555 · opened on Apr 2, 2025 · 1.20.0
1
move the product measure out of lebesgue_integral_fubini.v
math-comp/analysis#1554 · opened on Apr 2, 2025 · 1.20.0
CPOs (wip)
Unread
#1807 opened Dec 22, 2025 · Updated Oct 1, 2026Draft
Fundamental Theorem of Calculus
math-comp/analysis#965 · opened on Jun 27, 2023 · 1.20.0
improve the documentation of contra.v
math-comp/analysis#1197 · opened on Mar 28, 2024 · 1.20.0
funrpos and funepos should be factorized
math-comp/analysis#1903 · opened on Mar 15, 2026 · 1.20.0
2
max is a monoid operator
math-comp/analysis#2093 · opened on Aug 27, 2026 · 1.20.0
Document the sub-directories of theories
math-comp/analysis#1550 · opened on Apr 2, 2025 · 1.20.0
Split probability.v into a directory probability_theory
math-comp/analysis#1808 · opened on Dec 22, 2025 · 1.20.0
4
introduce {within [a, b], derivable f} or/and "differentiable from the right/left at a/b"
math-comp/analysis#904 · opened on Apr 20, 2023 · 1.20.0
redefine distr using esum and lebesgue
Unread
#1952 opened Apr 25, 2026 · Updated Oct 1, 2026Draft
Initial topology induced by a family of functions
Unread
#2003 opened Jun 21, 2026 · Updated Oct 1, 2026
4
Holomorphy
Unread
#2001 opened Jun 17, 2026 · Updated Oct 1, 2026
1
naming in classical_sets conflicts with fintype
math-comp/analysis#274 · opened on Nov 9, 2020 · 1.20.0
1
put together statements about ]x-r,x+r[
math-comp/analysis#1084 · opened on Nov 9, 2023 · 1.20.0
Add closed sets to topological mixin
math-comp/analysis#134 · opened on Mar 1, 2019 · 1.20.0
3
candidate lemma for a PR (bounded, lee_sum, nneseries)
math-comp/analysis#1530 · opened on Mar 17, 2025 · 1.20.0
1
Solve slowdown in derive
math-comp/analysis#118 · opened on Oct 30, 2018 · 1.20.0
TODO: rename pseudometric
math-comp/analysis#1990 · opened on Jun 9, 2026 · 1.20.0
9
the Gamma function
Unread
#1762 opened Nov 18, 2025 · Updated Oct 15, 2026
1
conv_gt0 as an instance of PosNum
math-comp/analysis#1009 · opened on Aug 11, 2023 · 1.20.0
2

Navigation Menu

1.20.0

Organization of the files in `lebesgue_integral_theory`

Redundancies between `realseq.v` and `sequences.v`

WIP: eudoxus reals

move dyadic intervals in a more appropriate file

Put `iavg` in its own file

move the product measure out of `lebesgue_integral_fubini.v`

CPOs (wip)

Fundamental Theorem of Calculus

improve the documentation of `contra.v`

`funrpos` and `funepos` should be factorized

max is a monoid operator

Document the sub-directories of `theories`

Split `probability.v` into a directory `probability_theory`

introduce `{within [a, b], derivable f}` or/and "differentiable from the right/left at a/b"

redefine distr using esum and lebesgue

Initial topology induced by a family of functions

Holomorphy

naming in `classical_sets` conflicts with `fintype`

put together statements about `]x-r,x+r[`

Add closed sets to topological mixin

candidate lemma for a PR (`bounded`, `lee_sum`, `nneseries`)

Solve slowdown in derive

TODO: rename `pseudometric`

the Gamma function

`conv_gt0` as an instance of `PosNum`

Issues