Counting distribution by lyonel2017 · Pull Request #2064 · math-comp/analysis

lyonel2017 · 2026-07-29T21:24:14Z

Motivation for this change

Porting the distr library from experimental_real in order to use esum (extracted from #2049).

Depends on #2062.

Checklist

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

Read this Checklist
Put a milestone if possible
Check labels

affeldt-aist · 2026-08-09T10:19:57Z

Note for later: check how le_esum_fine (and le_pos_esum_fine) are used and decide they are worth keeping

affeldt-aist · 2026-08-11T06:17:28Z

PR #2062 merged -> need rebasing

lyonel2017 · 2026-08-12T09:40:14Z

PR #2062 merged -> need rebasing

I made a rebase.

affeldt-aist · 2026-08-23T04:53:31Z

The CI is reporting a couple of errors, e.g.:

File "./theories/probability_theory/counting_distr.v", line 157, characters 0-36:
Error: The LHS of ge_ereal_sup
    (ereal_sup _ <= _)%E
does not match any subterm of the goal

lyonel2017 · 2026-08-24T09:02:43Z

A, I messed up something. I will fix this. If that's okay, I will make a few more changes. I started using this PR in a project, and there are things I don't like and/or that are poorly designed (mostly for dlim).

affeldt-aist · 2026-08-24T10:03:00Z

No problem (we still have to review #2063 beforehand anyway).

Don't hesitate to make micro PRs, especially if among the issues you spotted there are potential fixes to things that have already been merged in master (I am thinking about this PR #2062 we merged some time ago) because we are likely to make a release the end of the month.

lyonel2017 · 2026-08-26T17:12:04Z

I finish my changes (the issue where in the changes propose in #2064).

No problem (we still have to review #2063 beforehand anyway).

Review of #2063 does not necessary need to be done before #2064, except if we want to use result establish on lesbegue_integrale to do some simplification (if possible).

affeldt-aist · 2026-09-22T09:56:33Z

+HB.structure Definition Distribution (R : realType) (T : choiceType) :=
+  {f of @isDistribution R T f}.
+
+Notation "{ 'distr' T / R }" := (@Distribution.type R T)


What about adopting the notation R.-distr T? (There are already several datatypes whose notation follow this pattern in MathComp.)

affeldt-aist · 2026-09-22T09:58:21Z

+
+(* -------------------------------------------------------------------- *)
+Section Clamp.
+Context {R : realType}.


This type could be generalized to at least realFieldType and therefore this section is a candidate for PR to MathComp. It might go to unstable.v for a while but really MathComp looks like the right place.

I open a PR: #2106

affeldt-aist · 2026-09-22T10:00:09Z

+
+Implicit Types (mu : {distr T / R}) (A B E : pred T) (f : T -> R).
+
+Definition dinsupp mu := fun x => mu x != 0 :> R.


The notation of support does not need to be specialized to "distribution".

affeldt-aist · 2026-09-22T10:03:41Z

+
+Definition pr   mu E := fine (esum [set: T] (EFin \o (fun x => (E x)%:R * mu x))).
+Definition prc  mu E A := pr mu [predI E & A] / pr mu A.
+Definition esp  mu f   := fine (esum [set: T] (EFin \o (fun x => f x * mu x))).


Expectation is also defined in random_variable.v but for probability measure. It should maybe be generalized to subprobability measure so that the notation can be shared (provided "distributions" are shown to be subprobability measures, which they are).

affeldt-aist · 2026-09-22T10:05:48Z

+Section DistrTheory.
+Context {R : realType} {T : choiceType} (mu : T -> R).
+
+Definition isdistr :=


This might give raise to a "factory" in HB parlance: an alternative definition that is shown to produce a "distribution" by using HB.builder.

affeldt-aist · 2026-09-22T10:06:43Z

+
+Definition mkdistrd := @isDistribution.Build R T mu isd1 isd2 isd3.
+
+Definition ispredistr {T : choiceType} (mu : T -> R) :=


This could have been another mixin but it is actually not used in this PR.

affeldt-aist · 2026-09-22T10:08:51Z

+Section Restr.
+Context (R : realType) (T : choiceType) (p : pred T).
+
+Definition drestr_fun (mu : {distr T / R}) :=


It looks like this is redefining mrestr which is already in measure_function.v (and that would have come for free if "distributions" were shown to be (probability) measures).

affeldt-aist · 2026-09-22T10:11:22Z

+(* -------------------------------------------------------------------- *)
+(* Generic facts about [einfs] / [limn_einf] missing from sequences.v,  *)
+(* used below to make [dlim] total on sequences of subdistributions.    *)
+Lemma einfs_le {R : realType} (u : (\bar R)^nat) n m :


Maybe do a smaller PR with these facts to accelerate the review process.

I open a PR: #2107

affeldt-aist added this to the 1.18.0 milestone Jul 30, 2026

affeldt-aist force-pushed the master branch from 6e121ed to 219890d Compare July 30, 2026 05:56

lyonel2017 force-pushed the feature-counting-distribution branch 2 times, most recently from c83d705 to 3855cd8 Compare August 3, 2026 18:33

lyonel2017 force-pushed the feature-counting-distribution branch from 3855cd8 to ac892f5 Compare August 11, 2026 11:41

lyonel2017 and others added 3 commits August 26, 2026 11:41

Counting distribution

24961a6

Some cleanup

9fe9a50

Some refactoring for dlim

2bf37db

lyonel2017 force-pushed the feature-counting-distribution branch from fafee44 to 2bf37db Compare August 26, 2026 11:10

affeldt-aist modified the milestones: 1.18.0, 1.19.0 Aug 30, 2026

lyonel2017 mentioned this pull request Sep 1, 2026

Add mutual recusive function, and replace the use of experimental_real by counting_distr formosa-crypto/xhl#5

Draft

affeldt-aist reviewed Sep 22, 2026

View reviewed changes

lyonel2017 marked this pull request as draft September 23, 2026 14:17

This was referenced Sep 23, 2026

Add generic facts about einfs and limn_einf #2107

Open

Add function to restrict a real to the intervale [0 , 1] #2106

Open


		Implicit Types (mu : {distr T / R}) (A B E : pred T) (f : T -> R).

		Definition dinsupp mu := fun x => mu x != 0 :> R.


		Definition mkdistrd := @isDistribution.Build R T mu isd1 isd2 isd3.

		Definition ispredistr {T : choiceType} (mu : T -> R) :=

Conversation

lyonel2017 commented Jul 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation for this change

Checklist

Reminder to reviewers

Uh oh!

affeldt-aist commented Aug 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

affeldt-aist commented Aug 11, 2026

Uh oh!

lyonel2017 commented Aug 12, 2026

Uh oh!

affeldt-aist commented Aug 23, 2026

Uh oh!

lyonel2017 commented Aug 24, 2026

Uh oh!

affeldt-aist commented Aug 24, 2026

Uh oh!

lyonel2017 commented Aug 26, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Sep 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

lyonel2017 commented Jul 29, 2026 •

edited

Loading

affeldt-aist commented Aug 9, 2026 •

edited

Loading

affeldt-aist Sep 22, 2026 •

edited

Loading