Commit 2024-07-14 12:16 a5dbb9dd

feat: Lemma for fderiv of scalar function (#14502) Adds lemma for simplifying the Fréchet derivative when applied to a function maping scalars to scalars. This (currently named fderiv_deriv') is a special case of fderiv_deriv. Neither of simp, fun_prop, aesop, exact? , apply? currently seems to make progress on it. Possibly, it should be instead stated as (fderiv 𝕜 f x : 𝕜 → 𝕜) = ((deriv f x) * ·) if that makes it more likely to be applied by simp? I think it should be marked @[simp] because one would basically always prefer the right hand side to the left hand side of the equality. Does that make sense? I also think fderiv_deriv should be marked @[simp], though maybe there is a reason why it isn't. Marking it such requires a change to the proof of deriv_fderiv, which was using a simp rather than a simp only (not a non-terminal simp but still to be avoided, I would assume?). Maybe other things are also likely to break, however, if those are added to simp?