average): Lebesgue average
#19199

Closed

[Merged by Bors] - feat(measure_theory/integral/average): Lebesgue average #19199

YaelDillies wants to merge 7 commits into master from laverage

feat(measure_theory/integral/average): Lebesgue average

6e7ee32d

YaelDillies requested a review 2 years ago

YaelDillies added awaiting-review

YaelDillies added t-measure-probability

YaelDillies added modifies-synchronized-file

kex-y commented on 2023-06-18

Jason's suggestions

cbbbbef3

rewrap

adf08703

sgouezel commented on 2023-06-18

sgouezel commented on 2023-06-19

sgouezel removed awaiting-review

sgouezel added awaiting-author

generalise measure_set_laverage_le_pos

88b97625

YaelDillies removed awaiting-author

YaelDillies added awaiting-review

sgouezel commented on 2023-06-20

sgouezel removed awaiting-review

sgouezel added awaiting-author

more ∞

9ea98e90

YaelDillies removed awaiting-author

YaelDillies added awaiting-review

kex-y commented on 2023-06-20

kex-y removed awaiting-review

kex-y added awaiting-author

Update src/measure_theory/integral/average.lean

b8b76549

YaelDillies removed awaiting-author

YaelDillies added awaiting-review

remove useless arguments

dd154864

sgouezel commented on 2023-06-21

leanprover-community-bot-assistant added ready-to-merge

leanprover-community-bot-assistant removed awaiting-review

bors changed the title ~~feat(measure_theory/integral/average): Lebesgue average~~ [Merged by Bors] - feat(measure_theory/integral/average): Lebesgue average 2 years ago

bors closed this 2 years ago

bors deleted the laverage branch 2 years ago

Reviewers

sgouezel

kex-y

Assignees

No one assigned

Labels

ready-to-merge t-measure-probability modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - feat(measure_theory/integral/average): Lebesgue average #19199 Closed

[Merged by Bors] - feat(measure_theory/integral/average): Lebesgue average #19199

mathlib3
[Merged by Bors] - feat(measure_theory/integral/average): Lebesgue average
#19199

Closed