refactor: golf only AEEqOfIntegral, AEMeasurableOrder, ConditionalExpectation/Real

[yuanyi-350]

This PR selectively ports part of #38104.

Included files:

• Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
• Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
• Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean

More concretely:

• In AEEqOfIntegral.lean, the PR rewrites the lemmas saying "if two integrable functions have the same integrals on all finite-measure measurable sets, then they are equal almost everywhere." The old proof went through Lp; the new proof uses the more direct AEFinStronglyMeasurable lemmas. Same result, shorter route.
• In AEMeasurableOrder.lean, it cleans up one proof of almost-everywhere measurability by using standard lemmas like measure_eq_zero_iff_ae_notMem and Dense.exists_between instead of spelling those arguments out manually. This is a pure proof simplification.
• In ConditionalExpectation/Real.lean, the main change is to import ConditionalExpectation/CondJensen and use its general results. In particular:
  • the L¹ contraction statement for conditional expectation is now derived from the general inequality ‖E[f | m]‖ ≤ E[‖f‖ | m],
  • the inequality ∫ |E[f | m]| ≤ ∫ |f| becomes a direct consequence of that norm inequality plus integral_condExp,
  • the boundedness result "if |f| ≤ R a.e., then |E[f | m]| ≤ R a.e." is re-proved by saying that f lies a.e. in the closed convex interval [-R, R], so its conditional expectation stays in that interval by Convex.condExp_mem.

This intentionally excludes the rest of #38104.

[github-actions]

PR summary 8e3c989104

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Function.ConditionalExpectation.Real	2324	2340	+16 (+0.69%)

Import changes for all files

Files	Import difference
15 files Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs Mathlib.Probability.Distributions.Binomial Mathlib.Probability.Distributions.SetBernoulli Mathlib.Probability.HasLawExists Mathlib.Probability.IdentDistribIndep Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.InfinitePi Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.IonescuTulcea.Traj Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.ProductMeasure	15
23 files Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.FactorsThrough Mathlib.Probability.BorelCantelli Mathlib.Probability.Kernel.CompProdEqIff Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Posterior Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.LocalProperty Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Predictable Mathlib.Probability.Process.Stopping	16

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

---

No changes to technical debt.

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

[grunweg]

Can you update the PR description to say what this PR does (as opposed to what it doesn't do).
For instance, "I didn't run CI on this PR" does not belong into the PR description.
Thanks!

[yuanyi-350]

!bench

[leanprover-radar]

Benchmark results for c22a484 against 8e3c989 are in. No significant results found. @yuanyi-350

• ✅ build//instructions: -22.1G (-0.01%)

Small changes (1✅)

• ✅ build/module/Mathlib.MeasureTheory.Function.ConditionalExpectation.Real//instructions: -1.1G (-6.71%)

[grunweg]

Please follow the request made in the comments here and here. Thanks!