Takafumi Saikawa
Takafumi Saikawa
proba_monad_model.v uses another form of convA that is also specific to fsdist: fsdist_convA. This PR replaces it by its generic version convA0. I intend to remove fsdist_convA from infotheo as...
This PR adds a definition of abstract categories extending category.v. Due to shortcomings in the constraint solver for universes in Coq, this could only be done only for the impredicative...
This draft PR moves category theory from monae to infotheo, rebasing all algebraic structures (eg convex spaces) in infotheo over it. Suggestion by @CohenCyril
This PR removes assignments to `Ctype.current_level` except for those in `begin/end_def` API.
https://github.com/math-comp/analysis/blob/95daf6f73fd773414be3a0878aa0ba0aa6989231/theories/probability.v#L20 https://github.com/math-comp/analysis/blob/95daf6f73fd773414be3a0878aa0ba0aa6989231/theories/probability.v#L70 The header documentation says `distribution` takes only one argument `X : {RV P >-> R}`, but its actual definition requires two arguments `P : probability T R` and...
##### Motivation for this change As a user of Zorn, I sometimes want to have a maximal element over a specified point in the target poset. This PR adds that...
We want to have a measurable space structure on countable products of measurable spaces. It would be useful in formalizations of probability theory and statistics. Some pointers: - https://arxiv.org/pdf/2212.07246.pdf ,...
https://github.com/affeldt-aist/infotheo/blob/ee75502025e9fb5b988b025521aabab6f849b2e9/probability/fdist.v#L73 https://github.com/math-comp/analysis/blob/95daf6f73fd773414be3a0878aa0ba0aa6989231/theories/sequences.v#L100 Because of this conflict, these two files cannot be imported at the same time.
The following expression fails to be parsed after importing both proba.v (infotheo) and probability.v (mathcomp-analysis): ``` Local Open Scope form_scope. Variables (d : measure_display) (T : measurableType d) (R :...