Port to MathComp 2#951

Merged

affeldt-aist merged 212 commits intomasterfrom

hierarchy-builder

Jan 24, 2024

Commits on Mar 24, 2023

Port to Hierarchy-builder

authored and
proux01
committed
Add notation for dual_extended
proux01
committed
Add Zsemimodule instances on ereal
proux01
committed
Change +%E notations to use GRing.add
proux01
committed
Don't use dEFin in notation
proux01
committed
sumeN (#815)

affeldt-aist
authored and
proux01
committed
Quotient topology (#786)

authored and
proux01
committed
Product embedding (#768)

authored and
proux01
committed
add other work using mca (#837)

affeldt-aist
authored and
proux01
committed
rename and doc finSubCover (#832)

affeldt-aist
authored and
proux01
committed
Countable products of metrics is metrizable (#763)

authored and
proux01
committed
Clopen and Connected sets (#840)

authored and
proux01
committed
minor generalizations (#848)

affeldt-aist
authored and
proux01
committed
Cluster1 (#850)

authored and
proux01
committed
fixes #853 (#854)

affeldt-aist
authored and
proux01
committed
fixes #851

affeldt-aist
authored and
proux01
committed

Commits on Mar 25, 2023

fixes (#843)

affeldt-aist
authored and
proux01
committed
add a type for finite measures (#836)

affeldt-aist
authored and
proux01
committed
changelog fo version 0.6.1 (#855)

affeldt-aist
authored and
proux01
committed
\bar R canonicals for tblattice

authored and
proux01
committed
generalize emeasurable_itv_* lemmas

affeldt-aist
authored and
proux01
committed
Itv (#869)

proux01
and
affeldt-aist
committed
factor ae proofs

affeldt-aist
authored and
proux01
committed
complete changelog

affeldt-aist
authored and
proux01
committed
fubini for s-finite measures (#877)

affeldt-aist
authored and
proux01
committed

Commits on Mar 29, 2023

fixes naming of topology.v

affeldt-aist
authored and
proux01
committed
fixes #865

affeldt-aist
authored and
proux01
committed
fixes #864

affeldt-aist
authored and
proux01
committed
fix changelog

affeldt-aist
authored and
proux01
committed
porting quotient fixes

zstone1
authored and
proux01
committed
Merge pull request #888 from zstone1/port_quot_fix
proux01
authored

Commits on Apr 5, 2023

Commits on Apr 10, 2023

Add sqrte

proux01
and
affeldt-aist
committed
gen exp_fun (#876)

committed

Commits on Apr 12, 2023

Commits on Apr 13, 2023

Commits on Apr 14, 2023

Hb uniform pseudometric (#898)

zstone1
and
affeldt-aist
authored

Commits on Apr 15, 2023

Probability (#516)

committed

Commits on Apr 19, 2023

ae as a filter (#894)
affeldt-aist
committed

Commits on Apr 20, 2023

Convex exp (#873)

committed

Commits on Apr 21, 2023

Commits on Apr 24, 2023

changelog for version 0.6.2 (#908)
affeldt-aist
committed

Commits on Apr 26, 2023

Commits on Apr 27, 2023

Commits on Apr 29, 2023

Commits on May 4, 2023

Commits on May 5, 2023

fix
affeldt-aist
committed

Commits on May 6, 2023

Fix compilation
proux01
committed

Commits on May 7, 2023

Improve previous fix
proux01
committed

Commits on May 13, 2023

Commits on May 15, 2023

Refactoring lemmas about composition in Lebesgue Measure (#925)

committed

Commits on May 18, 2023

Commits on May 20, 2023

Lock integrable (#932)

proux01
authored and
affeldt-aist
committed

Commits on May 26, 2023

Commits on Jun 7, 2023

Remove some MathComp 2.0.0 deprecations

proux01
authored and
affeldt-aist
committed
Remove MathComp 1.17.0 deprecations

proux01
authored and
affeldt-aist
committed
fixes #940

affeldt-aist
authored and
proux01
committed

Commits on Jun 8, 2023

Hierarchy builder (#946)

affeldt-aist
and
zstone1
authored
format doc of charge.v

affeldt-aist
authored and
proux01
committed

Commits on Jun 21, 2023

update opam files

affeldt-aist
authored and
proux01
committed

Commits on Jun 25, 2023

fixes #948 (#949)

affeldt-aist
authored and
proux01
committed
changelog for version 0.6.3 (#952)

affeldt-aist
authored and
proux01
committed

Commits on Jun 27, 2023

put all_classical in Make

affeldt-aist
authored and
proux01
committed

Commits on Jul 8, 2023

Fix compilation of the HB branch
proux01
committed
Outer regularity for Lebesgue measure (#957)

authored and
proux01
committed
rm warnings

affeldt-aist
authored and
proux01
committed
More measure theory helpers (#962)

authored and
proux01
committed
rm warnings

affeldt-aist
authored and
proux01
committed
Smallest filter (#915)

authored and
proux01
committed
fix changelog unreleased

affeldt-aist
authored and
proux01
committed
Egorov's theorem (#964)

zstone1
authored and
proux01
committed
specifying filters for egorov

zstone1
authored and
proux01
committed

Commits on Jul 17, 2023

Revert "Fix compilation of the HB branch"
proux01
committed
fixes #960 (#961)

affeldt-aist
authored and
proux01
committed
add measurable_minr (#953)

affeldt-aist
authored and
proux01
committed
[doc] Improve output of coqdoc in header comments
proux01
committed
minor fixes and additions to `exp.v` (#939)

authored and
proux01
committed
fix make doc (#959)

affeldt-aist
authored and
proux01
committed
rm .classical

affeldt-aist
authored and
proux01
committed
powere_pos lemmas

authored and
proux01
committed

Commits on Jul 21, 2023

Simple functions are dense in L1 (#968)

authored and
proux01
committed
minor generalizations, additions, fixes (#974)

affeldt-aist
authored and
proux01
committed
Lusin (#966)

authored and
proux01
committed
minor generalizations (#977)

affeldt-aist
authored and
proux01
committed
fixes #979 (#980)

affeldt-aist
authored and
proux01
committed
Zorn lemma for inclusion (#978)

authored and
proux01
committed

Commits on Jul 31, 2023

extended distance (#986)

authored and
proux01
committed
fix

affeldt-aist
authored and
proux01
committed
Tietze's theorem (#971)

authored and
proux01
committed
minor generalizations, renaming (#985)

authored and
proux01
committed
Fixes 994 (#997)

affeldt-aist
authored and
proux01
committed
fixes #988 (#989)

affeldt-aist
authored and
proux01
committed
fix warning

affeldt-aist
authored and
proux01
committed

Commits on Aug 9, 2023

closed_bigcup (#991)
affeldt-aist
committed
Remove useless instance

proux01
authored and
affeldt-aist
committed
Add signed instances for Posz and Negz

proux01
authored and
affeldt-aist
committed
Proof of Urysohn's lemma. PR #900

authored and
affeldt-aist
committed
Forgotten probability.v in theories/Make (#1001)

proux01
authored and
affeldt-aist
committed
changelog for version 0.6.4 (#1003)
affeldt-aist
committed
declare kseries as an s-finite kernel (#1004)
affeldt-aist
committed
fix
affeldt-aist
committed
lee_addgt0Pr (#992)
affeldt-aist
committed
Lebesgue measure 20230807 (#1005)

affeldt-aist
and
zstone1
committed

Commits on Sep 22, 2023

Commits on Sep 23, 2023

Commits on Sep 25, 2023

Continuous functions are dense in L1 (#1015)

authored and
proux01
committed

Commits on Sep 28, 2023

simplify proof script, %type in notations

affeldt-aist
authored and
proux01
committed
Don't require nsatz in exp.v
proux01
committed
Hoelder's inequality (#942)

authored and
proux01
committed
Rm notation 2 in signed.v (#999)
proux01
committed
Fixes 1016 and 1017 (#1022)

affeldt-aist
authored and
proux01
committed

Commits on Oct 11, 2023

Commits on Oct 30, 2023

charge factory (#1008)

authored and
proux01
committed
Adapt to https://github.com/coq/coq/pull/18014
proux01
committed
negligible_bigcup (#1058)

affeldt-aist
authored and
proux01
committed
fixes #1056 (#1057)

affeldt-aist
authored and
proux01
committed
New notations of negative/positive_set (#1062)

authored and
proux01
committed
Lebesgue Stieltjes measure (#677)

authored and
proux01
committed
Adapt to https://github.com/math-comp/math-comp/pull/1052
proux01
committed
rm Idioms (#1070)

affeldt-aist
authored and
proux01
committed

Commits on Nov 10, 2023

Adapt to https://github.com/coq/coq/pull/18224
proux01
committed
fixes #1051 (rename `lim_sup` -> `limn_sup`) (#1068)

affeldt-aist
authored and
proux01
committed
Monotonicity lemmas for norms (#1060)

authored and
proux01
committed
Chernoff bound (#1053)

authored and
proux01
committed
Radon nikodym cscale (#1076)

authored and
proux01
committed
Fixes 20231108 (#1081)

affeldt-aist
authored and
proux01
committed

Commits on Nov 15, 2023

tentative formalization of Vitali's lemma (#973)

affeldt-aist
authored and
proux01
committed
fixes #1052 (#1085)

affeldt-aist
authored and
proux01
committed
expeR (#1047)

authored and
proux01
committed
Minkowski (#1000)

authored and
proux01
committed
fixes #1064 (#1091)

affeldt-aist
authored and
proux01
committed
easy lemmas (#1090)

authored and
proux01
committed
tentative formalization of Vitali's theorem (#984)

authored and
proux01
committed
changelog for version 0.6.6 (#1095)

affeldt-aist
authored and
proux01
committed

Commits on Nov 17, 2023

Alexandroff-Hausdorff Theorem and the Cantor Space (#834) (#1102)

affeldt-aist
and
zstone1
authored

Commits on Nov 24, 2023

Adapt to https://github.com/math-comp/math-comp/pull/986
proux01
committed

Commits on Dec 6, 2023

Adapt to math-comp/math-comp#1131

pi8027
authored and
proux01
committed

Commits on Dec 8, 2023

Commits on Dec 14, 2023

Commits on Dec 28, 2023

Hardy littlewood (#995)

affeldt-aist
authored and
proux01
committed
ae_eq lemmas (#1110)

authored and
proux01
committed
more opam keywords (MCA-dev meeting of 2023-12-21) (#1125)

affeldt-aist
authored and
proux01
committed
fixes #1123 (unusable lemma) (#1124)

authored and
proux01
committed
fixes #667 (#1127)

affeldt-aist
authored and
proux01
committed

Commits on Jan 8, 2024

[CI] Update Nix toolbox
proux01
committed
Redefine \min and \max in function_scope

pi8027
authored and
proux01
committed

Commits on Jan 9, 2024

rm dup lemmas (#1129)

affeldt-aist
authored and
proux01
committed
Radon-Nikodym chain rule (#1083)

authored and
proux01
committed
format doc (#1130)

affeldt-aist
and
proux01
committed
restrain the scope of measurable args (#1116)

authored and
proux01
committed
isolate the theory of lime_sup (#1121)

authored and
proux01
committed
helper lemmas for contra (PR #1119) (#1136)

authored and
proux01
committed
rm renaming warnings

affeldt-aist
authored and
proux01
committed
minimal changes to documentation to test coq2html (#1108)

affeldt-aist
authored and
proux01
committed
Alternative form of Chernoff's bound (#1140)

hoheinzollern
authored and
proux01
committed
upd misc/uniform_bigO.v (#1142)

affeldt-aist
authored and
proux01
committed
upd uniform_bigO.v

affeldt-aist
authored and
proux01
committed
Changelog067 (#1143) (#1145)
affeldt-aist
authored

Commits on Jan 15, 2024

add HB instances (#1146)

affeldt-aist
authored and
proux01
committed
adapt to change in coq2html (#1148)

affeldt-aist
authored and
proux01
committed

Commits on Jan 17, 2024

Redefine \min and \max in function_scope

pi8027
authored and
proux01
committed

Commits on Jan 20, 2024

fixes #1131 (#1132)

affeldt-aist
authored and
proux01
committed
generalizations (#1147)

affeldt-aist
authored and
proux01
committed
Curry is continuous (#926)

authored and
proux01
committed
Add contra tactics

authored and
proux01
committed
Total variation (#1118)

authored and
proux01
committed
changelog for version 0.7.0 (#1158)

affeldt-aist
authored and
proux01
committed