refactor: weaken assumptions in LpSeminorm/Count, ProductMeasure

[yuanyi-350]

This selectively ports part of #38104.

Included files only:

• Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
• Mathlib/MeasureTheory/Constructions/Pi.lean
• Mathlib/Probability/ProductMeasure.lean

Concretely, it does three things.

• In Mathlib/MeasureTheory/Constructions/Pi.lean, it rewrites pi_map_piCongrLeft so that it is derived directly from measurePreserving_piCongrLeft; this removes the old [Fintype ι'] assumption and makes the lemma more general.
• In Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean, it replaces a case-split proof of eLpNorm_count_lt_top_of_lt with a cleaner argument that bounds the function by a finite constant on a finite type and then applies general eLpNorm / MemLp lemmas; as a result, that theorem no longer needs MeasurableSingletonClass α.
• Finally, in Mathlib/Probability/ProductMeasure.lean, it updates piContent_eq_measure_pi to use the generalized pi_map_piCongrLeft.

[github-actions]

PR summary 05475cac70

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

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]

As in the other PRs, can you benchmark this PR and give it a more telling PR description? Thanks!

[yuanyi-350]

I ran a profiler comparison for the changed declarations in this PR.

Results (seconds):

• MeasureTheory.eLpNorm_count_lt_top_of_lt: 0.074790 -> 0.211809 (+183.2%)
• pi_map_piCongrLeft (before: MeasureTheory.Measure.pi_map_piCongrLeft, after: MeasureTheory.pi_map_piCongrLeft): 0.129019 -> 0.010057 (-92.2%)
• MeasureTheory.piContent_eq_measure_pi: 0.063107 -> 0.062638 (-0.7%)

Overall:

• pi_map_piCongrLeft is substantially faster after the refactor.
• eLpNorm_count_lt_top_of_lt is substantially slower after the refactor.
• piContent_eq_measure_pi is effectively unchanged.

Caveat:

• These are single-run set_option trace.profiler true in measurements on local before/after worktrees, so very small deltas should be treated as noise.

[yuanyi-350]

Although eLpNorm_count_lt_top_of_lt got slower, it now proves a stronger statement, so the tradeoff seems worthwhile.

[grunweg]

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