Add a sharp bound for the integral Taylor remainder

[lluiseriksson]

This adds an orientation-free norm bound obtained from the existing
vector-valued integral Taylor remainder:

‖f x - taylorWithinEval f n (uIcc x₀ x) x₀ x‖ ≤
  C * |x - x₀| ^ (n + 1) / (Nat.factorial (n + 1) : ℝ)

Unlike taylor_mean_remainder_bound, the statement allows either endpoint
ordering and retains the sharp (n + 1)! denominator. Nonnegativity of C is
derived from the derivative bound at the left endpoint rather than required as
a separate assumption.

Mathlib.Analysis.Calculus.TaylorIntegral was also checked. Its
map_add_eq_sum_add_integral_iteratedFDeriv is a higher-dimensional formula in
terms of global iteratedFDeriv, whereas this result bounds the existing
one-dimensional taylorWithinEval/iteratedDerivWithin remainder under a
ContDiffOn hypothesis. Converting between those interfaces would not shorten
the proof; this theorem is therefore derived directly from the existing
taylor_integral_remainder immediately above it.

Testing:

• kernel-checked with Lean 4.31.0 at the branch base;
• #print axioms reports only propext, Classical.choice, and Quot.sound;
• git diff --check passes.

The upstream master toolchain changed to Lean 4.33.0-rc2 after this branch
base. This is deliberately opened as a draft so CI/rebase can expose any API
adjustment required by the new toolchain.

[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 d52ea99b42

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Calculus.Taylor	2489	2530	+41 (+1.65%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Calculus.Taylor	41

---

Declarations diff (regex)

+ taylor_integral_remainder_bound

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.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit d52ea99b42
Reference commit fabf563a7c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).