refactor(MeasureTheory): golf 100 files

[yuanyi-350]

This PR is an experimental project. In this PR, we use an Agent to automatically scan and attempt to simplify proofs. We hope to eventually effectively golf 100 files and avoid reinventing the wheel in mathlib.

We have chosen Mathlib/MeasureTheory as the testing ground.

If this experiment is very successful and accepted by the mathlib community, we would be honored to open source it.

The relevant projects includes

• refactor(Analysis): golf 100 files #37968, which golfs Mathlib/Analysis.
• refactor(NumberTheory): Golf 100 files #38144 , which golfs Mathlib/NumberTheory.

This PR serves as an index. For the actual code review, please refer to the individual PRs linked below. Each of those PRs modifies only a single file to facilitate the review process.

---

[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%)
Mathlib.Probability.ProductMeasure	2423	2438	+15 (+0.62%)

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

+ instSemilatticeInf
+ instSemilatticeSup

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 mark this PR as depending on the other PRs, please? This way, reviewers won't accidentally review both. Thanks!

[yuanyi-350]

Can you mark this PR as depending on the other PRs, please? This way, reviewers won't accidentally review both. Thanks!

Done — I've marked this PR as depending on the other PRs. Thanks for the suggestion!