generalizing HasFDerivAtFilter

Stream: maths

[Yury G. Kudryashov]

WDYT about changing docs#HasFDerivAtFilter to take a filter in the product instead? This way it will be useful to state facts about docs#HasFDerivWithinAt and docs#HasStrictFDerivAt. Right now, it is not very useful, as we only use it with nhds and nhdsWithin.

[Floris van Doorn]

In that case HasFderivWithinAt will be defined using the filter pure x ×ˢ 𝓝[s] x? Yeah, that sounds good!

[Yury G. Kudryashov]

Either this spelling or map (fun y => (y, x)) (𝓝[s] x), not yet sure which one will be more convenient.

[Yury G. Kudryashov]

I'll do it after the current pass of generalizations to TVS.

[Yury G. Kudryashov]

On the one hand, #34965 compiles (not sure about the linter yet; definitely need to update some docstrings and write a commit message). On the other hand, it uncovered that docs#HasFDerivAt.congr_of_eventuallyEq and docs#HasDerivAtFilter.congr_of_eventuallyEq have one idea about LHS vs RHS of the equality assumptions, while docs#HasStrictFDerivAt.congr_of_eventuallyEq has the opposite idea about it. While looking for other data points, I found out that we have docs#ContinuousAt.congr and docs#ContinuousAt.congr_of_eventuallyEq that use different conventions. Which one should we use?

[Yury G. Kudryashov]

Probably, I should start a new thread to improve visibility.

[Yury G. Kudryashov]

See #mathlib4 > MyProp.congr_* lemmas, LHS vs RHS

[Yury G. Kudryashov]

#34965 is ready for review

[Yury G. Kudryashov]

I would really appreciate a review of #34965. It blocks some other refactors about fderiv I want to make (e.g., generalizing more to TVS).