Skip to content

[Merged by Bors] - feat: Conditional expectation commutes with continuous linear functionals and affine functions.#31399

Closed
CoolRmal wants to merge 17 commits intoleanprover-community:masterfrom
CoolRmal:condExpAffine
Closed

[Merged by Bors] - feat: Conditional expectation commutes with continuous linear functionals and affine functions.#31399
CoolRmal wants to merge 17 commits intoleanprover-community:masterfrom
CoolRmal:condExpAffine

Conversation

@CoolRmal
Copy link
Copy Markdown
Contributor

@CoolRmal CoolRmal commented Nov 8, 2025

This lemma is needed in the proof of conditional Jensen's inequality: #27953

Open in Gitpod

@github-actions 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 Nov 8, 2025
@CoolRmal CoolRmal mentioned this pull request Nov 8, 2025
Closed
4 tasks
@github-actions github-actions bot added the t-measure-probability Measure theory / Probability theory label Nov 8, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 8, 2025 •
edited
Loading

PR summary cda9a04e75

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.ContinuousLinearMap.comp_condExp_add_const_comm
+ _root_.ContinuousLinearMap.comp_condExp_comm

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/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).

EtienneC30
EtienneC30 reviewed Nov 13, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@EtienneC30 EtienneC30 left a comment

Choose a reason for hiding this comment

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

Thanks!

@EtienneC30 EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2025
@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2025
@EtienneC30
Copy link
Copy Markdown
Member

EtienneC30 commented Nov 13, 2025

When you applied a suggestion can you resolve the conversation please? It makes it easier to see what's left and it takes much less space on the screen.

EtienneC30
EtienneC30 reviewed Nov 13, 2025
View reviewed changes
@EtienneC30 EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2025
@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2025
@EtienneC30
Copy link
Copy Markdown
Member

EtienneC30 commented Nov 15, 2025

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 15, 2025

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 15, 2025
RemyDegenne
RemyDegenne approved these changes Nov 15, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

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

Thanks!
bors r+

mathlib-bors bot pushed a commit that referenced this pull request Nov 15, 2025
@CoolRmal
feat: Conditional expectation commutes with continuous linear functio…
6ee2e76 
…nals and affine functions. (#31399)

This lemma is needed in the proof of conditional Jensen's inequality: #27953
@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Nov 15, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 15, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Conditional expectation commutes with continuous linear functionals and affine functions. [Merged by Bors] - feat: Conditional expectation commutes with continuous linear functionals and affine functions. Nov 15, 2025
@mathlib-bors mathlib-bors bot closed this Nov 15, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@EtienneC30 EtienneC30 EtienneC30 left review comments

@RemyDegenne RemyDegenne RemyDegenne approved these changes

Assignees

@EtienneC30 EtienneC30

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@CoolRmal @EtienneC30 @RemyDegenne