Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(measure_theory/set_integral): use weaker assumptions here and there #5647

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(measure_theory/set_integral): use weaker assumptions here and there #5647

wants to merge 4 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jan 6, 2021

  • use ae_measurable f (μ.restrict s) in more lemmas;
  • introduce measurable_at_filter and use it.

@urkud urkud added the awaiting-review The author would like community review of the PR label Jan 6, 2021
@urkud urkud requested a review from sgouezel January 6, 2021 17:59
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 8, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 8, 2021
sgouezel
sgouezel reviewed Jan 9, 2021
View reviewed changes
src/measure_theory/set_integral.lean Show resolved Hide resolved
src/measure_theory/set_integral.lean Show resolved Hide resolved
src/measure_theory/set_integral.lean Outdated Show resolved Hide resolved
src/measure_theory/set_integral.lean Show resolved Hide resolved
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 9, 2021
@urkud urkud added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 9, 2021
@sgouezel
Copy link
Collaborator

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 10, 2021
bors bot pushed a commit that referenced this pull request Jan 10, 2021
@urkud
chore(measure_theory/set_integral): use weaker assumptions here and t…
db33c31 
…here (#5647)

* use `ae_measurable f (μ.restrict s)` in more lemmas;
* introduce `measurable_at_filter` and use it.
@bors
Copy link

bors bot commented Jan 10, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 10, 2021
@urkud
chore(measure_theory/set_integral): use weaker assumptions here and t…
bcdba33 
…here (#5647)

* use `ae_measurable f (μ.restrict s)` in more lemmas;
* introduce `measurable_at_filter` and use it.
@bors
Copy link

bors bot commented Jan 10, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 10, 2021
@urkud
chore(measure_theory/set_integral): use weaker assumptions here and t…
62c1912 
…here (#5647)

* use `ae_measurable f (μ.restrict s)` in more lemmas;
* introduce `measurable_at_filter` and use it.
@bors
Copy link

bors bot commented Jan 10, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(measure_theory/set_integral): use weaker assumptions here and there [Merged by Bors] - chore(measure_theory/set_integral): use weaker assumptions here and there Jan 10, 2021
@bors bors bot closed this Jan 10, 2021
@bors bors bot deleted the ae-measurable-more branch January 10, 2021 22:38
Julian added a commit that referenced this pull request Jan 12, 2021
@Julian
Merge remote-tracking branch 'origin/master' into freek-45
2be7703 
* origin/master: (751 commits)
  chore(topology/algebra/infinite_sum): speedup has_sum_sum (#5710)
  feat(submonoid/basic): subsingleton and nontrivial instances for {add_,}submonoid (#5690)
  docs(undergrad.yaml): analysis updates (#5675)
  feat(linear_algebra/multilinear_map): Add `range` and `map` (#5658)
  feat(measure_theory): each set has a measurable superset of the same measure (#5688)
  feat(data/set/intervals): add 2 Icc ssubset lemmas (#5617)
  chore(category_theory/limits): move constructions folder (#5681)
  fix(linear_algebra/tensor_product): Remove the priorities from the module structure (#5667)
  chore(category_theory/limits/over): generalise, golf and document over limits (#5674)
  chore(scripts): update nolints.txt (#5705)
  feat(measure_theory/pi): `ae_eq` lemmas about intervals in `Π i, α i` (#5633)
  feat(algebra/splitting_field): Restrict to splitting field (#5562)
  chore(scripts): update nolints.txt (#5699)
  feat(analysis/special/functions/trigonometric): complex trig and some even/odd lemmas (#5404)
  feat(equiv|set|topology): various additions (#5656)
  chore(measure_theory/set_integral): use weaker assumptions here and there (#5647)
  feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687)
  feat(order/complete_well_founded): characterise well-foundedness for complete lattices (#5575)
  chore(order/filter): a few more lemmas about `eventually` and set operations (#5686)
  chore(order/filter/basic): a few `simp` lemmas (#5685)
  feat(data/equiv/basic, logic/embedding): swap commutes with injective functions (#5636)
  chore(scripts): update nolints.txt (#5682)
  feat(algebra/lie/basic): Lie ideal operations are linear spans (#5676)
  feat(measure_theory/lp_space): add more lemmas about snorm (#5644)
  chore(data/set/lattice): add a few simp lemmas (#5671)
  feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523)
  feat(topology/algebra/ordered): prove `tendsto.Icc` for pi-types (#5639)
  chore(scripts): update nolints.txt (#5673)
  feat(category_theory/limits): preserving pullbacks (#5668)
  chore(linear_algebra/alternating): golf a proof (#5666)
  chore(algebra/group/hom): fix additive version of docstring (#5660)
  chore(analysis/special_functions/trigonometric): adding `@[pp_nodot]` to complex.log (#5670)
  feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets (#5410)
  feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat (#5645)
  feat(geometry/manifold/times_cont_mdiff): API for checking `times_cont_mdiff` (#5631)
  feat(category_theory/closed): Frobenius reciprocity of cartesian closed categories (#5624)
  feat(measure_theory/measure_space): ae_measurable and measurable are equivalent for complete measures (#5643)
  refactor(linear_algebra/alternating): Use unapplied maps when possible (#5648)
  chore(algebra/ordered_monoid): rename lemmas (#5657)
  feat(measure_theory/borel_space): locally finite measure is sigma finite (#5634)
  refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654)
  feat(topology/algebra): add additive/multiplicative instances (#5662)
  chore(scripts): update nolints.txt (#5661)
  feat(measure_theory): some additions (#5653)
  chore(data/list/basic): tag mmap(') with simp (#5443)
  feat(category_theory/sites): category of sheaves on the trivial topology  (#5651)
  feat(category_theory/monad): reflector preserves terminal object (#5649)
  feat(measure_theory/borel_space): a compact set has finite measure (#5628)
  feat(category_theory/closed): golf definition and proofs (#5623)
  feat(category_theory/limits): the product comparison natural transformation (#5621)
  ...
@benjamindavidson benjamindavidson mentioned this pull request Jan 14, 2021
Closed
@hrmacbeth hrmacbeth mentioned this pull request Jan 14, 2021
Closed
b-mehta pushed a commit that referenced this pull request Jan 16, 2021
@urkud @b-mehta
chore(measure_theory/set_integral): use weaker assumptions here and t…
18c3b1d 
…here (#5647)

* use `ae_measurable f (μ.restrict s)` in more lemmas;
* introduce `measurable_at_filter` and use it.
bors bot pushed a commit that referenced this pull request Jan 21, 2021
@benjamindavidson
feat(measure_theory/interval_integral): FTC-2 for the open set (#5733)
d66d563 
A follow-up to #4945. I replaced `integral_eq_sub_of_has_deriv_at'` with a stronger version that holds for functions that have a derivative on an `Ioo` (as opposed to an `Ico`). Inspired by [this](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/FTC-2.20on.20open.20set/near/222177308) conversation on Zulip.

I also emended docstrings to reflect changes made in #5647.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@urkud @sgouezel