hoeffding's inequality lemma definition#1698

Draft

hoheinzollern wants to merge 23 commits into

math-comp:masterfrom

hoheinzollern:hoeffding

Commits on Aug 14, 2025

hoeffding's inequality lemma definition
hoheinzollern
committed

Commits on Sep 22, 2025

simplify lemma lebesgue_measure_rat (#1700)

authored and
hoheinzollern
committed
fixes #1551 (move `isMeasurable` from `simple_functions.v` to `measure.v`) (#1695)

affeldt-aist
authored and
hoheinzollern
committed
Changelog for version 1.13.0 (#1701)

affeldt-aist
authored and
hoheinzollern
committed
Fix compilation on MC master with Rocq <= 9.1

proux01
authored and
hoheinzollern
committed
Update default bundle

proux01
authored and
hoheinzollern
committed
[CI] Test MC master on stable Rocq

proux01
authored and
hoheinzollern
committed
Make `cdf` an instance of `Cumulative` (fix #1572) (#1686)

authored and
hoheinzollern
committed
missing near lemma (#1699)

affeldt-aist
authored and
hoheinzollern
committed
Add section: Lebesgue-Stieltjes measure of cdf (#1689)

authored and
hoheinzollern
committed
add lemma cvg_addrl_Ny (#1716)

affeldt-aist
and
hoheinzollern
committed
continuous_big (#1706)

authored and
hoheinzollern
committed
two easy lemmas about inve

affeldt-aist
authored and
hoheinzollern
committed
`within_continuous_withinNx` (#1708)

authored and
hoheinzollern
committed
Add a parser/printer for extended-real integer constants (#1704)

proux01
authored and
hoheinzollern
committed
Closed ball0 20250911 (#1717)

affeldt-aist
authored and
hoheinzollern
committed
littleoE0 (#1707)

authored and
hoheinzollern
committed
add lemma lt0_adde (#1715)

affeldt-aist
and
hoheinzollern
committed
CI: :memo: :construction_worker: `make html` generate hierarchy graph (#1710)

yoshihiro503
authored and
hoheinzollern
committed
Divergence of the sum of the reciprocal of primes (#1705)

authored and
hoheinzollern
committed
Require MC >= 2.4.0

proux01
authored and
hoheinzollern
committed
Adapt to https://github.com/math-comp/math-comp/pull/1469

proux01
authored and
hoheinzollern
committed
skeleton
hoheinzollern
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

hoeffding's inequality lemma definition#1698

hoeffding's inequality lemma definition#1698
hoheinzollern wants to merge 23 commits into
math-comp:masterfrom
hoheinzollern:hoeffding

Commits on Aug 14, 2025

hoeffding's inequality lemma definition

Commits on Sep 22, 2025

simplify lemma lebesgue_measure_rat (#1700)

fixes #1551 (move `isMeasurable` from `simple_functions.v` to `measure.v`) (#1695)

Changelog for version 1.13.0 (#1701)

Fix compilation on MC master with Rocq <= 9.1

Update default bundle

[CI] Test MC master on stable Rocq

Make `cdf` an instance of `Cumulative` (fix #1572) (#1686)

missing near lemma (#1699)

Add section: Lebesgue-Stieltjes measure of cdf (#1689)

add lemma cvg_addrl_Ny (#1716)

continuous_big (#1706)

two easy lemmas about inve

`within_continuous_withinNx` (#1708)

Add a parser/printer for extended-real integer constants (#1704)

Closed ball0 20250911 (#1717)

littleoE0 (#1707)

add lemma lt0_adde (#1715)

CI: :memo: :construction_worker: `make html` generate hierarchy graph (#1710)

Divergence of the sum of the reciprocal of primes (#1705)

Require MC >= 2.4.0

Adapt to https://github.com/math-comp/math-comp/pull/1469

skeleton