Takafumi Saikawa

Results 60 comments of Takafumi Saikawa

Expectation lmodType lemmas

rebased

Lemmas `fiberwise_{finite,countable}_preimage`

TODO: 1. create a renaming PR : finite_preimage -> finite_inj_preimage 2. redo this PR

generic lemma to be more elsewhere

can you suggest a better name?

fix coercions from prob to algebraic structures

turned into a draft until I figure out how to handle mc master

Fix interaction of or-patterns, GADTs and as-patterns

PR #14327 is weakly related to this one (touching the same function).

Generalize integration_by_parts

I suggest keeping 4 lemmas as is, and additionally, provide a unified interface lemma that use the constant_sign predicate

Expand the notation `{within _, _ _}`?

that notion seems to deserve a definition and a notation. what about generalizing it a bit as "continuous within X and derivable in the interior of X" for any set...

Expand the notation `{within _, _ _}`?

(though derivability needs more structure than just topology, so it will not actually be "any" topological space. manifolds?)

`notP` is defined twice

> fyi @t6s the former looks internal to contra, thus not meant to be exported, while the latter looks like a misnomer since it is about double negations

`notP` is defined twice

> fyi @t6s the former looks internal to contra, thus meant to be exported, while the latter looks like a misnomer since it is about double negations