Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Hierarchy builder merged #1161

Merged
merged 216 commits into from
Jan 24, 2024
Merged

Hierarchy builder merged #1161

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
216 commits
Select commit Hold shift + click to select a range
be7aa7c
Port to Hierarchy-builder
CohenCyril Jul 13, 2022
2f09718
Add notation for dual_extended
proux01 Mar 6, 2023
da3c61b
Add Zsemimodule instances on ereal
proux01 Mar 6, 2023
70c7c8e
Change +%E notations to use GRing.add
proux01 Mar 19, 2023
847d558
Don't use dEFin in notation
proux01 Mar 20, 2023
329cb34
sumeN (#815)
affeldt-aist Feb 5, 2023
238ecda
Quotient topology (#786)
zstone1 Feb 6, 2023
d849efa
Product embedding (#768)
zstone1 Feb 6, 2023
c65401d
add other work using mca (#837)
affeldt-aist Feb 7, 2023
050367e
rename and doc finSubCover (#832)
affeldt-aist Feb 7, 2023
c7c4824
Countable products of metrics is metrizable (#763)
zstone1 Feb 7, 2023
7cad444
Clopen and Connected sets (#840)
zstone1 Feb 13, 2023
e750162
minor generalizations (#848)
affeldt-aist Feb 18, 2023
30ad54d
Cluster1 (#850)
zstone1 Feb 22, 2023
7ea530f
fixes #853 (#854)
affeldt-aist Feb 23, 2023
c41f931
fixes #851
affeldt-aist Feb 22, 2023
79d20c0
fixes (#843)
affeldt-aist Feb 24, 2023
741d81f
add a type for finite measures (#836)
affeldt-aist Feb 24, 2023
b8642a2
changelog fo version 0.6.1 (#855)
affeldt-aist Feb 24, 2023
8de48e1
\bar R canonicals for tblattice
affeldt-aist Feb 27, 2023
5060f8c
generalize emeasurable_itv_* lemmas
affeldt-aist Feb 25, 2023
dea05f6
Itv (#869)
proux01 Mar 15, 2023
9d73a4e
factor ae proofs
affeldt-aist Mar 16, 2023
a886775
complete changelog
affeldt-aist Mar 16, 2023
9405ce4
fubini for s-finite measures (#877)
affeldt-aist Mar 18, 2023
cdd5d04
fixes naming of topology.v
affeldt-aist Mar 14, 2023
92e3a22
fixes #865
affeldt-aist Mar 14, 2023
255fb20
fixes #864
affeldt-aist Mar 14, 2023
c665e8b
fix changelog
affeldt-aist Mar 14, 2023
7ce6f23
porting quotient fixes
zstone1 Mar 29, 2023
10a75dd
Merge pull request #888 from zstone1/port_quot_fix
proux01 Mar 29, 2023
1397a88
add comment about HB compatibility to pr_template.md
affeldt-aist Mar 27, 2023
7a89a87
typo
affeldt-aist Apr 5, 2023
3dbb4aa
Add sqrte
proux01 Mar 28, 2023
30c226e
gen exp_fun (#876)
affeldt-aist Mar 31, 2023
435cb61
powere_pos
affeldt-aist Apr 6, 2023
bc2c2f9
redirect to tools
affeldt-aist Apr 6, 2023
7a84006
conv -> line_path
affeldt-aist Mar 14, 2023
7de4f74
fix changelog
affeldt-aist Mar 14, 2023
528617e
[CI] Update Nix toolbox
proux01 Apr 9, 2023
2b1047b
Cantor Space Theory: zero dimensional and totally disconnected (#886)
zstone1 Apr 13, 2023
948feae
fixing product names
zstone1 Apr 13, 2023
fbf0f9d
Merge pull request #897 from zstone1/hb_zero_dimensional
proux01 Apr 13, 2023
82f2a47
Hb uniform pseudometric (#898)
zstone1 Apr 14, 2023
4efa5c7
Probability (#516)
affeldt-aist Apr 14, 2023
f7261c0
ae as a filter (#894)
affeldt-aist Apr 19, 2023
5e0a18d
Convex exp (#873)
affeldt-aist Apr 20, 2023
2b87e2b
fixing instances for convex
affeldt-aist Apr 21, 2023
81651a8
tentative proof of Hahn decomposition theorem (#777)
affeldt-aist Apr 21, 2023
2623d61
clarify status of lemmas in altreals (#833)
affeldt-aist Apr 21, 2023
0c9e3b2
changelog for version 0.6.2 (#908)
affeldt-aist Apr 21, 2023
5ad79c4
fixes #901 (#907)
affeldt-aist Apr 26, 2023
3d54730
fixes #909 (#910)
affeldt-aist Apr 26, 2023
16b11c2
globally lipschitz lemmas (#906)
IshiguroYoshihiro Apr 27, 2023
5d9c6fd
generalization of `measurable_funU` (#913)
affeldt-aist Apr 27, 2023
3b7b705
eq_seriesl (#911)
affeldt-aist Apr 27, 2023
77c20df
fix eq_seriesl
affeldt-aist Apr 27, 2023
3602fd7
[CI] Update Nix toolbox (#923)
proux01 Apr 29, 2023
fec4499
Cantor misc (#893) (#922)
proux01 Apr 29, 2023
d392c15
adding second countable stuff (#902)
zstone1 May 3, 2023
ed1629f
rm dup emeasurable_funM (#924)
affeldt-aist May 4, 2023
b6355f0
uniqueness of RN derivatives up ae eq (#914)
affeldt-aist May 4, 2023
c2d31fd
fix
affeldt-aist May 5, 2023
fe0d4fd
Fix compilation
proux01 May 6, 2023
497b612
Improve previous fix
proux01 May 7, 2023
6a85274
a hierarchy and a theory of kernels (#896)
affeldt-aist May 13, 2023
ff32a0b
fix kernel.v
affeldt-aist May 13, 2023
3a92e7b
Refactoring lemmas about composition in Lebesgue Measure (#925)
marcomole00 May 15, 2023
64b5046
Covariance (#918)
proux01 May 16, 2023
ec67ee3
remove duplicated information about nix
affeldt-aist May 16, 2023
d22c5d6
measurable_fun lemmas renaming
affeldt-aist May 16, 2023
0789d14
fixes #930
affeldt-aist May 16, 2023
1b9c531
Cantelli (#920)
proux01 May 17, 2023
c68b2e1
Lock integrable (#932)
proux01 May 20, 2023
fffb22f
Covariance inequality (#919)
proux01 May 21, 2023
dd1b0af
upd doc and convention in measure.v (#933)
affeldt-aist May 25, 2023
c61bed0
swapping definition of the semiring on intervals and hlength to remov…
CohenCyril May 26, 2023
447ef98
Remove some MathComp 2.0.0 deprecations
proux01 Jun 6, 2023
bad6b21
Remove MathComp 1.17.0 deprecations
proux01 Jun 6, 2023
c36cf0c
fixes #940
affeldt-aist Jun 3, 2023
53b22c2
Hierarchy builder (#946)
affeldt-aist Jun 8, 2023
4b50ab6
format doc of charge.v
affeldt-aist Jun 7, 2023
fdc39c9
update opam files
affeldt-aist Jun 20, 2023
aa0099a
fixes #948 (#949)
affeldt-aist Jun 20, 2023
e0d9997
changelog for version 0.6.3 (#952)
affeldt-aist Jun 21, 2023
edffcad
put all_classical in Make
affeldt-aist Jun 24, 2023
bc0f2c9
Fix compilation of the HB branch
proux01 Jul 6, 2023
92c0d46
Outer regularity for Lebesgue measure (#957)
zstone1 Jun 26, 2023
7e9c364
rm warnings
affeldt-aist Jun 28, 2023
a2098e9
More measure theory helpers (#962)
zstone1 Jun 26, 2023
3f138fc
rm warnings
affeldt-aist Jun 28, 2023
f146a80
Smallest filter (#915)
zstone1 Jun 27, 2023
44e5c0a
fix changelog unreleased
affeldt-aist Jun 28, 2023
f23e2f2
Egorov's theorem (#964)
zstone1 Jun 27, 2023
06ca9d8
specifying filters for egorov
zstone1 Jun 28, 2023
e0c108b
Revert "Fix compilation of the HB branch"
proux01 Jul 13, 2023
6e07591
fixes #960 (#961)
affeldt-aist Jun 28, 2023
8bab876
add measurable_minr (#953)
affeldt-aist Jun 28, 2023
bcf723e
[doc] Improve output of coqdoc in header comments
proux01 Jun 21, 2023
2f5a2c0
minor fixes and additions to `exp.v` (#939)
affeldt-aist Jun 29, 2023
2f0ba78
fix make doc (#959)
affeldt-aist Jun 29, 2023
8444298
rm .classical
affeldt-aist Jul 6, 2023
4f69d46
powere_pos lemmas
affeldt-aist Jun 1, 2023
9b8468d
Simple functions are dense in L1 (#968)
zstone1 Jul 7, 2023
b513e81
minor generalizations, additions, fixes (#974)
affeldt-aist Jul 16, 2023
5613bc0
Lusin (#966)
zstone1 Jul 17, 2023
b9d6c8f
minor generalizations (#977)
affeldt-aist Jul 18, 2023
d26fb19
fixes #979 (#980)
affeldt-aist Jul 18, 2023
bfcef7b
Zorn lemma for inclusion (#978)
affeldt-aist Jul 20, 2023
753304e
extended distance (#986)
zstone1 Jul 26, 2023
5c4cf33
fix
affeldt-aist Jul 29, 2023
e584619
Tietze's theorem (#971)
zstone1 Jul 28, 2023
4341ce8
minor generalizations, renaming (#985)
affeldt-aist Jul 28, 2023
6e0d97d
Fixes 994 (#997)
affeldt-aist Jul 29, 2023
acf43c0
fixes #988 (#989)
affeldt-aist Jul 29, 2023
a952136
fix warning
affeldt-aist Jul 29, 2023
b7cea34
closed_bigcup (#991)
affeldt-aist Jul 31, 2023
bebe72c
Remove useless instance
proux01 Jul 27, 2023
73e67de
Add signed instances for Posz and Negz
proux01 Jul 27, 2023
3aa6338
Proof of Urysohn's lemma. PR #900
zstone1 Apr 13, 2023
28c4d5f
Forgotten probability.v in theories/Make (#1001)
proux01 Aug 5, 2023
b98e88a
changelog for version 0.6.4 (#1003)
affeldt-aist Aug 5, 2023
7c179ee
declare kseries as an s-finite kernel (#1004)
affeldt-aist Aug 7, 2023
57e18a8
fix
affeldt-aist Aug 9, 2023
7040a92
lee_addgt0Pr (#992)
affeldt-aist Aug 8, 2023
31d29ce
Lebesgue measure 20230807 (#1005)
affeldt-aist Aug 8, 2023
fef976b
ln is concave (#990)
affeldt-aist Aug 11, 2023
3e0ad7f
script simplification (#1012)
affeldt-aist Aug 22, 2023
381bfba
Lebesgue differentiation for continuous functions (#972)
zstone1 Aug 22, 2023
eae701e
fix compilation
affeldt-aist Aug 23, 2023
f6ad511
Metric Spaces are Normal (#1002)
zstone1 Aug 22, 2023
ac4bbfb
fix compilation
affeldt-aist Aug 23, 2023
ffc8024
Fix comilation
proux01 Sep 22, 2023
812c17d
[CI] Update Nix CI
proux01 Sep 22, 2023
9490ab2
Adapt to https://github.com/math-comp/math-comp/pull/1052
proux01 Sep 23, 2023
b998c41
Adapt to https://github.com/math-comp/math-comp/pull/1068
proux01 Sep 23, 2023
25e23a4
Continuous functions are dense in L1 (#1015)
zstone1 Aug 31, 2023
dac8f36
simplify proof script, %type in notations
affeldt-aist Aug 22, 2023
81bc67c
Don't require nsatz in exp.v
proux01 Sep 7, 2023
bf0ab5a
Hoelder's inequality (#942)
affeldt-aist Sep 14, 2023
6b4c85e
Rm notation 2 in signed.v (#999)
proux01 Sep 25, 2023
2926a14
Fixes 1016 and 1017 (#1022)
affeldt-aist Sep 27, 2023
10c666f
Lemma gt0_ltr_powR (#1027)
hoheinzollern Oct 2, 2023
bbeed4c
Convexity of powR (#1011)
hoheinzollern Oct 2, 2023
10e8dc3
changelog for version 0.6.5 (#1032)
affeldt-aist Oct 2, 2023
fd83f43
upd README (#1033)
affeldt-aist Oct 2, 2023
28ec510
add link to coqdoc (#1034)
affeldt-aist Oct 2, 2023
7f238c0
bump coq version in opam
affeldt-aist Oct 2, 2023
caabd47
fixes #1042
affeldt-aist Oct 3, 2023
8d60548
fix warnings
affeldt-aist Oct 10, 2023
c8cfdf9
fixes #1037
affeldt-aist Oct 3, 2023
baf1026
fixes #1045
affeldt-aist Oct 5, 2023
d8955a7
fixes #1046
affeldt-aist Oct 5, 2023
fcac853
fixes #1049 (#1050)
affeldt-aist Oct 10, 2023
1cbb3aa
charge factory (#1008)
IshiguroYoshihiro Oct 11, 2023
c29e498
Adapt to https://github.com/coq/coq/pull/18014
proux01 Oct 10, 2023
05968c7
negligible_bigcup (#1058)
affeldt-aist Oct 15, 2023
6312d87
fixes #1056 (#1057)
affeldt-aist Oct 15, 2023
5ef9815
New notations of negative/positive_set (#1062)
IshiguroYoshihiro Oct 20, 2023
98403cd
Lebesgue Stieltjes measure (#677)
affeldt-aist Oct 23, 2023
69fcf5d
Adapt to https://github.com/math-comp/math-comp/pull/1052
proux01 Oct 24, 2023
6d29336
rm Idioms (#1070)
affeldt-aist Oct 26, 2023
eeca1a3
Adapt to https://github.com/coq/coq/pull/18224
proux01 Nov 10, 2023
7e0b61e
fixes #1051 (rename `lim_sup` -> `limn_sup`) (#1068)
affeldt-aist Oct 30, 2023
d105e23
Monotonicity lemmas for norms (#1060)
hoheinzollern Nov 1, 2023
a140ffd
Chernoff bound (#1053)
hoheinzollern Nov 1, 2023
fc7ebdc
Radon nikodym cscale (#1076)
IshiguroYoshihiro Nov 6, 2023
323e8a0
Fixes 20231108 (#1081)
affeldt-aist Nov 9, 2023
e4d3396
tentative formalization of Vitali's lemma (#973)
affeldt-aist Nov 9, 2023
31e13ee
fixes #1052 (#1085)
affeldt-aist Nov 10, 2023
83690d1
expeR (#1047)
hoheinzollern Nov 10, 2023
f485ccc
Minkowski (#1000)
hoheinzollern Nov 13, 2023
574424a
fixes #1064 (#1091)
affeldt-aist Nov 13, 2023
d97bec5
easy lemmas (#1090)
affeldt-aist Nov 13, 2023
0a1c250
tentative formalization of Vitali's theorem (#984)
affeldt-aist Nov 14, 2023
bd1e2ac
changelog for version 0.6.6 (#1095)
affeldt-aist Nov 14, 2023
e3a557e
Alexandroff-Hausdorff Theorem and the Cantor Space (#834) (#1102)
affeldt-aist Nov 17, 2023
38f7ea7
Adapt to https://github.com/math-comp/math-comp/pull/986
proux01 Nov 24, 2023
480ca05
Adapt to math-comp/math-comp#1131
pi8027 Dec 5, 2023
a1bd43b
Adapt to math-comp/math-comp#1133 (replace fun_scope with function_sc…
pi8027 Dec 8, 2023
5c4d92b
Merge pull request #1115 from math-comp/function_scope
pi8027 Dec 8, 2023
c1e55ab
Fixes 20231117 (#1106)
affeldt-aist Nov 17, 2023
0385cce
cvg lemmas for fun
affeldt-aist Nov 16, 2023
55c498c
doc
affeldt-aist Nov 16, 2023
eb75723
Hardy littlewood (#995)
affeldt-aist Dec 14, 2023
1ce88e6
ae_eq lemmas (#1110)
IshiguroYoshihiro Dec 21, 2023
c34d076
more opam keywords (MCA-dev meeting of 2023-12-21) (#1125)
affeldt-aist Dec 22, 2023
4fb7acc
fixes #1123 (unusable lemma) (#1124)
affeldt-aist Dec 26, 2023
23499db
fixes #667 (#1127)
affeldt-aist Dec 27, 2023
903a339
[CI] Update Nix toolbox
proux01 Jan 8, 2024
d2c1665
Redefine \min and \max in function_scope
pi8027 Jan 8, 2024
cd6f8c0
rm dup lemmas (#1129)
affeldt-aist Jan 1, 2024
aed4ed5
Radon-Nikodym chain rule (#1083)
affeldt-aist Jan 6, 2024
1fd0e85
format doc (#1130)
affeldt-aist Jan 7, 2024
75650ef
restrain the scope of measurable args (#1116)
affeldt-aist Jan 7, 2024
0e48333
isolate the theory of lime_sup (#1121)
affeldt-aist Jan 7, 2024
1ed1122
helper lemmas for contra (PR #1119) (#1136)
Tragicus Jan 8, 2024
65fcb33
rm renaming warnings
affeldt-aist Jan 9, 2024
cb2be15
minimal changes to documentation to test coq2html (#1108)
affeldt-aist Jan 8, 2024
f566876
Alternative form of Chernoff's bound (#1140)
hoheinzollern Jan 8, 2024
16891ad
upd misc/uniform_bigO.v (#1142)
affeldt-aist Jan 9, 2024
1c5d36e
upd uniform_bigO.v
affeldt-aist Jan 9, 2024
186bd3c
Changelog067 (#1143) (#1145)
affeldt-aist Jan 9, 2024
aac80f4
add HB instances (#1146)
affeldt-aist Jan 11, 2024
d1d2d70
adapt to change in coq2html (#1148)
affeldt-aist Jan 14, 2024
a9aa47b
Redefine \min and \max in function_scope
pi8027 Jan 8, 2024
592f514
fixes #1131 (#1132)
affeldt-aist Jan 18, 2024
04975f7
generalizations (#1147)
affeldt-aist Jan 18, 2024
71e2ede
Curry is continuous (#926)
zstone1 Jan 18, 2024
7b1644a
Add contra tactics
Dec 18, 2023
9ba7c5b
Total variation (#1118)
zstone1 Jan 19, 2024
9258582
changelog for version 0.7.0 (#1158)
affeldt-aist Jan 19, 2024
0a8b956
Merge remote-tracking branch 'origin/hierarchy-builder'
affeldt-aist Jan 22, 2024
2ab529b
fix
affeldt-aist Jan 22, 2024
5004eee
changelog
affeldt-aist Jan 23, 2024
bfcfe58
upd of the doc
affeldt-aist Jan 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 0 additions & 40 deletions .github/workflows/docker-action.yml
View file
Open in desktop

This file was deleted.

203 changes: 0 additions & 203 deletions .github/workflows/nix-action-8.15.yml
View file
Open in desktop

This file was deleted.

Loading
Loading