refactor(Bernstein): decompose the repeated integration-by-parts proof

[CBirkbeck]

chafai_repeated_ibp was a 76-line induction — the largest proof in
Bernstein/Measures.lean and one of the longest in the repo. Both branches of the induction
were far past the point where a case should be extracted (the base case ~20 lines, the
inductive step ~42), so the mathematical shape of the argument was buried.

Split into three helpers, each proving one self-contained fact:

Lines	Declaration	What it proves
14	integral_Ioi_neg_iteratedDerivWithin_one	the order-one case: ∫_{(x,∞)} -f' = f x - L, by the FTC on [x, T] plus f → L
10	intervalIntegral_neg_one_pow_succ_kernel	raising the sign exponent of the order-k kernel negates its integral
31	chafai_repeated_ibp_succ	the inductive step: one integration by parts lowers the kernel order k + 1 → k, the boundary term decays, and T → ∞ gives the result
15	chafai_repeated_ibp	now just the induction skeleton dispatching to the three

Every resulting proof is comfortably inside the project's ~50-line limit, and the main theorem
reads as the outline of the argument rather than its implementation.

Two incidental improvements fell out of the extraction:

• the sign-flip step was an inline 13-line have doing intervalIntegral.integral_congr_ae
  by hand; as its own lemma it golfs to a 4-line proof;
• the base case needed a 10-line hsimpl function-rewrite to strip the 0 + 1 / (0+1-1)!
  dressing off the goal. With the order-one fact stated cleanly in its own lemma, simpa
  discharges that in one line.

No statement changes: chafai_repeated_ibp keeps its exact signature, and its only consumer
(chafaiRescaled_integral_bernsteinKernel_eq_sub_tendsto_atTop) is untouched. All helpers are
private, matching the surrounding ibp_finite_interval / boundary_term_decay /
ibp_kernel_integrableOn machinery they sit with.

Gates: lake build ✓, lake exe axioms (allowlist) ✓, lake exe module-system ✓,
scripts/lint-env.sh PASS ✓.

[kim-em]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The generalized endpoint lemma correctly applies the improper FTC on (x, ∞), and the extracted sign and successor lemmas preserve the original repeated integration-by-parts statement without weakening its hypotheses or conclusions.
✅	reuse	approved	codex/gpt-5.6-sol	The current proof reuses Mathlib’s integral_Ioi_of_hasDerivAt_of_nonpos directly, resolving the prior duplication concern. No direct replacement or materially redundant parallel API was found for the extracted private helpers or generalized endpoint specialization.
✅	scope	approved	codex/gpt-5.6-sol	This is a single-topic refactor of already-merged integration-by-parts mathematics. The endpoint-generalized lemma extracts the existing base-case argument and directly supports the refactored theorem.
✅	attribution	approved	codex/gpt-5.6-sol	The affected files credit the central Chafaï construction and relevant Bernstein references; the refactor and endpoint generalization introduce no additional identifiable source requiring attribution.
✅	api-design	approved	codex/gpt-5.6-sol	The new arbitrary-endpoint integral theorem is a reusable public result with a complete statement, while all proof-specific helpers remain private. No exposed bodies, redundant API, or missing automation annotations warrant changes.
✅	generality	approved	codex/gpt-5.6-sol	The generalized endpoint lemma is at the natural level for derivatives within [0, ∞), while the original zero-endpoint result is correctly retained as a specialization. All assumptions in the extracted private induction helpers are substantively used.
✅	placement	approved	codex/gpt-5.6-sol	The endpoint-general improper-integral theorem is in the canonical completely-monotone integral API, while the Bernstein-specific private helpers remain beside the machinery they use. The PR introduces no evidently wrong imports.
✅	naming	approved	codex/gpt-5.6-sol	The introduced names accurately describe their conclusions, follow adjacent terminology and structural _succ conventions, and introduce no notation.
✅	documentation	approved	codex/gpt-5.6-sol	The new public lemma and extracted helpers have accurate, result-focused docstrings, and the Integral module documentation covers the expanded API.
✅	proof-quality	approved	codex/gpt-5.6-sol	The extracted proofs are focused and robust, with arithmetic normalization handled by automation and the analytic structure documented. No brittle rewrite chain, undocumented definitional-equality manipulation, or missing factoring warrants changes.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 80b22e7. rubrics @ b9539a3. Review spend: $7.19.}