feat(Probability/HypothesisTesting): add Neyman-Pearson lemma

[zixiaowang17]

This PR adds Probability/HypothesisTesting/NeymanPearson.lean, formalizing the classical Neyman-Pearson lemma with reference

Ingster, Y. and Suslina, I.A., 2012. Nonparametric goodness-of-fit testing under Gaussian models (Vol. 169). Springer Science & Business Media.
-/

The main definitions are:

• ProbabilityTheory.NeymanPearson.npLikelihoodRatio
• ProbabilityTheory.NeymanPearson.npTest
• ProbabilityTheory.NeymanPearson.npSumError

The main theorem is:

• ProbabilityTheory.NeymanPearson.neyman_pearson

We state the theorem in the weighted form ∫ T dP + t * ∫ (1 - T) dQ, over measurable tests T : Ω → ℝ with values in [0, 1], using P + Q as the canonical dominating measure; rather than starting with the constrained formulation that fixes the Type I error and minimizes the Type II error. The reasons are two fold.

First, it can be thought as the Lagrangian form of the classical constrained Neyman-Pearson problem.

Second, this weighted form is often arises in applications, such as, in minimax lower-bound arguments for functional estimation, where one typically reduces estimation lower bounds to testing inequalities involving weighted sums of error probabilities.

Worflow with AI: we first manually wrote a blueprint in latex with every definition and lemma we need NL_Blueprint_NP_Lemma.pdf. then we checked the Mathlib API with claude code, chatgpt and LeanSearch, We manually wrote the outline, in the outline version we deleted the discussion on gamma in the blueprint - since we have used the version of the NP lemma that uses the likelihood ratio to construct the test, rather than writing in terms of comparisons of Radon-Nikodym derivatives with a common dominating measure, and hence have used gamma to arbitrarily define likelihood-ratio sets of measure zero under the null hypothesis. This choice is motivated by the downstream derivation of errors of NP tests. since we are unfamiliar with mathlib naming style, we used claude code skill for proof golfing and some syntax correction, eg whether should use unfold or simp only [];

Co-authored-by: Rajarshi Mukherjee ram521@mail.harvard.edu

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary f95e015368

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Probability.Decision.HypothesisTesting.NeymanPearson (new file)	2317

---

Declarations diff

+ measurable_npLikelihoodRatio
+ measurable_npTest
+ neyman_pearson
+ npLikelihoodRatio
+ npSumError
+ npTest
+ npTest_le_one
+ npTest_nonneg

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[grunweg]

Per zulip, the code in this PR is LLM-generated.
I've labelled the PR accordingly. Note that the PR description should be updated to match the zulip comment.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.