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] - feat(measure_theory/function/conditional_expectation): define the conditional expectation of a function, prove the equality of integrals #9114

Closed
wants to merge 365 commits into from
Closed

[Merged by Bors] - feat(measure_theory/function/conditional_expectation): define the conditional expectation of a function, prove the equality of integrals #9114

wants to merge 365 commits into from

Conversation

RemyDegenne
Copy link
Collaborator

@RemyDegenne RemyDegenne commented Sep 9, 2021 •
edited
Loading

This PR puts together the generalized Bochner integral construction of #8939 and the set function condexp_ind of #8920 to define the conditional expectation of a function.

The equality of integrals that defines the conditional expectation is proven in set_integral_condexp.

Open in Gitpod

@RemyDegenne
Merge remote-tracking branch 'origin/master' into integral_norm
c2de830
@RemyDegenne
docstrings
b62880b
@RemyDegenne
generalize one lemma beyond R
ccec7ee
@RemyDegenne
use lt instead of ne
3bd742c
@RemyDegenne
change name
37f2f93
@RemyDegenne
Merge remote-tracking branch 'origin/master' into condexp_L2
a3b770c
@RemyDegenne
use measurable_set[m] notation
b5e87a8
@RemyDegenne
make a variable explicit
152d38c
@RemyDegenne
Merge remote-tracking branch 'origin/condexp_L2' into condexp_to_L1
e8bd13b
@RemyDegenne
Merge remote-tracking branch 'origin/integral_norm' into condexp_to_L1
1900b65
@RemyDegenne
integral of norm of condexp
8cd15da
@RemyDegenne
work on ae_eq_zero
b078f40
@RemyDegenne
unicity of condexp
648e558
@RemyDegenne
move things
680bf49
@RemyDegenne
strongly_measurable docstring
edfb19c
@RemyDegenne
move stuff
d98ce84
@RemyDegenne
move things
d69ea78
@RemyDegenne
simplify
5b4603e
@RemyDegenne
move
c7803e1
@RemyDegenne
fix
7014c31
@RemyDegenne
move mem_Lp.const_inner
044a70f
@RemyDegenne
fix
0ee4d95
@RemyDegenne
move integrable.const_inner
588c3a8
@RemyDegenne
fix
f5e8590
@RemyDegenne
add mem_Lp.re/im
7fd98b0
@RemyDegenne
add measurable.strongly_measurable
148cff3
@RemyDegenne
docstring
6737450
@RemyDegenne
docstring
fe5c914
@RemyDegenne
change strongly_measurable
c7d9778
@RemyDegenne
fix
fac81da
@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR 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 Sep 21, 2021
@RemyDegenne
Copy link
Collaborator Author

I changed the definition of condexp to make sure that m-measurable functions are sent to themselves. In order to prove that I still had μ[f|hm] =ᵐ[μ] condexp_L1 hm μ f, I had to prove results about the application of condexp_L1 and other functions to m-measurable functions.
The lemmas and definitions added are:

  • Lp_meas_to_Lp_trim, its inverse, and a couple results about it
  • Lp_meas_to_Lp_trim_lie which I introduced in a previous version, then dropped, but which is handy after all to prove results for Lp_meas by using Lp.induction on the Lp space of µ.trim hm
  • condexp_ind_of_measurable
  • condexp_L1_clm_of_ae_measurable'
  • condexp_L1_of_ae_measurable'

@RemyDegenne RemyDegenne 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 Sep 23, 2021
urkud
urkud reviewed Sep 24, 2021
View reviewed changes
Copy link
Member

@urkud urkud left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot for formalizing this!
I left a few minor comments about docstrings.

src/measure_theory/function/conditional_expectation.lean Show resolved Hide resolved
src/measure_theory/function/conditional_expectation.lean Show resolved Hide resolved
src/measure_theory/function/conditional_expectation.lean Show resolved Hide resolved
src/measure_theory/function/conditional_expectation.lean Show resolved Hide resolved
src/measure_theory/function/conditional_expectation.lean Outdated Show resolved Hide resolved
src/measure_theory/function/conditional_expectation.lean Show resolved Hide resolved
@urkud urkud 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 Sep 24, 2021
@urkud
Copy link
Member

urkud commented Sep 24, 2021

One more remark: could you please explain the role of 𝕜 in the module docstring?

@RemyDegenne RemyDegenne 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 Sep 24, 2021
@sgouezel
Copy link
Collaborator

bors r+
Thanks!!!

@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 Sep 24, 2021
bors bot pushed a commit that referenced this pull request Sep 24, 2021
@RemyDegenne
feat(measure_theory/function/conditional_expectation): define the con…
e14cf58 
…ditional expectation of a function, prove the equality of integrals (#9114)

This PR puts together the generalized Bochner integral construction of #8939 and the set function `condexp_ind` of #8920 to define the conditional expectation of a function.

The equality of integrals that defines the conditional expectation is proven in `set_integral_condexp`.
@bors
Copy link

bors bot commented Sep 24, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/function/conditional_expectation): define the conditional expectation of a function, prove the equality of integrals [Merged by Bors] - feat(measure_theory/function/conditional_expectation): define the conditional expectation of a function, prove the equality of integrals Sep 24, 2021
@bors bors bot closed this Sep 24, 2021
@bors bors bot deleted the condexp branch September 24, 2021 13:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@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
3 participants
@RemyDegenne @urkud @sgouezel