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

RemyDegenne · 2021-09-09T13:33:13Z

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.

depends on: [Merged by Bors] - feat(measure_theory/integral/bochner): generalize the Bochner integral construction #8939
depends on: [Merged by Bors] - feat(measure_theory/function/conditional_expectation): conditional expectation of an indicator #8920
depends on: [Merged by Bors] - chore(measure_theory/integral/set_integral): update old lemmas that were in comments at the end of the file #9111
depends on: [Merged by Bors] - feat(measure_theory/integral/set_to_L1): image of an indicator by set_to_fun (and related functions) #9205
depends on: [Merged by Bors] - feat(measure_theory/function/conditional_expectation): condexp_ind is ae_measurable' #9263

RemyDegenne · 2021-09-23T07:29:43Z

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'

urkud

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

src/measure_theory/function/conditional_expectation.lean

urkud · 2021-09-24T04:51:52Z

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

sgouezel · 2021-09-24T12:21:24Z

bors r+
Thanks!!!

…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 · 2021-09-24T13:48:25Z

Pull request successfully merged into master.

Build succeeded:

RemyDegenne added 30 commits July 14, 2021 18:27

Merge remote-tracking branch 'origin/master' into integral_norm

c2de830

docstrings

b62880b

generalize one lemma beyond R

ccec7ee

use lt instead of ne

3bd742c

change name

37f2f93

Merge remote-tracking branch 'origin/master' into condexp_L2

a3b770c

use measurable_set[m] notation

b5e87a8

make a variable explicit

152d38c

Merge remote-tracking branch 'origin/condexp_L2' into condexp_to_L1

e8bd13b

Merge remote-tracking branch 'origin/integral_norm' into condexp_to_L1

1900b65

integral of norm of condexp

8cd15da

work on ae_eq_zero

b078f40

unicity of condexp

648e558

move things

680bf49

strongly_measurable docstring

edfb19c

move stuff

d98ce84

move things

d69ea78

simplify

5b4603e

move

c7803e1

fix

7014c31

move mem_Lp.const_inner

044a70f

fix

0ee4d95

move integrable.const_inner

588c3a8

fix

f5e8590

add mem_Lp.re/im

7fd98b0

add measurable.strongly_measurable

148cff3

docstring

6737450

docstring

fe5c914

change strongly_measurable

c7d9778

fix

fac81da

RemyDegenne added awaiting-review awaiting-author and removed awaiting-review labels Sep 21, 2021

RemyDegenne added 2 commits September 23, 2021 09:19

change definition of condexp

e045dfd

spaces

fc4c656

RemyDegenne added awaiting-review and removed awaiting-author labels Sep 23, 2021

RemyDegenne added 2 commits September 23, 2021 09:33

lint

86348e2

make sure the notation works outside of measure_theory

8cd0d59

urkud reviewed Sep 24, 2021

View reviewed changes

urkud added awaiting-author and removed awaiting-review labels Sep 24, 2021

Move neg after smul, use smul in the proof

3e5a032

RemyDegenne added 5 commits September 24, 2021 09:29

some docstrings and ae_eq_condexp_of...

9ec0449

add simp

aec2be4

docstrings

6861cc0

fix

bfea8f2

add implementation note about k

735a033

RemyDegenne added awaiting-review and removed awaiting-author labels Sep 24, 2021

github-actions bot added ready-to-merge and removed awaiting-review labels Sep 24, 2021

bors bot closed this Sep 24, 2021

bors bot deleted the condexp branch September 24, 2021 13:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

RemyDegenne commented Sep 9, 2021 •

edited

Loading

RemyDegenne commented Sep 23, 2021

urkud left a comment

urkud commented Sep 24, 2021

sgouezel commented Sep 24, 2021

bors bot commented Sep 24, 2021

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

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

Conversation

RemyDegenne commented Sep 9, 2021 • edited Loading

RemyDegenne commented Sep 23, 2021

urkud left a comment

Choose a reason for hiding this comment

urkud commented Sep 24, 2021

sgouezel commented Sep 24, 2021

bors bot commented Sep 24, 2021

RemyDegenne commented Sep 9, 2021 •

edited

Loading