exists_hasDerivWithinAt_eq_of_le_of_ge
theorem exists_hasDerivWithinAt_eq_of_le_of_ge :
∀ {a b : ℝ} {f f' : ℝ → ℝ},
a ≤ b →
(∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
∀ {m : ℝ}, f' a ≤ m → m ≤ f' b → m ∈ f' '' Set.Icc a b
**Darboux's theorem**: Given two real numbers `a` and `b` with `a ≤ b`, and a function `f` with its derivative function `f'`, if the derivative of `f` at every point `x` in the closed interval `[a, b]` exists, and a real number `m` satisfies `f' a ≤ m ≤ f' b`, then there exists a point `c` in the interval `[a, b]` such that `f' c = m`. This means the image of the derivative function `f'` over the interval `[a, b]` includes all the values between `f' a` and `f' b`, inclusive.
More concisely: Given a real function `f` with derivative `f'` on a closed interval `[a, b]` where `a ≤ b`, if `f'` is continuous on `[a, b]` and `f'` takes on all values between `f' a` and `f' b` inclusively, then there exists a point `c` in `[a, b]` such that `f' (c) = m`, for any `m` with `f' a ≤ m ≤ f' b`.
|
exists_hasDerivWithinAt_eq_of_lt_of_gt
theorem exists_hasDerivWithinAt_eq_of_lt_of_gt :
∀ {a b : ℝ} {f f' : ℝ → ℝ},
a ≤ b →
(∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
∀ {m : ℝ}, m < f' a → f' b < m → m ∈ f' '' Set.Ioo a b
**Darboux's theorem**: Given a real-valued function `f` and its derivative `f'`, and two real numbers `a` and `b` such that `a ≤ b`, if `f'` exists within the closed interval from `a` to `b`, and for some real number `m`, `m` is less than `f'(a)` and greater than `f'(b)`, then there exists some `c` within the open interval from `a` to `b` such that `f'(c)` equals `m`. This theorem is a mathematical way of stating that the derivative of a function does not 'jump' over values, and aligns with the intuitive idea that a function and its derivative change 'smoothly'.
More concisely: If a real-valued function `f` and its derivative `f'` exist on a closed interval [a, b], and `f'` has opposite signs at the endpoints, then there exists a number `c` in the open interval (a, b) such that `f'(c) = m`, where `m` is the value between `f'(a)` and `f'(b)`.
|
Set.OrdConnected.image_hasDerivWithinAt
theorem Set.OrdConnected.image_hasDerivWithinAt :
∀ {f f' : ℝ → ℝ} {s : Set ℝ}, s.OrdConnected → (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → (f' '' s).OrdConnected
**Darboux's theorem** states that if a set `s` of real numbers is connected in order (that is, for any two numbers in the set, all numbers between them are also in the set), and a function `f` has a derivative `f'` within the set `s` at each point `x` in `s`, then the image of the set `s` under the function `f'` is also connected in order. In other words, the derivative `f'` preserves the order connectedness property of the set `s`.
More concisely: If a connected-in-order set of real numbers `s` and its continuous derivative `f'` are defined over `s`, then the image `f'(s)` is also a connected-in-order set.
|
exists_hasDerivWithinAt_eq_of_ge_of_le
theorem exists_hasDerivWithinAt_eq_of_ge_of_le :
∀ {a b : ℝ} {f f' : ℝ → ℝ},
a ≤ b →
(∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
∀ {m : ℝ}, f' a ≤ m → m ≤ f' b → m ∈ f' '' Set.Icc a b
**Darboux's Theorem**: Suppose `a` and `b` are real numbers with `a ≤ b`, `f` and `f'` are real-valued functions, and for each `x` in the closed interval `[a, b]`, the function `f` has a derivative `f'(x)` at `x` within this interval. For any real number `m` where `f'(a) ≤ m ≤ f'(b)`, there exists some `c` in the interval `[a, b]` such that `f'(c) = m`. This means that the derivative `f'` cannot "jump" over the value `m` and takes all values between `f'(a)` and `f'(b)` when `x` ranges in the closed interval `[a, b]` (inclusive). This property is a special case of the Intermediate Value Theorem for derivatives, also known as Darboux's Theorem.
More concisely: Given real numbers `a ≤ b`, a real-valued function `f` with derivative `f'` on `[a, b]`, if `f'(a) ≤ m ≤ f'(b)`, then there exists `c` in `[a, b]` with `f'(c) = m`.
|
Convex.image_derivWithin
theorem Convex.image_derivWithin :
∀ {f : ℝ → ℝ} {s : Set ℝ}, Convex ℝ s → DifferentiableOn ℝ f s → Convex ℝ (derivWithin f s '' s)
The theorem, known as Darboux's theorem, states that if you have a function `f` from real numbers to real numbers and a convex set `s` of real numbers, then if `f` is differentiable on `s`, the image of `s` under the derivative of `f` is also a convex set. In other words, the set of all derivative values of `f` at points within `s` forms a convex set. Here, the derivative is calculated within the set `s` using the `derivWithin` function.
More concisely: If `f` is a differentiable real function on a convex set `s` in the real numbers, then the image of `s` under the derivative `df/dx` is a convex set.
|
Set.OrdConnected.image_deriv
theorem Set.OrdConnected.image_deriv :
∀ {f : ℝ → ℝ} {s : Set ℝ}, s.OrdConnected → (∀ x ∈ s, DifferentiableAt ℝ f x) → (deriv f '' s).OrdConnected := by
sorry
**Darboux's theorem**: Given a function `f : ℝ → ℝ` and a set `s : Set ℝ` that is order-connected (i.e., for any two elements in the set, all the elements that lie between these two are also in the set), if the function `f` is differentiable at every point in `s`, then the image of `s` under the derivative of `f` is also an order-connected set. This is the version of the theorem that uses the derivative function `deriv`. In other words, the set of derivatives of `f` at each point in `s` preserves the order-connected property. This is a formalization of a well-known result in real analysis that states the derivative of a differentiable function has the intermediate value property.
More concisely: If a differentiable function maps an order-connected set to another set, then the image set is also order-connected. (Darboux's Theorem)
|
Convex.image_hasDerivWithinAt
theorem Convex.image_hasDerivWithinAt :
∀ {f f' : ℝ → ℝ} {s : Set ℝ}, Convex ℝ s → (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → Convex ℝ (f' '' s)
**Darboux's Theorem**: This theorem states that if a function `f` has a derivative `f'` within a convex set `s` of real numbers, then the image of the convex set under the derivative function `f'` is also a convex set. Here, the derivative of the function at any point `x` in the set `s` is given by `f'(x)`. The convexity of a set is defined such that for any two points in the set, the function is less than or equal to the maximum of the function values at those two points.
More concisely: If a real-valued function `f` has a convex derivative `f'` on a convex set `s`, then the image `f'(s)` is also a convex set.
|
hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne
theorem hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne :
∀ {f f' : ℝ → ℝ} {s : Set ℝ},
Convex ℝ s →
(∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
∀ {m : ℝ}, (∀ x ∈ s, f' x ≠ m) → (∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x
The theorem `hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne` states that given a function `f` and its derivative function `f'`, and a convex set `s` of real numbers, if for every `x` in `s`, the derivative of `f` at `x` within `s` exists and is not equal to a particular real number `m`, then either for all `x` in `s`, `f'` of `x` is less than `m`, or for all `x` in `s`, `m` is less than `f'` of `x`. In other words, if the derivative of a function within a convex set is never equal to a particular value, then it is always either greater than or less than that value.
More concisely: If a real-valued function and its derivative exist in a convex set and are never equal to a specific value, then the derivative is strictly less than or strictly greater than that value throughout the set.
|
exists_hasDerivWithinAt_eq_of_gt_of_lt
theorem exists_hasDerivWithinAt_eq_of_gt_of_lt :
∀ {a b : ℝ} {f f' : ℝ → ℝ},
a ≤ b →
(∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
∀ {m : ℝ}, f' a < m → m < f' b → m ∈ f' '' Set.Ioo a b
**Darboux's theorem**: This theorem states that for a function `f` and its derivative `f'`, defined over real numbers, if `a ≤ b` and the value of the derivative `f'` at `a` is less than a real number `m`, which in turn is less than the value of `f'` at `b`, then there exists a point `c` in the open interval `(a, b)` such that the derivative `f'` at `c` equals `m`. In other words, if the derivative at the endpoints of an interval changes, the derivative takes every value between those two values at some point in the interval. The theorem assumes that the derivative `f'` exists and is continuous within the closed interval `[a, b]`.
More concisely: If a real-valued function `f` with continuous derivative `f'` on the closed interval `[a, b]` satisfies `f'(a) < m < f'(b)`, then there exists a number `c` in the open interval `(a, b)` such that `f'(c) = m`.
|
Set.OrdConnected.image_derivWithin
theorem Set.OrdConnected.image_derivWithin :
∀ {f : ℝ → ℝ} {s : Set ℝ}, s.OrdConnected → DifferentiableOn ℝ f s → (derivWithin f s '' s).OrdConnected
**Darboux's theorem**: Given a function `f` from real numbers to real numbers and an ordered connected set `s` of real numbers, if the function `f` is differentiable on the set `s`, then the image of the set `s` under the derivative of `f` within `s` (i.e., `derivWithin f s`) is also an ordered connected set. This is a version of Darboux's theorem specific to derivatives within a set.
More concisely: If a real-valued function is differentiable on an ordered and connected set, then the image of that set under its derivative is an ordered and connected set.
|
Convex.image_deriv
theorem Convex.image_deriv :
∀ {f : ℝ → ℝ} {s : Set ℝ}, Convex ℝ s → (∀ x ∈ s, DifferentiableAt ℝ f x) → Convex ℝ (deriv f '' s)
**Darboux's theorem**: Given a convex set `s` in the real numbers and a real function `f` that is differentiable at every point in `s`, the image of `s` under the derivative of `f` (denoted as `deriv f`) is also a convex set in the real numbers. This is a version of Darboux's theorem applied to the derivative of a function.
More concisely: The derivative of a differentiable real function on a convex domain maps the domain to a convex set in the real numbers.
|