refactor: golf Gaussian/GaussianIntegral

[yuanyi-350]

This PR selectively ports part of #37968 and only migrates the changes in:

• Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Concretely, this PR:

• rewrites integral_gaussian_complex_Ioi by introducing the integrand as a local f and identifying the Iic 0 and Ioi 0 integrals via integral_comp_neg_Ioi
• replaces the previous interval-integral limit argument with a shorter proof using integral_add_compl and the symmetry of the Gaussian integrand on the half-line

[github-actions]

PR summary 700fcd702f

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]

@yuanyi-350 Can I make two global requests to you --- for all such golfing PRs you have made (i.e., please also apply this to all your PRs waiting for review) and all future ones:

Firstly, please provide a more precise PR description: say what the PR actually does (this is the case for this PR already, but not for other PRs) --- and make the general description in your first sentences much shorter: instead of

This PR selectively ports part of https://github.com/leanprover-community/mathlib4/pull/37968 and only migrates the changes in:

    Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Concretely, this PR:
- rewrites integral_gaussian_complex_Ioi by introducing the integrand as a local f and identifying the Iic 0 and Ioi 0 integrals via integral_comp_neg_Ioi
- replaces the previous interval-integral limit argument with a shorter proof using integral_add_compl and the symmetry of the Gaussian integrand on the half-line

you can say

- Rewrite `integral_gaussian_complex_Ioi` by introducing the integrand as a local f and identifying the Iic 0 and Ioi 0 integrals via `integral_comp_neg_Ioi`
- replace the previous interval-integral limit argument with a shorter proof using `integral_add_compl` and the symmetry of the Gaussian integrand on the half-line

Extracted from #37968

which has half the length, but the same information. (Arguably, even the first two sentences could and should be shortened: focus on the why of a change, not the what.)

[grunweg]

Secondly, please provide benchmarking numbers for your PR --- and gather these before making your PR. They should be available the moment your PR is ready for review. Thanks!

Finally, let me share (for the sake of transparency) that we are discussing your series of PRs within the mathlib maintainers. Hopefully, we can provide a more detailed answer to your question "are these PRs desirable?" soon. (The above points are table stakes for the answer to be yes.)

[yuanyi-350]

@grunweg Thank you for your suggestions, which are very helpful for improving our work.
I will spend some time further refining the workflow. Specifically:

1. Each subsequent PR will modify only one file to facilitate review.
2. We will incorporate benchmarking results into the PR message and standardize the PR title as you suggested.
3. We aim to follow common review conventions as much as possible, such as your frequent reminder to use "↦" instead of "=>", and in certain places to write have : statement := foo; simpa using this for better readability, rather than directly simpa using foo.

Finally, may I ask for your Zulip ID? I would like to continue discussing some questions with you.

[grunweg]

Finally, may I ask for your Zulip ID? I would like to continue discussing some questions with you.

You're very welcome to ask your questions publically --- this way others can help you also (and perhaps learn from answers if they wonder about the same thing)! Zulip is generally a friendly place; the mathlib4 stream is probably suitable.