[Merged by Bors] - feat(ProbabilityTheory): Conditional Jensen's Inequality by CoolRmal · Pull Request #27953 · leanprover-community/mathlib4

CoolRmal · 2025-08-04T21:27:02Z

This PR adds several variants of the conditional Jensen's inequality. I made some changes to Mathlib/Analysis/Convex/Approximation.lean because I need the sequence of affine functions to be bouneded above at each point in the proof of conditional_jensen_hereditarilyLindelofSpace.

depends on: [Merged by Bors] - feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space #31411
depends on: [Merged by Bors] - feat: Conditional expectation commutes with continuous linear functionals and affine functions. #31399
depends on: [Merged by Bors] - feat(Analysis): a closed convex set is the intersection of countably many half-spaces #31180
depends on: [Merged by Bors] - feat: f is lowersemicontinuous iff -f is uppersemicontinuous #36598

github-actions · 2025-08-04T21:28:20Z

PR summary 1c7e491807

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen` (new file)	2412

Declarations diff

+ AEStronglyMeasurable.norm_condExp_le
+ ConcaveOn.condExp_map_le
+ ConcaveOn.condExp_map_le_of_finiteDimensional
+ ConcaveOn.condExp_map_le_univ
+ Convex.condExp_mem
+ ConvexOn.map_condExp_le
+ ConvexOn.map_condExp_le_of_finiteDimensional
+ ConvexOn.map_condExp_le_of_hereditarilyLindelofSpace
+ ConvexOn.map_condExp_le_of_isFiniteMeasure
+ ConvexOn.map_condExp_le_univ
+ Measurable.codRestrict
+ _root_.IsCountablySpanning.null_of_forall_inter_null
+ _root_.IsCountablySpanning.null_of_forall_restrict_null
+ forall_measure_inter_isCountablySpanning_eq_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
9502	1	backward.isDefEq

Current commit 47825382cc
Reference commit 1c7e491807

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib4-merge-conflict-bot · 2025-08-05T10:25:40Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-merge-conflict-bot · 2025-08-14T20:54:37Z

This pull request has conflicts, please merge master and resolve them.

EtienneC30 · 2025-10-25T19:06:16Z

This PR has a huge diff which makes it hard to review. Could you split it smaller bits please? For instance everything in the Separation file could be in its own PR on which this one would depend.

mathlib4-merge-conflict-bot · 2025-11-06T20:43:49Z

This pull request has conflicts, please merge master and resolve them.

CoolRmal · 2025-11-09T09:10:43Z

@EtienneC30 Thank you for your comments. I created several new PRs and I believe they are ready to review now.

-awaiting-author

CoolRmal · 2026-03-14T13:02:17Z

-awaiting-author

mathlib-dependent-issues · 2026-03-17T18:38:11Z

This PR/issue depends on:

~~[Merged by Bors] - feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space #31411~~
~~[Merged by Bors] - feat: Conditional expectation commutes with continuous linear functionals and affine functions. #31399~~
~~[Merged by Bors] - feat(Analysis): a closed convex set is the intersection of countably many half-spaces #31180~~
~~[Merged by Bors] - feat: f is lowersemicontinuous iff -f is uppersemicontinuous #36598~~
By Dependent Issues (🤖). Happy coding!

Mathlib/Algebra/Notation/Pi/Defs.lean

Mathlib/MeasureTheory/Measure/Restrict.lean

RemyDegenne

This is looking really good now! We will be able to merge it soon.

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean

CoolRmal · 2026-03-18T17:35:09Z

-awaiting-author

RemyDegenne

Thanks! This work has led to many nice PRs!
bors d+

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean

mathlib-bors · 2026-03-18T19:06:57Z

✌️ CoolRmal can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

CoolRmal · 2026-03-18T19:14:33Z

bors r+

This PR adds several variants of the conditional Jensen's inequality. I made some changes to Mathlib/Analysis/Convex/Approximation.lean because I need the sequence of affine functions to be bouneded above at each point in the proof of `conditional_jensen_hereditarilyLindelofSpace`.

mathlib-bors · 2026-03-18T19:35:20Z

Pull request successfully merged into master.

Build succeeded:

…community#27953) This PR adds several variants of the conditional Jensen's inequality. I made some changes to Mathlib/Analysis/Convex/Approximation.lean because I need the sequence of affine functions to be bouneded above at each point in the proof of `conditional_jensen_hereditarilyLindelofSpace`.

CoolRmal added 2 commits August 2, 2025 21:57

Initial commit (orphan branch)

6cccdd4

Merge branch 'leanprover-community:master' into unique_riesz

35fc51a

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 4, 2025

CoolRmal marked this pull request as ready for review August 4, 2025 21:47

RemyDegenne changed the title ~~feat(ProbabilityTheory): Conditional Jensen's InequalityConditional jensen~~ feat(ProbabilityTheory): Conditional Jensen's Inequality Aug 5, 2025

RemyDegenne added the t-measure-probability Measure theory / Probability theory label Aug 5, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 5, 2025

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 6, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 14, 2025

CoolRmal added 2 commits September 13, 2025 03:46

Merge branch 'leanprover-community:master' into main

3a340c2

Merge branch 'leanprover-community:master' into main

65bfb5c

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 10, 2025

CoolRmal added 2 commits October 10, 2025 14:05

Merge branch 'leanprover-community:master' into main

6e4ffe9

Merge branch 'leanprover-community:master' into main

a5e675b

leanprover-community-bot-assistant assigned sgouezel Oct 18, 2025

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 29, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 2, 2025

Merge branch 'leanprover-community:master' into main

02aa441

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 6, 2025

EtienneC30 mentioned this pull request Nov 7, 2025

Generalize the type of submartingale results in Mathlib.Probability.Martingale.Basic RemyDegenne/brownian-motion#203

Closed

CoolRmal mentioned this pull request Nov 8, 2025

[Merged by Bors] - feat(Analysis): a closed convex set is the intersection of countably many half-spaces #31180

Closed

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 8, 2025

Update SFinite.lean

5407545

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 14, 2026

CoolRmal added 2 commits March 15, 2026 23:43

Update Basic.lean

f36e3be

Merge branch 'upperSemiContinuousNeg' into conditional-jensen

5f51d73

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 17, 2026

Merge branch 'master' into conditional-jensen

665e742

CoolRmal commented Mar 17, 2026

View reviewed changes

Mathlib/Algebra/Notation/Pi/Defs.lean Outdated Show resolved Hide resolved

CoolRmal added 2 commits March 17, 2026 15:30

Apply suggestion from @CoolRmal

d66b1da

Update Defs.lean

e7fad50

RemyDegenne reviewed Mar 18, 2026

View reviewed changes

Mathlib/MeasureTheory/Measure/Restrict.lean Outdated Show resolved Hide resolved

RemyDegenne reviewed Mar 18, 2026

View reviewed changes

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean Outdated Show resolved Hide resolved

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean Outdated Show resolved Hide resolved

EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026

address comments

2d7ad37

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026

CoolRmal added 2 commits March 18, 2026 14:08

fix

cce0c58

name

62a610e

RemyDegenne approved these changes Mar 18, 2026

View reviewed changes

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 18, 2026

fix name

4782538

mathlib-bors bot changed the title ~~feat(ProbabilityTheory): Conditional Jensen's Inequality~~ [Merged by Bors] - feat(ProbabilityTheory): Conditional Jensen's Inequality Mar 18, 2026

mathlib-bors bot closed this Mar 18, 2026

CoolRmal deleted the conditional-jensen branch March 18, 2026 21:00

Conversation

CoolRmal commented Aug 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 1c7e491807

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Aug 5, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Aug 14, 2025

Uh oh!

EtienneC30 commented Oct 25, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 6, 2025

Uh oh!

CoolRmal commented Nov 9, 2025

Uh oh!

CoolRmal commented Mar 14, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 17, 2026

Uh oh!

Uh oh!

Uh oh!

RemyDegenne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

CoolRmal commented Mar 18, 2026

Uh oh!

RemyDegenne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Mar 18, 2026

Uh oh!

CoolRmal commented Mar 18, 2026

Uh oh!

mathlib-bors bot commented Mar 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

CoolRmal commented Aug 4, 2025 •

edited

Loading

github-actions bot commented Aug 4, 2025 •

edited

Loading