leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/RD_subgaussian' into RD_bounded_subg

RemyDegenne committed 3 years ago

0f922a2a

Merge remote-tracking branch 'origin/RD_mgf_sum' into RD_subgaussian

RemyDegenne committed 3 years ago

5306d1e8

RemyDegenne committed 3 years ago

50dca103

RemyDegenne committed 3 years ago

880a3e29

move to_real_prob_le_one

RemyDegenne committed 3 years ago

ae1645cf

RemyDegenne committed 3 years ago

a4d9a518

RemyDegenne committed 3 years ago

1e2e5d00

RemyDegenne committed 3 years ago

650cbacb

feat(geometry/manifold/local_invariant_properties): simplify definitions and proofs (#15116)

fpvandoorn committed 3 years ago

f09322bc

add file docstring

RemyDegenne committed 3 years ago

3449effa

RemyDegenne committed 3 years ago

d4c2ec6b

move sum lemmas up

RemyDegenne committed 3 years ago

6834b24a

remove subgaussian

RemyDegenne committed 3 years ago

617de097

Merge remote-tracking branch 'origin/RD_subgaussian' into RD_mgf_sum

RemyDegenne committed 3 years ago

b20788e8

RemyDegenne committed 3 years ago

26f5e263

feat(analysis/special_functions/complex/arg): add complex.abs_eq_one_iff (#15125)

Ruben-VandeVelde committed 3 years ago

8ff5e113

chore(data/fintype): drop a `decidable_pred` assumption (#14971)

urkud committed 3 years ago

d908bc0b

feat(probability/martingale): Doob's maximal inequality (#14737)

kex-y committed 3 years ago

a95b4427

doc(overview): add probability theory (#15114)

fpvandoorn committed 3 years ago

bd9c307d

feat(analysis/convex/function): Variants of `convex_on.le_right_of_left_le` (#14821)

tb65536 committed 3 years ago

93e97d1e

chore(analysis/normed/field/basic): add `@[simp]` to `real.norm_eq_abs (#15006)

urkud committed 3 years ago

71e11de8

feat(probability/martingale): positive part of a submartingale is also a submartingale (#14932)

kex-y committed 3 years ago

071dc908

replace big rw by tactics

RemyDegenne committed 3 years ago

f0ab1d51

feat(*): add lemmas about sigma types (#15085)

urkud committed 3 years ago

f10d0abc

RemyDegenne committed 3 years ago

1a0618f2

version with mean instead of sum

RemyDegenne committed 3 years ago

88bbb832

feat(topology/sets/compacts): prod constructions (#15118)

sgouezel committed 3 years ago

527afb3d

RemyDegenne committed 3 years ago

6d96d0eb

remove pos hypothesis

RemyDegenne committed 3 years ago

7e8f9433

feat(analysis/complex): equiv_real_prod_symm_apply (#15122)

sgouezel committed 3 years ago

db9cb466

Older