leanprover-community/mathlib

Pull Requests Commits

chore(measure_theory/function/lp_space): split file

eric-wieser committed 2 years ago

baf5306c

norm version of lemma

eric-wieser committed 2 years ago

606cf2d5

actually fix the downstream file

eric-wieser committed 2 years ago

4e141189

eric-wieser committed 2 years ago

2dbf55cf

remove lipschitz results

eric-wieser committed 2 years ago

fa997957

eric-wieser committed 2 years ago

ba1c0d4a

Merge remote-tracking branch 'origin/master' into eric-wieser/lp_space-bounded

eric-wieser committed 2 years ago

252f10d2

remove headin to aid with merge

eric-wieser committed 2 years ago

8fdcc0f5

Generalize Hölder's inequality

eric-wieser committed 2 years ago

9f74146b

eric-wieser committed 2 years ago

1e458c60

feat(analysis/calculus/bump_function_inner): add `real.smooth_transition.proj_Icc` (#19097)

urkud committed 2 years ago

42e9a1fd

chore(topology/continuous_function/ideals): generalize type class requirements (#19093)

j-loreaux committed 2 years ago

c2258f7b

chore(measure_theory/function/lp_space): add and reorder monotonicity results (#19092)

eric-wieser committed 2 years ago

d2d14e72

feat(data/real/basic): add `real.supr_nonneg` etc (#19096)

urkud committed 2 years ago

cb425931

feat(topology/{maps,separation}): add lemmas about closed and quotient maps (#19071)

urkud committed 2 years ago

d91e7f7a

doc(analysis/complex/arg): fix docs (#19095)

ericrbg committed 2 years ago

45a46f4f

feat(analysis/special_functions/exponential): derivative of `u ↦ exp 𝕂 (u • x)` (#19062)

eric-wieser committed 2 years ago

e1a18cad

feat(algebra/homology/local_cohomology): just the definition (#19061)

emwitt committed 2 years ago

5a684ce8

eric-wieser committed 2 years ago

1c6a1c4f

feat(analysis/normed_space/lp_space): generalize from normed_field to `normed_ring` (#19085)

eric-wieser committed 2 years ago

de83b437

more helper lemmas

eric-wieser committed 2 years ago

7a1dcc12

Merge remote-tracking branch 'origin/staging' into eric-wieser/lp_space-bounded

eric-wieser committed 2 years ago

2cd1357b

chore(measure_theory/function/lp_space): add nnnorm lemmas (#19091)

eric-wieser committed 2 years ago

6480bedf

eric-wieser committed 2 years ago

dc035620

eric-wieser committed 2 years ago

b92c3da1

chore(*): add mathlib4 synchronization comments (#19089)

leanprover-community-bot committed 2 years ago

a87d2257

feat(linear_algebra/span): generalise to_span_nonzero_singleton (#19082)

Multramate committed 2 years ago

10878f6b

fix: bump to Lean 3.51.1 (#19088)

eric-wieser committed 2 years ago

96d2ccbe

eric-wieser committed 2 years ago

c3357531

feat(measure_theory/function/strongly_measurable/basic): generalize to `is_unit c` from `c ≠ 0` (#19081)

eric-wieser committed 2 years ago

ef95945c

Older