This is a question about the notion of derivatives from the Isabelle libraries.
I am trying to understand what (f has_field_derivative D x) (at x within S) means. I know (at x within S) is a filter, but intuitively I was imagining that the following statement is true
lemma DERIV_at_within:
"(∀x ∈ S. (f has_field_derivative D x) (at x))
= (∀x. (f has_field_derivative D x) (at x within S))"
If it is not, how else should I interpret (at x within S) in the context of derivatives?
at x within A is the pointed neighbourhood of x, intersected with A. For instance, at_right is an abbreviation for at x within {x<..}, i.e. the right-neighbourhood of x. This allows you to express one-sided derivatives.
Occasionally, one also sees assumptions like ∀x∈{a..b}. (f has_field_derivative f' x) (at x within {a..b}). This means that f is differentiable with derivative f' between a and b, but the derivatives at the edges (i.e. at a and b) need only be one-sided.
Note also that at x = at x within UNIV. Also, if A is an open set containint x, you simply have at x within A = at x.
Typically, you only really need has_field_derivative with at x within … if you want something like a one-sided limit (or, in higher dimensions, if you somehow want to constrain the direction of approach).