[Merged by Bors] - feat(Analysis/Calculus/FDeriv): add fderiv_apply simp lemmas

[IlPreteRosso]

Add @[simp] lemmas fderiv_apply and fderivWithin_apply that extract a component from the fderiv of a Pi-type function: (proj i).comp (fderiv 𝕜 Φ x) = fderiv 𝕜 (fun x => Φ x i) x. This completes the extraction direction of the Pi fderiv API alongside the existing construction direction (fderiv_pi).

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

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ fderivWithin_apply
+ fderiv_apply

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).

[IlPreteRosso]

One question about the direction. In my downstream project the pattern that shows up frequently is Φ : XL1 ν L → XL1 ν L to fderiv 𝕜 (fun x => Φ x i) x v, from bundled derivative evaluated then projected simplified to proj., deriv, then eval., so that component-level proof can proceed.

The fderiv_pi' can go in the direction complying with the API convention, and can be unsimped, but the real simp workhorse I can tell from my project is something like

@[simp]
lemma fderiv_apply {Φ : E → ∀ i, F' i} (hΦ : DifferentiableAt 𝕜 Φ x) (v : E) (i : ι) :                       
      fderiv 𝕜 Φ x v i = fderiv 𝕜 (fun x => Φ x i) x v := by                                                               
      rw [fderiv_pi']; ... 

Ok I misunderstood the _apply suffix in Mathlib's fderiv API so after a second thought I will just keep this simp lemma to local project instead.

[eric-wieser]

Suggested change

	theorem fderivWithin_pi' (hΦ : DifferentiableWithinAt 𝕜 Φ s x)
	theorem fderivWithin_apply (hΦ : DifferentiableWithinAt 𝕜 Φ s x)

is now the right name I think; my comment earlier was that your name suggested the current direction but the type was the opposite.

[eric-wieser]

Ah apologies, I missed the message above. Perhaps get a second opinion

[IlPreteRosso]

Ah apologies, I missed the message above. Perhaps get a second opinion

No worries. I was not folloing the api's _apply implication ealier on. Let me know your opinion.

[j-loreaux]

I think apply is the right name here. Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step