Code

Hierarchy builder merged#1161

Code

Merged

affeldt-aist merged 216 commits intomath-comp:mastermath-comp/analysis:masterfrom affeldt-aist:hierarchy-builder_mergedaffeldt-aist/analysis:hierarchy-builder_mergedCopy head branch name to clipboardJan 24, 2024

+5,328-6,585

Commits

Commits on Mar 24, 2023

• Port to Hierarchy-builder

  Show description for be7aa7c
  

  2 peopleauthored and

  proux01

  committed
  be7aa7c

• Add notation for dual_extended

  proux01

  committed
  2f09718

• Add Zsemimodule instances on ereal

  proux01

  committed
  da3c61b

• Change +%E notations to use GRing.add

  proux01

  committed
  70c7c8e

• Don't use dEFin in notation

  proux01

  committed
  847d558

• sumeN (math-comp#815)

  Show description for 329cb34
  

  affeldt-aist

  authored and

  proux01

  committed
  329cb34

• Quotient topology (math-comp#786)

  Show description for 238ecda
  

  2 peopleauthored and

  proux01

  committed
  238ecda

• Product embedding (math-comp#768)

  Show description for d849efa
  

  2 peopleauthored and

  proux01

  committed
  d849efa

• add other work using mca (math-comp#837)

  

  affeldt-aist

  authored and

  proux01

  committed
  c65401d

• rename and doc finSubCover (math-comp#832)

  Show description for 050367e
  

  affeldt-aist

  authored and

  proux01

  committed
  050367e

• Countable products of metrics is metrizable (math-comp#763)

  Show description for c7c4824
  

  2 peopleauthored and

  proux01

  committed
  c7c4824

• Clopen and Connected sets (math-comp#840)

  Show description for 7cad444
  

  2 peopleauthored and

  proux01

  committed
  7cad444

• minor generalizations (math-comp#848)

  Show description for e750162
  

  affeldt-aist

  authored and

  proux01

  committed
  e750162

• Cluster1 (math-comp#850)

  Show description for 30ad54d
  

  2 peopleauthored and

  proux01

  committed
  30ad54d

• fixes math-comp#853 (math-comp#854)

  

  affeldt-aist

  authored and

  proux01

  committed
  7ea530f

• fixes math-comp#851

  

  affeldt-aist

  authored and

  proux01

  committed
  c41f931

Commits on Mar 25, 2023

• fixes (math-comp#843)

  Show description for 79d20c0
  

  affeldt-aist

  authored and

  proux01

  committed
  79d20c0

• add a type for finite measures (math-comp#836)

  Show description for 741d81f
  

  affeldt-aist

  authored and

  proux01

  committed
  741d81f

• changelog fo version 0.6.1 (math-comp#855)

  

  affeldt-aist

  authored and

  proux01

  committed
  b8642a2

• \bar R canonicals for tblattice

  Show description for 8de48e1
  

  2 peopleauthored and

  proux01

  committed
  8de48e1

• generalize emeasurable_itv_* lemmas

  Show description for 5060f8c
  

  affeldt-aist

  authored and

  proux01

  committed
  5060f8c

• Itv (math-comp#869)

  Show description for dea05f6
  

  proux01

  and

  affeldt-aist

  committed
  dea05f6

• factor ae proofs

  

  affeldt-aist

  authored and

  proux01

  committed
  9d73a4e

• complete changelog

  

  affeldt-aist

  authored and

  proux01

  committed
  a886775

• fubini for s-finite measures (math-comp#877)

  

  affeldt-aist

  authored and

  proux01

  committed
  9405ce4

Commits on Mar 29, 2023

• fixes naming of topology.v

  Show description for cdd5d04
  

  affeldt-aist

  authored and

  proux01

  committed
  cdd5d04

• fixes math-comp#865

  

  affeldt-aist

  authored and

  proux01

  committed
  92e3a22

• fixes math-comp#864

  

  affeldt-aist

  authored and

  proux01

  committed
  255fb20

• fix changelog

  

  affeldt-aist

  authored and

  proux01

  committed
  c665e8b

• porting quotient fixes

  

  zstone1

  authored and

  proux01

  committed
  7ce6f23

• Merge pull request math-comp#888 from zstone1/port_quot_fix

  Show description for 10a75dd
  proux01

  authored
  10a75dd

Commits on Apr 5, 2023

• add comment about HB compatibility to pr_template.md

  affeldt-aist

  committed
  1397a88

• typo

  affeldt-aist

  committed
  7a89a87

Commits on Apr 10, 2023

• Add sqrte

  Show description for 3dbb4aa
  

  proux01

  and

  affeldt-aist

  committed
  3dbb4aa

• gen exp_fun (math-comp#876)

  Show description for 30c226e
  

  3 peoplecommitted
  30c226e

Commits on Apr 12, 2023

• powere_pos

  Show description for 435cb61
  

  3 peoplecommitted
  435cb61

• redirect to tools

  affeldt-aist

  committed
  bc2c2f9

• conv -> line_path

  affeldt-aist

  committed
  7a84006

• fix changelog

  affeldt-aist

  committed
  7de4f74

• [CI] Update Nix toolbox

  proux01

  committed
  528617e

Commits on Apr 13, 2023

• Cantor Space Theory: zero dimensional and totally disconnected (math-comp#886)

  Show description for 2b1047b
  

  zstone1

  and

  affeldt-aist

  committed
  2b1047b

• fixing product names

  zstone1

  committed
  948feae

• Merge pull request math-comp#897 from zstone1/hb_zero_dimensional

  Show description for fbf0f9d
  proux01

  authored
  fbf0f9d

Commits on Apr 14, 2023

• Hb uniform pseudometric (math-comp#898)

  Show description for 82f2a47
  

  zstone1

  and

  affeldt-aist

  authored
  82f2a47

Commits on Apr 15, 2023

• Probability (math-comp#516)

  Show description for 4efa5c7
  

  4 peoplecommitted
  4efa5c7

Commits on Apr 19, 2023

• ae as a filter (math-comp#894)

  Show description for f7261c0
  affeldt-aist

  committed
  f7261c0

Commits on Apr 20, 2023

• Convex exp (math-comp#873)

  Show description for 5e0a18d
  

  5 peoplecommitted
  5e0a18d

Commits on Apr 21, 2023

• fixing instances for convex

  affeldt-aist

  committed
  2b87e2b

• tentative proof of Hahn decomposition theorem (math-comp#777)

  Show description for 81651a8
  affeldt-aist

  committed
  81651a8

• clarify status of lemmas in altreals (math-comp#833)

  affeldt-aist

  committed
  2623d61

Commits on Apr 24, 2023

• changelog for version 0.6.2 (math-comp#908)

  Show description for 0c9e3b2
  affeldt-aist

  committed
  0c9e3b2

Commits on Apr 26, 2023

• fixes math-comp#901 (math-comp#907)

  Show description for 5ad79c4
  affeldt-aist

  committed
  5ad79c4

• fixes math-comp#909 (math-comp#910)

  affeldt-aist

  committed
  3d54730

Commits on Apr 27, 2023

• globally lipschitz lemmas (math-comp#906)

  Show description for 16b11c2
  

  3 peoplecommitted
  16b11c2

• generalization of measurable_funU (math-comp#913)

  Show description for 5d9c6fd
  affeldt-aist

  committed
  5d9c6fd

• eq_seriesl (math-comp#911)

  affeldt-aist

  committed
  3b7b705

• fix eq_seriesl

  affeldt-aist

  committed
  77c20df

Commits on Apr 29, 2023

• [CI] Update Nix toolbox (math-comp#923)

  proux01

  authored
  3602fd7

• Cantor misc (math-comp#893) (math-comp#922)

  Show description for fec4499
  

  3 peopleauthored
  fec4499

Commits on May 4, 2023

• adding second countable stuff (math-comp#902)

  Show description for d392c15
  

  zstone1

  and

  affeldt-aist

  committed
  d392c15

• rm dup emeasurable_funM (math-comp#924)

  affeldt-aist

  committed
  ed1629f

• uniqueness of RN derivatives up ae eq (math-comp#914)

  affeldt-aist

  committed
  b6355f0

Commits on May 5, 2023

• fix

  affeldt-aist

  committed
  c2d31fd

Commits on May 6, 2023

• Fix compilation

  proux01

  committed
  fe0d4fd

Commits on May 7, 2023

• Improve previous fix

  proux01

  committed
  497b612

Commits on May 13, 2023

• a hierarchy and a theory of kernels (math-comp#896)

  Show description for 6a85274
  

  affeldt-aist

  and

  CohenCyril

  committed
  6a85274

• fix kernel.v

  affeldt-aist

  committed
  ff32a0b

Commits on May 15, 2023

• Refactoring lemmas about composition in Lebesgue Measure (math-comp#925)

  Show description for 3a92e7b
  

  4 peoplecommitted
  3a92e7b

Commits on May 18, 2023

• Covariance (math-comp#918)

  Show description for 64b5046
  

  proux01

  and

  affeldt-aist

  committed
  64b5046

• remove duplicated information about nix

  Show description for ec67ee3
  affeldt-aist

  committed
  ec67ee3

• measurable_fun lemmas renaming

  Show description for d22c5d6
  affeldt-aist

  committed
  d22c5d6

• fixes math-comp#930

  affeldt-aist

  committed
  0789d14

• Cantelli (math-comp#920)

  Show description for 1b9c531
  

  proux01

  and

  affeldt-aist

  committed
  1b9c531

Commits on May 20, 2023

• Lock integrable (math-comp#932)

  Show description for c68b2e1
  

  proux01

  authored and

  affeldt-aist

  committed
  c68b2e1

Commits on May 26, 2023

• Covariance inequality (math-comp#919)

  Show description for fffb22f
  

  proux01

  and

  affeldt-aist

  committed
  fffb22f

• upd doc and convention in measure.v (math-comp#933)

  Show description for dd1b0af
  

  affeldt-aist

  and

  CohenCyril

  committed
  dd1b0af

• swapping definition of the semiring on intervals and hlength to remove type annotations

  

  CohenCyril

  authored and

  affeldt-aist

  committed
  c61bed0

Commits on Jun 7, 2023

• Remove some MathComp 2.0.0 deprecations

  

  proux01

  authored and

  affeldt-aist

  committed
  447ef98

• Remove MathComp 1.17.0 deprecations

  

  proux01

  authored and

  affeldt-aist

  committed
  bad6b21

• fixes math-comp#940

  

  affeldt-aist

  authored and

  proux01

  committed
  c36cf0c

Commits on Jun 8, 2023

• Hierarchy builder (math-comp#946)

  Show description for 53b22c2
  

  affeldt-aist

  and

  zstone1

  authored
  53b22c2

• format doc of charge.v

  

  affeldt-aist

  authored and

  proux01

  committed
  4b50ab6

Commits on Jun 21, 2023

• update opam files

  

  affeldt-aist

  authored and

  proux01

  committed
  fdc39c9

Commits on Jun 25, 2023

• fixes math-comp#948 (math-comp#949)

  

  affeldt-aist

  authored and

  proux01

  committed
  aa0099a

• changelog for version 0.6.3 (math-comp#952)

  Show description for e0d9997
  

  affeldt-aist

  authored and

  proux01

  committed
  e0d9997

Commits on Jun 27, 2023

• put all_classical in Make

  

  affeldt-aist

  authored and

  proux01

  committed
  edffcad

Commits on Jul 8, 2023

• Fix compilation of the HB branch

  Show description for bc0f2c9
  proux01

  committed
  bc0f2c9

• Outer regularity for Lebesgue measure (math-comp#957)

  Show description for 92c0d46
  

  2 peopleauthored and

  proux01

  committed
  92c0d46

• rm warnings

  

  affeldt-aist

  authored and

  proux01

  committed
  7e9c364

• More measure theory helpers (math-comp#962)

  Show description for a2098e9
  

  2 peopleauthored and

  proux01

  committed
  a2098e9

• rm warnings

  

  affeldt-aist

  authored and

  proux01

  committed
  3f138fc

• Smallest filter (math-comp#915)

  Show description for f146a80
  

  2 peopleauthored and

  proux01

  committed
  f146a80

• fix changelog unreleased

  

  affeldt-aist

  authored and

  proux01

  committed
  44e5c0a

• Egorov's theorem (math-comp#964)

  Show description for f23e2f2
  

  zstone1

  authored and

  proux01

  committed
  f23e2f2

• specifying filters for egorov

  

  zstone1

  authored and

  proux01

  committed
  06ca9d8

Commits on Jul 17, 2023

• Revert "Fix compilation of the HB branch"

  Show description for e0c108b
  proux01

  committed
  e0c108b

• fixes math-comp#960 (math-comp#961)

  

  affeldt-aist

  authored and

  proux01

  committed
  6e07591

• add measurable_minr (math-comp#953)

  

  affeldt-aist

  authored and

  proux01

  committed
  8bab876

• [doc] Improve output of coqdoc in header comments

  proux01

  committed
  bcf723e

• minor fixes and additions to exp.v (math-comp#939)

  Show description for 2f5a2c0
  

  2 peopleauthored and

  proux01

  committed
  2f5a2c0

• fix make doc (math-comp#959)

  

  affeldt-aist

  authored and

  proux01

  committed
  2f0ba78

• rm .classical

  

  affeldt-aist

  authored and

  proux01

  committed
  8444298

• powere_pos lemmas

  Show description for 4f69d46
  

  3 peopleauthored and

  proux01

  committed
  4f69d46

Commits on Jul 21, 2023

• Simple functions are dense in L1 (math-comp#968)

  Show description for 9b8468d
  

  2 peopleauthored and

  proux01

  committed
  9b8468d

• minor generalizations, additions, fixes (math-comp#974)

  Show description for b513e81
  

  affeldt-aist

  authored and

  proux01

  committed
  b513e81

• Lusin (math-comp#966)

  Show description for 5613bc0
  

  2 peopleauthored and

  proux01

  committed
  5613bc0

• minor generalizations (math-comp#977)

  

  affeldt-aist

  authored and

  proux01

  committed
  b9d6c8f

• fixes math-comp#979 (math-comp#980)

  

  affeldt-aist

  authored and

  proux01

  committed
  d26fb19

• Zorn lemma for inclusion (math-comp#978)

  Show description for bfcef7b
  

  3 peopleauthored and

  proux01

  committed
  bfcef7b

Commits on Jul 31, 2023

• extended distance (math-comp#986)

  Show description for 753304e
  

  2 peopleauthored and

  proux01

  committed
  753304e

• fix

  

  affeldt-aist

  authored and

  proux01

  committed
  5c4cf33

• Tietze's theorem (math-comp#971)

  Show description for e584619
  

  2 peopleauthored and

  proux01

  committed
  e584619

• minor generalizations, renaming (math-comp#985)

  Show description for 4341ce8
  

  2 peopleauthored and

  proux01

  committed
  4341ce8

• Fixes 994 (math-comp#997)

  Show description for 6e0d97d
  

  affeldt-aist

  authored and

  proux01

  committed
  6e0d97d

• fixes math-comp#988 (math-comp#989)

  

  affeldt-aist

  authored and

  proux01

  committed
  acf43c0

• fix warning

  

  affeldt-aist

  authored and

  proux01

  committed
  a952136

Commits on Aug 9, 2023

• closed_bigcup (math-comp#991)

  affeldt-aist

  committed
  b7cea34

• Remove useless instance

  

  proux01

  authored and

  affeldt-aist

  committed
  bebe72c

• Add signed instances for Posz and Negz

  

  proux01

  authored and

  affeldt-aist

  committed
  73e67de

• Proof of Urysohn's lemma. PR math-comp#900

  Show description for 3aa6338
  

  2 peopleauthored and

  affeldt-aist

  committed
  3aa6338

• Forgotten probability.v in theories/Make (math-comp#1001)

  Show description for 28c4d5f
  

  proux01

  authored and

  affeldt-aist

  committed
  28c4d5f

• changelog for version 0.6.4 (math-comp#1003)

  Show description for b98e88a
  affeldt-aist

  committed
  b98e88a

• declare kseries as an s-finite kernel (math-comp#1004)

  Show description for 7c179ee
  affeldt-aist

  committed
  7c179ee

• fix

  affeldt-aist

  committed
  57e18a8

• lee_addgt0Pr (math-comp#992)

  affeldt-aist

  committed
  7040a92

• Lebesgue measure 20230807 (math-comp#1005)

  Show description for 31d29ce
  

  affeldt-aist

  and

  zstone1

  committed
  31d29ce

Commits on Aug 23, 2023

• ln is concave (math-comp#990)

  Show description for fef976b
  affeldt-aist

  committed
  fef976b

• script simplification (math-comp#1012)

  affeldt-aist

  committed
  3e0ad7f

• Lebesgue differentiation for continuous functions (math-comp#972)

  Show description for 381bfba
  

  zstone1

  and

  affeldt-aist

  committed
  381bfba

• fix compilation

  affeldt-aist

  committed
  eae701e

• Metric Spaces are Normal (math-comp#1002)

  Show description for f6ad511
  

  zstone1

  and

  affeldt-aist

  committed
  f6ad511

• fix compilation

  affeldt-aist

  committed
  ac4bbfb

Commits on Sep 22, 2023

• Fix comilation

  proux01

  committed
  ffc8024

• [CI] Update Nix CI

  proux01

  committed
  812c17d

Commits on Sep 23, 2023

• Adapt to math-comp/math-comp#1052

  proux01

  committed
  9490ab2

• Adapt to math-comp/math-comp#1068

  proux01

  committed
  b998c41

Commits on Sep 25, 2023

• Continuous functions are dense in L1 (math-comp#1015)

  Show description for 25e23a4
  

  2 peopleauthored and

  proux01

  committed
  25e23a4

Commits on Sep 28, 2023

• simplify proof script, %type in notations

  

  affeldt-aist

  authored and

  proux01

  committed
  dac8f36

• Don't require nsatz in exp.v

  Show description for 81bc67c
  proux01

  committed
  81bc67c

• Hoelder's inequality (math-comp#942)

  Show description for bf0ab5a
  

  2 peopleauthored and

  proux01

  committed
  bf0ab5a

• Rm notation 2 in signed.v (math-comp#999)

  Show description for 6b4c85e
  proux01

  committed
  6b4c85e

• Fixes 1016 and 1017 (math-comp#1022)

  Show description for 2926a14
  

  affeldt-aist

  authored and

  proux01

  committed
  2926a14

Commits on Oct 11, 2023

• Lemma gt0_ltr_powR (math-comp#1027)

  Show description for 10c666f
  

  hoheinzollern

  and

  affeldt-aist

  committed
  10c666f

• Convexity of powR (math-comp#1011)

  Show description for bbeed4c
  

  hoheinzollern

  and

  affeldt-aist

  committed
  bbeed4c

• changelog for version 0.6.5 (math-comp#1032)

  affeldt-aist

  committed
  10e8dc3

• upd README (math-comp#1033)

  affeldt-aist

  committed
  fd83f43

• add link to coqdoc (math-comp#1034)

  Show description for 28ec510
  affeldt-aist

  committed
  28ec510

• bump coq version in opam

  affeldt-aist

  committed
  7f238c0

• fixes math-comp#1042

  affeldt-aist

  committed
  caabd47

• fix warnings

  affeldt-aist

  committed
  8d60548

• fixes math-comp#1037

  Show description for c8cfdf9
  

  affeldt-aist

  and

  CohenCyril

  committed
  c8cfdf9

• fixes math-comp#1045

  affeldt-aist

  committed
  baf1026

• fixes math-comp#1046

  affeldt-aist

  committed
  d8955a7

• fixes math-comp#1049 (math-comp#1050)

  Show description for fcac853
  affeldt-aist

  committed
  fcac853

Commits on Oct 30, 2023

• charge factory (math-comp#1008)

  Show description for 1cbb3aa
  

  2 peopleauthored and

  proux01

  committed
  1cbb3aa

• Adapt to coq/coq#18014

  proux01

  committed
  c29e498

• negligible_bigcup (math-comp#1058)

  

  affeldt-aist

  authored and

  proux01

  committed
  05968c7

• fixes math-comp#1056 (math-comp#1057)

  

  affeldt-aist

  authored and

  proux01

  committed
  6312d87

• New notations of negative/positive_set (math-comp#1062)

  Show description for 5ef9815
  

  2 peopleauthored and

  proux01

  committed
  5ef9815

• Lebesgue Stieltjes measure (math-comp#677)

  Show description for 98403cd
  

  3 peopleauthored and

  proux01

  committed
  98403cd

• Adapt to math-comp/math-comp#1052

  proux01

  committed
  69fcf5d

• rm Idioms (math-comp#1070)

  

  affeldt-aist

  authored and

  proux01

  committed
  6d29336

Commits on Nov 10, 2023

• Adapt to coq/coq#18224

  proux01

  committed
  eeca1a3

• fixes math-comp#1051 (rename lim_sup -> limn_sup) (math-comp#1068)

  Show description for 7e0b61e
  

  affeldt-aist

  authored and

  proux01

  committed
  7e0b61e

• Monotonicity lemmas for norms (math-comp#1060)

  Show description for d105e23
  

  2 peopleauthored and

  proux01

  committed
  d105e23

• Chernoff bound (math-comp#1053)

  Show description for a140ffd
  

  2 peopleauthored and

  proux01

  committed
  a140ffd

• Radon nikodym cscale (math-comp#1076)

  Show description for fc7ebdc
  

  2 peopleauthored and

  proux01

  committed
  fc7ebdc

• Fixes 20231108 (math-comp#1081)

  Show description for 323e8a0
  

  affeldt-aist

  authored and

  proux01

  committed
  323e8a0

Commits on Nov 15, 2023

• tentative formalization of Vitali's lemma (math-comp#973)

  Show description for e4d3396
  

  affeldt-aist

  authored and

  proux01

  committed
  e4d3396

• fixes math-comp#1052 (math-comp#1085)

  

  affeldt-aist

  authored and

  proux01

  committed
  31e13ee

• expeR (math-comp#1047)

  Show description for 83690d1
  

  hoheinzollern

  authored and

  proux01

  committed
  83690d1

• Minkowski (math-comp#1000)

  Show description for f485ccc
  

  hoheinzollern

  authored and

  proux01

  committed
  f485ccc

• fixes math-comp#1064 (math-comp#1091)

  

  affeldt-aist

  authored and

  proux01

  committed
  574424a

• easy lemmas (math-comp#1090)

  Show description for d97bec5
  

  2 peopleauthored and

  proux01

  committed
  d97bec5

• tentative formalization of Vitali's theorem (math-comp#984)

  Show description for 0a1c250
  

  2 peopleauthored and

  proux01

  committed
  0a1c250

• changelog for version 0.6.6 (math-comp#1095)

  Show description for bd1e2ac
  

  affeldt-aist

  authored and

  proux01

  committed
  bd1e2ac

Commits on Nov 17, 2023

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

  Show description for e3a557e
  

  affeldt-aist

  and

  zstone1

  authored
  e3a557e

Commits on Nov 24, 2023

• Adapt to math-comp/math-comp#986

  proux01

  committed
  38f7ea7

Commits on Dec 6, 2023

• Adapt to math-comp/math-comp#1131

  

  pi8027

  authored and

  proux01

  committed
  480ca05

Commits on Dec 8, 2023

• Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope)

  pi8027

  committed
  a1bd43b

• Merge pull request math-comp#1115 from math-comp/function_scope

  Show description for 5c4d92b
  pi8027

  authored
  5c4d92b

Commits on Dec 14, 2023

• Fixes 20231117 (math-comp#1106)

  Show description for c1e55ab
  affeldt-aist

  committed
  c1e55ab

• cvg lemmas for fun

  affeldt-aist

  committed
  0385cce

• doc

  affeldt-aist

  committed
  55c498c

Commits on Dec 28, 2023

• Hardy littlewood (math-comp#995)

  Show description for eb75723
  

  affeldt-aist

  authored and

  proux01

  committed
  eb75723

• ae_eq lemmas (math-comp#1110)

  Show description for 1ce88e6
  

  2 peopleauthored and

  proux01

  committed
  1ce88e6

• more opam keywords (MCA-dev meeting of 2023-12-21) (math-comp#1125)

  Show description for c34d076
  

  affeldt-aist

  authored and

  proux01

  committed
  c34d076

• fixes math-comp#1123 (unusable lemma) (math-comp#1124)

  Show description for 4fb7acc
  

  3 peopleauthored and

  proux01

  committed
  4fb7acc

• fixes math-comp#667 (math-comp#1127)

  

  affeldt-aist

  authored and

  proux01

  committed
  23499db

Commits on Jan 8, 2024

• [CI] Update Nix toolbox

  proux01

  committed
  903a339

• Redefine \min and \max in function_scope

  

  pi8027

  authored and

  proux01

  committed
  d2c1665

Commits on Jan 9, 2024

• rm dup lemmas (math-comp#1129)

  

  affeldt-aist

  authored and

  proux01

  committed
  cd6f8c0

• Radon-Nikodym chain rule (math-comp#1083)

  Show description for aed4ed5
  

  affeldt-aist

  authored and

  proux01

  committed
  aed4ed5

• format doc (math-comp#1130)

  Show description for 1fd0e85
  

  affeldt-aist

  authored and

  proux01

  committed
  1fd0e85

• restrain the scope of measurable args (math-comp#1116)

  Show description for 75650ef
  

  2 peopleauthored and

  proux01

  committed
  75650ef

• isolate the theory of lime_sup (math-comp#1121)

  Show description for 0e48333
  

  2 peopleauthored and

  proux01

  committed
  0e48333

• helper lemmas for contra (PR math-comp#1119) (math-comp#1136)

  Show description for 1ed1122
  

  2 peopleauthored and

  proux01

  committed
  1ed1122

• rm renaming warnings

  

  affeldt-aist

  authored and

  proux01

  committed
  65fcb33

• minimal changes to documentation to test coq2html (math-comp#1108)

  Show description for cb2be15
  

  affeldt-aist

  authored and

  proux01

  committed
  cb2be15

• Alternative form of Chernoff's bound (math-comp#1140)

  

  hoheinzollern

  authored and

  proux01

  committed
  f566876

• upd misc/uniform_bigO.v (math-comp#1142)

  

  affeldt-aist

  authored and

  proux01

  committed
  16891ad

• upd uniform_bigO.v

  

  affeldt-aist

  authored and

  proux01

  committed
  1c5d36e

• Changelog067 (math-comp#1143) (math-comp#1145)

  Show description for 186bd3c
  affeldt-aist

  authored
  186bd3c

Commits on Jan 15, 2024

• add HB instances (math-comp#1146)

  

  affeldt-aist

  authored and

  proux01

  committed
  aac80f4

• adapt to change in coq2html (math-comp#1148)

  

  affeldt-aist

  authored and

  proux01

  committed
  d1d2d70

Commits on Jan 17, 2024

• Redefine \min and \max in function_scope

  

  pi8027

  authored and

  proux01

  committed
  a9aa47b

Commits on Jan 20, 2024

• fixes math-comp#1131 (math-comp#1132)

  Show description for 592f514
  

  affeldt-aist

  authored and

  proux01

  committed
  592f514

• generalizations (math-comp#1147)

  Show description for 04975f7
  

  affeldt-aist

  authored and

  proux01

  committed
  04975f7

• Curry is continuous (math-comp#926)

  Show description for 71e2ede
  

  2 peopleauthored and

  proux01

  committed
  71e2ede

• Add contra tactics

  Show description for 7b1644a
  

  2 peopleauthored and

  proux01

  committed
  7b1644a

• Total variation (math-comp#1118)

  Show description for 9ba7c5b
  

  2 peopleauthored and

  proux01

  committed
  9ba7c5b

• changelog for version 0.7.0 (math-comp#1158)

  Show description for 9258582
  

  affeldt-aist

  authored and

  proux01

  committed
  9258582

Commits on Jan 22, 2024

• Merge remote-tracking branch 'origin/hierarchy-builder'

  affeldt-aist

  committed
  0a8b956

• fix

  Show description for 2ab529b
  affeldt-aist

  committed
  2ab529b

Commits on Jan 24, 2024

• changelog

  affeldt-aist

  committed
  5004eee

• upd of the doc

  affeldt-aist

  committed
  bfcfe58