alternative proof of gauss integral#1584

Closed

IshiguroYoshihiro wants to merge 55 commits intomath-comp:masterfrom

IshiguroYoshihiro:gauss_integral_alternative_20250422

Commits on Apr 22, 2025

Commits on Apr 24, 2025

Commits on Jun 3, 2025

Commits on Jun 4, 2025

add changelog
IshiguroYoshihiro
committed

Commits on Jun 20, 2025

fixes #1586 (#1587)

affeldt-aist
authored and
IshiguroYoshihiro
committed
typos (#1588)

affeldt-aist
authored and
IshiguroYoshihiro
committed
Adapt to https://github.com/math-comp/math-comp/pull/1354

proux01
authored and
IshiguroYoshihiro
committed
generic lemmas from the prob_lang PR (#1583)

authored and
IshiguroYoshihiro
committed
lemma extracted from the sampling branch to help rebasing (#1592)

affeldt-aist
authored and
IshiguroYoshihiro
committed
[opam] Add upper bound on MC

proux01
authored and
IshiguroYoshihiro
committed
Fix coqc in Makefile (#1596)

proux01
authored and
IshiguroYoshihiro
committed
Measurable realfun 20250430 (#1597)

authored and
IshiguroYoshihiro
committed
is_derive1_powR (#1566)
IshiguroYoshihiro
committed
Add Lemma `cvge_ninftyP` (#1591)

Yosuke-Ito-345
authored and
IshiguroYoshihiro
committed
Port of lemmas in classical from lspace master (#1598)`

authored and
IshiguroYoshihiro
committed
minor generalization

affeldt-aist
authored and
IshiguroYoshihiro
committed
avoid Program Definition

affeldt-aist
authored and
IshiguroYoshihiro
committed
natmulfctE

affeldt-aist
authored and
IshiguroYoshihiro
committed
lemmas on ereal.v from lspace_master (#1599)

authored and
IshiguroYoshihiro
committed
generalized `measurable_ln` (#1602)

authored and
IshiguroYoshihiro
committed
rm warnings (#1605)

affeldt-aist
authored and
IshiguroYoshihiro
committed
expe lemmas (#1604)

authored and
IshiguroYoshihiro
committed
fixes #1292

affeldt-aist
authored and
IshiguroYoshihiro
committed
fixes #1590

affeldt-aist
authored and
IshiguroYoshihiro
committed
lemmas from the lspace_master PR

authored and
IshiguroYoshihiro
committed
changelog for version 1.11.0

affeldt-aist
authored and
IshiguroYoshihiro
committed
almost everywhere equality (#1600)

authored and
IshiguroYoshihiro
committed
cleanup README / INSTALL instructions (#1619)

hoheinzollern
authored and
IshiguroYoshihiro
committed
[CI] Update

proux01
authored and
IshiguroYoshihiro
committed
[CI] Disactivate currently broken generate_doc

proux01
authored and
IshiguroYoshihiro
committed
Essential supremum (#1606)

authored and
IshiguroYoshihiro
committed
CI: Rocqnavi released version (#1614)

yoshihiro503
authored and
IshiguroYoshihiro
committed
Minor cleanup (#1625)

pi8027
authored and
IshiguroYoshihiro
committed
Fix the affiliation of Kazuhiko Sakaguchi in AUTHORS.md

pi8027
authored and
IshiguroYoshihiro
committed
adapt to rocq#19987 (#1532)

Tragicus
authored and
IshiguroYoshihiro
committed
fixes #1632 (#1633)

affeldt-aist
authored and
IshiguroYoshihiro
committed
Conv convention (#1630)

authored and
IshiguroYoshihiro
committed
Repair structure names in tvs.v (#1631)

Tragicus
authored and
IshiguroYoshihiro
committed
ereal inverse + simplification mule and mule_def (#1494)

authored and
IshiguroYoshihiro
committed
:memo: :wrench: `make html` to make the html documentation (#1622)

yoshihiro503
authored and
IshiguroYoshihiro
committed
pseudometric alias (#1628)

authored and
IshiguroYoshihiro
committed
`is_deriveX`: is that a generalization? (#1637)

authored and
IshiguroYoshihiro
committed
exponential distribution (#1635)

affeldt-aist
and
IshiguroYoshihiro
committed
expR_ge1Dxn (#1638)
IshiguroYoshihiro
committed
measurability for tuples (#1618)

authored and
IshiguroYoshihiro
committed
lemmas for integrals on increasing set sequences (#1579)

IshiguroYoshihiro
and
affeldt-aist
committed
CHANGELOG
IshiguroYoshihiro
committed
add changelog
IshiguroYoshihiro
committed
rename
IshiguroYoshihiro
committed
fix
IshiguroYoshihiro
committed
cleaning
IshiguroYoshihiro
committed