mathlib

mathlib copied to clipboard

This generalizes `multilinear_map.dom_coprod` to maps with non-uniform argument types, at the expense of introducing unpleasant `sum.elim M N` pi-types --- [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/The.20tensor.20product.20of.20two.20multilinear.20maps.20is.20a.20multiline.2E.2E.2E/near/218474366)

eric-wieser

feat(probability/subgaussian): define sub-Gaussian random variables

3

Define sub-Gaussian random variables and prove Hoeffding's inequality. --- - [x] depends on: #15140 [](https://gitpod.io/from-referrer/)

RemyDegenne

refactor(set_theory/cardinal/basic): constrain universes

12

We enforce a canonical way to compare cardinals `a` and `b` of different universes `u` and `v`, namely to compare `cardinal.lift.{v} a` and `cardinal.lift.{u} b`. By doing this, we alleviate...

vihdzp

feat(data/polynomial/root_isolation): root_parity_in_range_of_evals

1

A PR to prove that the parity of the number of roots of a real polynomial in a range depends on the signs of the evaluations of the polynomial on...

BoltonBailey

TODO: merge master once #16543 is merged. --- [](https://gitpod.io/from-referrer/)

urkud

feat(probability/tail_prob): the tail probability formula

1

This PR adds the tail probability formula which is needed for Doob's Lp inequality. --- [](https://gitpod.io/from-referrer/)

kex-y

feat(data/int|nat/modeq): add modneq notation

2

Add notation for `≢ ` in modeq files. --- [](https://gitpod.io/from-referrer/)

oxarbitrage

feat(algebra/module/polynomial): Modules over `R[X]`

4

A `R[X]`-module is a `R`-module with the additional data of a `R`-linear endomorphism, describing the action of `X`. --- [](https://gitpod.io/from-referrer/)

pbazin

feat(set_theory/game/pgame): notation and basic API for `P{x | y}`, `P{x |}`, `P{| x}`

1

We introduce constructors for games `P{x | y}`, `P{x |}`, `P{| x}` and provide a basic API. We also make `1` and `star` reducible, which allows us to remove redundant...

vihdzp

feat(topology,analysis): add the discrete metric and normed spaces

6

These are provided as definitions for now, but in future might be reasonable to associate with a type synonym. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Discrete.20metric.2E/near/281044832) --- - [x] depends on: #13927 - [x] depends on:...

eric-wieser