Commits leanprover-community/mathlib3

start with covariance estim

abentkamp committed 3 years ago

2039115e

feat(analysis/normed/group/basic): add `norm_multiset_sum_le` (#16419)

astrainfinita committed 3 years ago

75cc1ae9

feat(order/upper_lower): `Iic` is not bounded below (#16425)

YaelDillies committed 3 years ago

ba346d8b

feat(number_theory/legendre_symbol/jacobi_symbol): add new file with the definition and properties of the Jacobi symbol (#16395)

MichaelStollBayreuth committed 3 years ago

d2d66526

refactor(data/{finite,fintype}): redefine `infinite` in terms of `finite`, move to `data.finite.defs` (#16390)

urkud committed 3 years ago

662786a8

feat(combinatorics/young_diagram): add transposes, rows and columns of Young diagrams (#16120)

jakelev committed 3 years ago

e0bdbbe1

feat(ring_theory/dedekind_domain/integer_unit): define S-integers and S-units (#15646)

Multramate committed 3 years ago

00ab7761

feat(combinatorics/simple_graph/triangle/basic): add ε-triangle-free far graph predicate (#12988)

YaelDillies committed 3 years ago

cd7f0626

feat(analysis/calculus/uniform_limits_deriv): Swap limits and derivatives (#14090)

khwilson committed 3 years ago

d645d0e8

chore(algebra/big_operators/basic): golf (#16427)

astrainfinita committed 3 years ago

aff61c0f

fix(data/nat/interval): do not dedup when implementing `finset.Icc` etc (#16423)

eric-wieser committed 3 years ago

d75314b3

feat(algebra/big_operators/multiset): add `prod_map_le_prod_map` (#16418)

astrainfinita committed 3 years ago

370dabe7

fix(*): fix padding around notations (#16333)

digama0 committed 3 years ago

a0735864

feat(analysis/schwartz): Definition of the Schwartz space (#15850)

mcdoll committed 3 years ago

4c0aa6e7

feat(number_theory/modular_forms/congruence_subgroups): Add definition of congruence subgroups. (#15159)

CBirkbeck committed 3 years ago

9b6eef6e

fix(algebra/big_operators/multiset): rename `prod_le_sum_prod` to `prod_le_prod_map` (#16420)

astrainfinita committed 3 years ago

572e54ab

chore(measure_theory/function/conditional_expectation): change the definition of `condexp` (#16325)

RemyDegenne committed 3 years ago

fd5d3068

feat(analysis/convex/gauge): unit ball of the gauge seminorm (#16413)

ADedecker committed 3 years ago

5ebb7d87

chore(data/finset/basic): generalize `finset.nonempty_mk_coe` to `nonempty_mk` (#16399)

urkud committed 3 years ago

ed4882b1

feat(order/max): equivalence of no_top_order and no_max_order for linear orders (#16341)

RemyDegenne committed 3 years ago

019df1c0

feat(analysis/normed/group/add_torsor): `normed_add_torsor` instance for `affine_subspace` (#16339)

jsm28 committed 3 years ago

eae1ec81

feat(analysis/seminorm): `restrict_scalars` for seminorms (#16401)

ADedecker committed 3 years ago

56e4f0d5

feat(group_theory/subgroup/basic): Centralizer of closure is intersection of centralizers (#16394)

tb65536 committed 3 years ago

13c6c437

feat(analysis/complex/upper_half_plane): Functions bounded at infinity (#15009)

CBirkbeck committed 3 years ago

62119451

feat(data/polynomial/degree/definitions): add `degree_X_sub_C_le` (#16404)

astrainfinita committed 3 years ago

41626f7d

feat(order/interval): Order intervals (#14807)

YaelDillies committed 3 years ago

63014d26

docs(data/polynomial/ring_division, field_theory/splitting_field): update docs (#16406)

astrainfinita committed 3 years ago

9362a5b5

feat(linear_algebra/matrix): A positive definite matrix has a positive determinant (#16376)

abentkamp committed 3 years ago

914d4216

chore(scripts): update nolints.txt (#16409)

leanprover-community-bot committed 3 years ago

18cf2ca3

feat(topology/sheaves/*): sheafification preserves zero morphisms (#16381)

jjaassoonn committed 3 years ago

a0d1a84d