LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.Deriv.Slope

range_deriv_subset_closure_span_image

theorem range_deriv_subset_closure_span_image : βˆ€ {π•œ : Type u} [inst : NontriviallyNormedField π•œ] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace π•œ F] (f : π•œ β†’ F) {t : Set π•œ}, Dense t β†’ Set.range (deriv f) βŠ† closure ↑(Submodule.span π•œ (f '' t))

The theorem `range_deriv_subset_closure_span_image` states that for any dense set `t` in a non-trivially normed field `π•œ` with a normed space `F`, the range of the derivative function `deriv f` is contained within the closure of the submodule spanned by the image of `t` under the function `f`. In other words, all values that the derivative of a function `f` can take are included in the smallest closed set containing the submodule generated by `f` acting on `t`. This signifies the link between the derivative of a function and the topology of the space in which the function is defined.

More concisely: The derivative of a function on a dense subset of a non-trivially normed field maps into the closure of the subspace spanned by the function's values on that subset.

range_derivWithin_subset_closure_span_image

theorem range_derivWithin_subset_closure_span_image : βˆ€ {π•œ : Type u} [inst : NontriviallyNormedField π•œ] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace π•œ F] (f : π•œ β†’ F) {s t : Set π•œ}, s βŠ† closure (s ∩ t) β†’ Set.range (derivWithin f s) βŠ† closure ↑(Submodule.span π•œ (f '' t))

This theorem states that for any function `f` mapping from a non-trivially normed field `π•œ` to a normed add commutative group `F` (which is also a normed space over `π•œ`), given a set `s` and a set `t` such that the intersection of `s` and `t` is dense in `s`, then the range of the derivative of `f` within `s` is contained in the closure of the submodule spanned by the image of `t` under `f`. In other words, if we take all the points within `s` where `f` has a derivative and look at the set of those derivative values, this set is contained within the smallest closed set that contains all linear combinations of values that `f` takes on `t`.

More concisely: Given a function `f` from a non-trivially normed field to a normed add commutative group that is also a normed space, if `s` and `t` are sets with dense intersection, then the derivative range of `f` in `s` is contained in the closure of the submodule spanned by the images of `t` under `f`.

HasDerivWithinAt.limsup_norm_slope_le

theorem HasDerivWithinAt.limsup_norm_slope_le : βˆ€ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ β†’ E} {f' : E} {s : Set ℝ} {x r : ℝ}, HasDerivWithinAt f f' s x β†’ β€–f'β€– < r β†’ βˆ€αΆ  (z : ℝ) in nhdsWithin x s, β€–z - x‖⁻¹ * β€–f z - f xβ€– < r

This theorem states that if a function `f` has a derivative `f'` at a point `x` within a subset `s`, then for any real number `r` that is greater than the norm of `f'`, the ratio of the norm of the difference between `f(z)` and `f(x)` to the norm of the difference between `z` and `x` is less than `r` in a neighborhood of `x` within `s`. In other words, the limit superior of this ratio as `z` tends to `x` along `s` is less than or equal to the norm of `f'`. This theorem thus bounds the slope of the function `f` in a neighborhood around `x` within the set `s`.

More concisely: Given a real-valued function `f` with derivative `f'` at a point `x` in a subset `s`, and for any real number `r` greater than the norm of `f'`, the ratio of the norm of `f(z) - f(x)` to the norm of `z - x` is less than `r` for all `z` in a neighborhood of `x` within `s`, that is, the limit superior of this ratio as `z` approaches `x` in `s` is less than or equal to the norm of `f'`.

HasDerivWithinAt.liminf_right_norm_slope_le

theorem HasDerivWithinAt.liminf_right_norm_slope_le : βˆ€ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ β†’ E} {f' : E} {x r : ℝ}, HasDerivWithinAt f f' (Set.Ici x) x β†’ β€–f'β€– < r β†’ βˆƒαΆ  (z : ℝ) in nhdsWithin x (Set.Ioi x), β€–z - x‖⁻¹ * β€–f z - f xβ€– < r

The theorem `HasDerivWithinAt.liminf_right_norm_slope_le` states that if a function `f` has a derivative `f'` at a point `x` within the interval `(x, +∞)`, then for any real number `r` greater than the norm of `f'`, the ratio of the norm of the difference between `f(z)` and `f(x)` to the norm of the difference between `z` and `x` is frequently less than `r` as `z` approaches `x` from the right. In mathematical terms, this means the limit inferior (or lower limit) of this ratio as `z` tends to `x+0` is less than or equal to the norm of `f'`. A stronger version of this theorem is also available which uses the limit superior and can be applied to any set `s`.

More concisely: If a real-valued function `f` has a derivative `f'` at `x`, then the limit inferior of the ratio of `|f(z) - f(x)|` to `|z - x|` as `z -> x+` is less than or equal to the norm of `f'`.

hasDerivAtFilter_iff_tendsto_slope

theorem hasDerivAtFilter_iff_tendsto_slope : βˆ€ {π•œ : Type u} [inst : NontriviallyNormedField π•œ] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ}, HasDerivAtFilter f f' x L ↔ Filter.Tendsto (slope f x) (L βŠ“ Filter.principal {x}ᢜ) (nhds f')

This theorem states that for a function `f` from a non-trivially normed field `π•œ` to a normed add-commutative group `F` that also forms a normed space over `π•œ`, the derivative of `f` at a point `x` with respect to a filter `L` exists if and only if the function that calculates the slope of `f` at `x` tends towards the derivative `f'` as we approach `x` along the filter `L` intersected with the principal filter of the complement of the set `{x}` (i.e., all points other than `x`). In other words, when the domain has one dimension, the concept of the FrΓ©chet derivative, a more general form of derivative, reduces to the classical definition of a derivative as a limit of the slope of the function. However, the limit needs to be taken along the points different from `x` because when `y = x`, the slope is zero due to the convention that `0⁻¹ = 0`.

More concisely: For a function from a non-trivially normed field to a normed add-commutative group, the FrΓ©chet derivative at a point exists if and only if the slope function tends to the derivative as filters approaching the point intersect the principal filter of points other than that point.

HasDerivWithinAt.limsup_slope_norm_le

theorem HasDerivWithinAt.limsup_slope_norm_le : βˆ€ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ β†’ E} {f' : E} {s : Set ℝ} {x r : ℝ}, HasDerivWithinAt f f' s x β†’ β€–f'β€– < r β†’ βˆ€αΆ  (z : ℝ) in nhdsWithin x s, β€–z - x‖⁻¹ * (β€–f zβ€– - β€–f xβ€–) < r

This theorem states that if a function `f` has a derivative `f'` at a point `x` within a subset `s`, then for any real number `r` greater than the norm of `f'`, the ratio `(β€–f zβ€– - β€–f xβ€–) / β€–z - xβ€–` is less than `r` in some neighborhood of `x` within `s`. This means, the limit supremum of this ratio as `z` approaches `x` within `s` is less than or equal to the norm of `f'`. This is a weaker version of another theorem where `β€–f zβ€– - β€–f xβ€–` is replaced by `β€–f z - f xβ€–`.

More concisely: If `f` is differentiable at `x` in the subset `s`, then for any `r` greater than the norm of `f'` at `x`, the limit superior of `(||f(z) - f(x)|| / ||z - x||)` as `z` approaches `x` within `s` is less than or equal to `||f'||`.

HasDerivAt.tendsto_slope_zero

theorem HasDerivAt.tendsto_slope_zero : βˆ€ {π•œ : Type u} [inst : NontriviallyNormedField π•œ] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ}, HasDerivAt f f' x β†’ Filter.Tendsto (fun t => t⁻¹ β€’ (f (x + t) - f x)) (nhdsWithin 0 {0}ᢜ) (nhds f')

This theorem, `HasDerivAt.tendsto_slope_zero`, states that for a function `f` from a nontrivial normed field `π•œ` to a normed add commutative group `F`, if `f` has a derivative `f'` at a point `x`, then as `t` tends to 0 in `π•œ` (excluding the point 0), the expression `t⁻¹ β€’ (f (x + t) - f x)`, which can be seen as a scaled difference quotient or "slope", tends to `f'`. In other words, this theorem states that a function having a derivative at a point implies that the function's scaled slope converges to the derivative as we zoom in towards that point.

More concisely: If a function `f` from a nontrivial normed field to a normed add commutative group has a derivative `f'` at a point `x`, then the scaled difference quotient `t⁻¹ β€’ (f (x + t) - f x)` converges to `f'` as `t` tends to 0, excluding the point 0.

HasDerivWithinAt.liminf_right_slope_norm_le

theorem HasDerivWithinAt.liminf_right_slope_norm_le : βˆ€ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ β†’ E} {f' : E} {x r : ℝ}, HasDerivWithinAt f f' (Set.Ici x) x β†’ β€–f'β€– < r β†’ βˆƒαΆ  (z : ℝ) in nhdsWithin x (Set.Ioi x), (z - x)⁻¹ * (β€–f zβ€– - β€–f xβ€–) < r

The theorem `HasDerivWithinAt.liminf_right_slope_norm_le` states that if a function `f` has a derivative `f'` at a point `x` within the interval extending from `x` to positive infinity, then for any real number `r` that is greater than the norm of `f'`, there frequently exists a point `z` within the interval that extends from `x` to just over `x` such that the ratio `(β€–f zβ€– - β€–f xβ€–) / (z - x)` is less than `r`. In other terms, the lower limit (or limit inferior) of this ratio as `z` approaches `x` from the right is less than or equal to the norm of `f'`. This theorem also refers to two stronger versions, one employing limit superior and any set `s`, and another using the difference of function values `β€–f z - f xpβ€–` instead of the difference of norms `β€–f zβ€– - β€–f xβ€–`.

More concisely: If a real-valued function `f` has a derivative `f'` at `x`, then for any `r` greater than the norm of `f'`, there exists `z` near `x` such that the ratio of the norm difference `|f z - f x|` to the distance `|z - x|` is less than `r`. (The lower right-hand limit of this ratio is less than or equal to the norm of `f'`.)