exists_ratio_deriv_eq_ratio_slope
theorem exists_ratio_deriv_eq_ratio_slope :
∀ (f : ℝ → ℝ) {a b : ℝ},
a < b →
ContinuousOn f (Set.Icc a b) →
DifferentiableOn ℝ f (Set.Ioo a b) →
∀ (g : ℝ → ℝ),
ContinuousOn g (Set.Icc a b) →
DifferentiableOn ℝ g (Set.Ioo a b) →
∃ c ∈ Set.Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c
This theorem is a Lean version of Cauchy's Mean Value Theorem, specifically for derivatives. It states that for all real-valued functions `f` and `g`, given two real numbers `a` and `b` with `a < b`, if `f` and `g` are both continuous on the closed interval from `a` to `b` and differentiable on the open interval from `a` to `b`, then there exists a real number `c` in the open interval from `a` to `b` such that the ratio of the difference in function values of `g` at `b` and `a` to the derivative of `f` at `c` equals the ratio of the difference in function values of `f` at `b` and `a` to the derivative of `g` at `c`. This is represented mathematically as `(g(b) - g(a)) * deriv f c = (f(b) - f(a)) * deriv g c`.
More concisely: Given real-valued functions `f` and `g` with `a < b`, if `f` and `g` are continuous on `[a, b]` and differentiable on `(a, b)`, then there exists `c \in (a, b)` such that `(g(b) - g(a)) / (f'(c)) = (f(b) - f(a)) / (g'(c))`.
|
Convex.mul_sub_lt_image_sub_of_lt_deriv
theorem Convex.mul_sub_lt_image_sub_of_lt_deriv :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D →
DifferentiableOn ℝ f (interior D) →
∀ {C : ℝ}, (∀ x ∈ interior D, C < deriv f x) → ∀ x ∈ D, ∀ y ∈ D, x < y → C * (y - x) < f y - f x
The theorem states that if we have a set `D` in the real numbers that is convex, and a function `f` that is continuous on `D` and differentiable on the interior of `D`, then if for some real number `C`, the derivative of `f` at any point in the interior of `D` is greater than `C`, then for any two points `x` and `y` in `D` where `x` is less than `y`, the value of `C` multiplied by the difference between `y` and `x` is less than the difference between `f(y)` and `f(x)`. This essentially means that the function `f` is growing faster than `C * x` on `D`.
More concisely: If `D` is a convex set of real numbers, `f` is a continuous and differentiable function on the interior of `D`, and there exists a real number `C` such that the derivative of `f` is strictly greater than `C` at every point in the interior of `D`, then for any `x, y` in `D` with `x < y`, we have `C * (y - x) < f(y) - f(x)`.
|
exists_ratio_hasDerivAt_eq_ratio_slope'
theorem exists_ratio_hasDerivAt_eq_ratio_slope' :
∀ (f f' : ℝ → ℝ) {a b : ℝ},
a < b →
∀ (g g' : ℝ → ℝ) {lfa lga lfb lgb : ℝ},
(∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
(∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa) →
Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga) →
Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb) →
Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb) →
∃ c ∈ Set.Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
This is an extended version of Cauchy's Mean Value Theorem, which involves the derivative of real-valued functions. Given two functions `f` and `g` along with their derivatives `f'` and `g'`, and four real numbers `lfa`, `lga`, `lfb` and `lgb`, the theorem states that if `a` is less than `b`, and both `f` and `g` have their derivatives at every point in the left-open right-open interval between `a` and `b`, and if `f` and `g` tend to `lfa` and `lga` respectively as we approach `a` from values greater than `a`, and `f` and `g` also tend to `lfb` and `lgb` respectively as we approach `b` from values less than `b`, then there exists a point `c` in the interval between `a` and `b` such that the difference between `lgb` and `lga` times the derivative of `f` at `c` equals the difference between `lfb` and `lfa` times the derivative of `g` at `c`.
More concisely: Given two real-valued functions `f` and `g` with derivatives `f'` and `g'` on the interval `(a, b)` where `a < b`, if `f` and `g` have the given limits at the endpoints and `f'` and `g'` exist at every point in `(a, b)`, then there exists a point `c` in `(a, b)` such that `(lfb - lfa) * f'(c) = (lgb - lga) * g'(c)`.
|
lipschitzWith_of_nnnorm_fderiv_le
theorem lipschitzWith_of_nnnorm_fderiv_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{E : Type u_5} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → G} {C : NNReal},
Differentiable 𝕜 f → (∀ (x : E), ‖fderiv 𝕜 f x‖₊ ≤ C) → LipschitzWith C f
This is a version of the Mean Value Theorem. It states that for any function `f` from a normed space `E` to a normed addative commutative group `G`, both over a type `𝕜` that behaves like real numbers, if `f` is differentiable everywhere and the nonnegative norm of its derivative at any point `x` is bounded by a constant `C` (i.e., `‖fderiv 𝕜 f x‖₊ ≤ C`), then `f` is Lipschitz continuous with Lipschitz constant `C`. In other words, for all pairs of points `x` and `y` in `E`, the distance between `f(x)` and `f(y)` is at most `C` times the distance between `x` and `y` (i.e., `dist (f x) (f y) ≤ C * dist x y`).
More concisely: If a differentiable function `f` from a normed space to a normed additive commutative group, with its derivative having bounded norm, is Lipschitz continuous with constant equal to the supremum of the derivative norms.
|
norm_image_sub_le_of_norm_deriv_right_le_segment
theorem norm_image_sub_le_of_norm_deriv_right_le_segment :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E}
{C : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ C) → ∀ x ∈ Set.Icc a b, ‖f x - f a‖ ≤ C * (x - a)
This theorem states that if we have a function `f` mapping real numbers to a normed additive commutative group `E` such that `f` is continuous on a closed interval `[a, b]`, and for every `x` in the half-open interval `[a, b)`, `f` has a right derivative at `x` within the set of all real numbers greater than or equal to `x`, then if the norm of the right derivative of `f` at any point in the half-open interval `[a, b)` is bounded by a real number `C`, it follows that for each `x` in the closed interval `[a, b]`, the norm of the difference between `f(x)` and `f(a)` is less than or equal to `C` times the difference between `x` and `a`. This is a result in mathematical analysis that sets a bound on the change in a function based on bounds on its derivative.
More concisely: If a real-valued function `f` is continuous on a closed interval `[a, b]`, has a right derivative on the half-open interval `[a, b)`, and the norm of its right derivative is bounded on this interval, then the norm of `f(x) - f(a)` is less than or equal to the norm of the interval endpoint difference multiplied by the supremum of the right derivative's norm for all `x` in `[a, b)`.
|
eq_of_has_deriv_right_eq
theorem eq_of_has_deriv_right_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' g : ℝ → E},
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt g (f' x) (Set.Ici x) x) →
ContinuousOn f (Set.Icc a b) → ContinuousOn g (Set.Icc a b) → f a = g a → ∀ y ∈ Set.Icc a b, f y = g y
The theorem `eq_of_has_deriv_right_eq` states that: given two continuous functions `f` and `g` on the closed interval from `a` to `b` which are equal at `a`, if both functions have the same right derivative for each point in the left-closed right-open interval from `a` to `b`, then `f` and `g` are equal at every point in the closed interval from `a` to `b`. Here a function has a right derivative at a point if the function's derivative at that point exists when approaching from values greater than or equal to the point.
More concisely: If continuous functions `f` and `g` on the closed interval `[a, b]` have the same right derivative on `(a, b]` and are equal at `a`, then they are equal on `[a, b]`.
|
hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt
theorem hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt :
∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {G : Type u_4} [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{H : Type u_5} [inst_3 : NormedAddCommGroup H] [inst_4 : NormedSpace 𝕜 H] {f : G → H} {f' : G → G →L[𝕜] H}
{x : G}, (∀ᶠ (y : G) in nhds x, HasFDerivAt f (f' y) y) → ContinuousAt f' x → HasStrictFDerivAt f (f' x) x
The theorem `hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt` states that for a function `f` from a normed additive group `G` to another normed additive group `H`, both over a field `𝕜` which is either the real numbers or the complex numbers, if `f` has a derivative `f'` at each point in a neighborhood of a point `x` in `G` and if `f'` is continuous at `x`, then `f` is strictly differentiable at `x` with respect to `f'`. In mathematical terms, this means that if `f` has a derivative in the neighborhood of a point and this derivative is continuous at that point, then the function is strictly differentiable at that point.
More concisely: If a function `f` from a normed additive group `G` to another normed additive group `H` over a field `𝕜` has a continuous derivative at a point `x` in `G`, then `f` is strictly differentiable at `x`.
|
image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary
theorem image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary :
∀ {a b : ℝ} {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {f' : ℝ → ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope (norm ∘ f) x z < r) →
∀ {B B' : ℝ → ℝ},
‖f a‖ ≤ B a →
ContinuousOn B (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, ‖f x‖ = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
This theorem, known as the general fencing theorem for continuous functions with an estimate on the derivative, states that for two continuous functions `f` and `B` on a closed interval `[a, b]`, with `‖f a‖ ≤ B a`, and `B` having a right derivative at every point of the open interval `[a, b)`. If for each `x` in the open interval `[a, b)`, the right-side limit inferior of `(‖f z‖ - ‖f x‖) / (z - x)` is bounded above by a function `f'`, and whenever `‖f x‖ = B x`, we have `f' x < B' x`, then `‖f x‖ ≤ B x` holds everywhere on the closed interval `[a, b]`.
This essentially provides a constraint for the derivative of a function at the boundary, which results in an upper bound for the norm of the function over the entire interval.
More concisely: If functions `f` and `B` are continuous on a closed interval `[a, b]` with `‖f a‖ ≤ B a`, `B` having a right derivative on `[a, b)`, and the right-limit inferior of `(‖f z‖ - ‖f x‖) / (z - x)` is bounded above by `f'` for all `x < z` in `[a, b)`, and `‖f x‖ = B x` implies `f' x < B' x`, then `‖f x‖ ≤ B x` for all `x` in `[a, b]`.
|
antitoneOn_of_deriv_nonpos
theorem antitoneOn_of_deriv_nonpos :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D → DifferentiableOn ℝ f (interior D) → (∀ x ∈ interior D, deriv f x ≤ 0) → AntitoneOn f D
The theorem `antitoneOn_of_deriv_nonpos` states that, given a function `f` that is continuous on a convex (or equivalently, connected) subset `D` of the real line, if `f` is differentiable on the interior of `D` and the derivative of `f` is nonpositive (i.e., less than or equal to zero) throughout the interior of `D`, then `f` is an antitone function on `D`. An antitone function is one for which an increase in the input value results in a decrease in the output value. In other words, for any two points in `D`, if the first point is less than or equal to the second, then the value of `f` at the second point is less than or equal to the value of `f` at the first point.
More concisely: If a continuous, convex function `f` with a nonpositive derivative on its interior is differentiable, then `f` is antitone on its domain.
|
eq_of_derivWithin_eq
theorem eq_of_derivWithin_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {g : ℝ → E},
DifferentiableOn ℝ f (Set.Icc a b) →
DifferentiableOn ℝ g (Set.Icc a b) →
Set.EqOn (derivWithin f (Set.Icc a b)) (derivWithin g (Set.Icc a b)) (Set.Ico a b) →
f a = g a → ∀ y ∈ Set.Icc a b, f y = g y
The theorem `eq_of_derivWithin_eq` states that given two differentiable functions `f` and `g` on a closed interval `[a, b]`, if they have the same derivative within the interval `[a, b]` for every point in the half-open interval `[a, b)` and if they are equal at the point `a`, then the two functions are equal everywhere on the closed interval `[a, b]`. In other words, if two functions have the same derivatives and are equal at the start of an interval, then they are equal throughout the entire interval. This is a formal statement in Lean 4 of a well-known result in calculus.
More concisely: If two differentiable functions on a closed interval have the same derivative at all points in the interval and are equal at one point, then they are equal everywhere on the interval.
|
strictMono_of_deriv_pos
theorem strictMono_of_deriv_pos : ∀ {f : ℝ → ℝ}, (∀ (x : ℝ), 0 < deriv f x) → StrictMono f
The theorem `strictMono_of_deriv_pos` states that for any function `f` mapping real numbers to real numbers, if the derivative of `f` is positive for all real numbers, then `f` is strictly monotone. This means that if `a` is less than `b`, then `f(a)` is less than `f(b)`. Note that the requirement for `f` to be differentiable is implicit since we are assuming that the derivative of `f` exists and is strictly positive.
More concisely: If a real-valued function has strictly positive derivative on the real numbers, then it is strictly monotone.
|
Convex.is_const_of_fderivWithin_eq_zero
theorem Convex.is_const_of_fderivWithin_eq_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f : E → G} {s : Set E} {x y : E},
Convex ℝ s → DifferentiableOn 𝕜 f s → (∀ x ∈ s, fderivWithin 𝕜 f s x = 0) → x ∈ s → y ∈ s → f x = f y
The theorem `Convex.is_const_of_fderivWithin_eq_zero` states that if a function has a zero Fréchet derivative at every point of a convex set, then the function is constant on that set. More formally, given a set `s` of elements of a certain type `E`, if `s` is convex, the function `f` is differentiable on `s`, and the Fréchet derivative of `f` within `s` at any point `x` in `s` is zero, then for any two points `x` and `y` in `s`, `f(x)` is equal to `f(y)`. Thus, the function `f` takes the same value at every point in the convex set `s`.
More concisely: If a differentiable function has a zero Fréchet derivative at every point of a convex set, then the function is constant on that set.
|
Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt
theorem Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{s : Set E} {x : E} {f' : E → E →L[𝕜] G},
Convex ℝ s →
∀ {f : E → G},
(∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) →
ContinuousWithinAt f' s x → ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
The theorem states that if we have a convex set `s` in a real normed vector space `E` and a function `f : E → G` that is differentiable within `s` in a neighborhood of a point `x : E` with derivative `f'`, and if `f'` is continuous within `s` at `x`, then for any positive real number `K` larger than the non-negative norm of `f' x`, there exists a neighborhood of `x` within `s` where `f` is Lipschitz with Lipschitz constant `K`. The theorem also points out that there is another version of this theorem which provides an explicit estimate on the Lipschitz constant.
More concisely: If a differentiable function `f` with continuous derivative on a convex set `s` in a real normed vector space has a derivative of norm larger than a positive constant `K` at a point `x` in `s`, then there exists a neighborhood of `x` in `s` where `f` is Lipschitz continuous with Lipschitz constant `K`.
|
image_norm_le_of_norm_deriv_right_le_deriv_boundary'
theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
∀ {B B' : ℝ → ℝ},
‖f a‖ ≤ B a →
ContinuousOn B (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
The theorem, known as the general fencing theorem for continuous functions with an estimate on the norm of the derivative, states that given two continuous functions `f` and `B` on a closed interval `[a, b]`, if the norm of `f` at `a` is less than or equal to `B` at `a`, `f` and `B` have right derivatives `f'` and `B'` respectively at every point in the half-open interval `[a, b)`, and the norm of `f'` at any point in `[a, b)` is less than or equal to `B` at that point, then the norm of `f` at any point in `[a, b]` is less than or equal to `B` at that point. This theorem allows for piecewise differentiable functions as it uses one-sided derivatives in the assumptions.
More concisely: If two continuous functions on a closed interval have matching norms at an interior point and the norm of one's derivative is less than or equal to that of the other at each interior point, then the norm of the first function is less than or equal to the norm of the second function at every point in the interval.
|
image_le_of_liminf_slope_right_lt_deriv_boundary'
theorem image_le_of_liminf_slope_right_lt_deriv_boundary' :
∀ {f f' : ℝ → ℝ} {a b : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) →
∀ {B B' : ℝ → ℝ},
f a ≤ B a →
ContinuousOn B (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
This theorem, known as the General fencing theorem for continuous functions with an estimate on the derivative, states the following:
Let `f` and `B` be continuous functions defined on the closed interval `[a, b]` with the following properties:
- `f(a)` is less than or equal to `B(a)`,
- `B` has a right derivative `B'` at every point in the half-open interval `[a, b)`,
- for every `x` in the half-open interval `[a, b)`, the right-side limit inferior of `(f(z) - f(x)) / (z - x)` is bounded above by a function `f'`,
- and whenever `f(x)` is equal to `B(x)`, `f'(x)` is strictly less than `B'(x)`.
Then the theorem asserts that `f(x)` is less than or equal to `B(x)` for all `x` in the closed interval `[a, b]`.
More concisely: If `f` is a continuous function on the closed interval `[a, b]` with `f(a) ≤ B(a)`, `B` is continuous on `[a, b]` with a right derivative `B'` on `[a, b)`, the right-limit inferiors of `(f(z) - f(x)) / (z - x)` are bounded above by a function `f'`, and `f(x) = B(x)` implies `f'(x) < B'(x)`, then `f(x) ≤ B(x)` for all `x` in `[a, b]`.
|
norm_image_sub_le_of_norm_deriv_le_segment'
theorem norm_image_sub_le_of_norm_deriv_le_segment' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E}
{C : ℝ},
(∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
(∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ C) → ∀ x ∈ Set.Icc a b, ‖f x - f a‖ ≤ C * (x - a)
This theorem states that given a function `f` which maps real numbers to a normed additive commutative group `E`, and a real-valued function `f'` that represents the derivative of `f`, if `f` has a derivative `f'` within the closed interval `[a, b]` for all `x` in `[a, b]` and the norm of `f'` within the half-open interval `[a, b)` is bounded by a real number `C`, then for all `x` in `[a, b]`, the norm of the difference between `f(x)` and `f(a)` is less than or equal to `C` times the difference between `x` and `a`. In simpler terms, the theorem provides a bound on the change in the function `f` in terms of the maximum allowed rate of change (`C`) and the distance from `a` as per the Mean Value Theorem.
More concisely: If a real-valued function `f` with derivative `f'` on the interval `[a, b]` satisfies `∀x∈[a,b]. ∥f'(x)∥ ≤ C` and `f` is differentiable on `[a, b]`, then `∥f(x) - f(a)∥ ≤ C * (x - a)` for all `x ∈ [a, b]`.
|
norm_image_sub_le_of_norm_deriv_le_segment
theorem norm_image_sub_le_of_norm_deriv_le_segment :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b C : ℝ},
DifferentiableOn ℝ f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, ‖derivWithin f (Set.Icc a b) x‖ ≤ C) → ∀ x ∈ Set.Icc a b, ‖f x - f a‖ ≤ C * (x - a)
The theorem `norm_image_sub_le_of_norm_deriv_le_segment` states that for a function `f` from reals (`ℝ`) to a normed additive commutative group (`E`), if the function `f` is differentiable on a closed interval `[a, b]` and the norm of the derivative of `f` within this interval is bounded by a real number `C`, then for any `x` in the interval `[a, b]`, the norm of the difference `f(x) - f(a)` is less than or equal to `C` times `(x - a)`. This theorem essentially provides a bound on the change in `f` in terms of the bound on its derivative.
More concisely: Given a real-valued, differentiable function `f` on a closed interval `[a, b]` with derivative norm `C`, the norm of `f(x) - f(a)` is bounded by `C * (x - a)` for all `x` in `[a, b]`.
|
image_sub_lt_mul_sub_of_deriv_lt
theorem image_sub_lt_mul_sub_of_deriv_lt :
∀ {f : ℝ → ℝ},
Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), deriv f x < C) → ∀ ⦃x y : ℝ⦄, x < y → f y - f x < C * (y - x)
The theorem `image_sub_lt_mul_sub_of_deriv_lt` states that for a differentiable function `f : ℝ → ℝ`, if the derivative of `f` at any point is less than a constant `C`, then the function `f` grows slower than `C * x` on the domain of real numbers. More specifically, for any two real numbers `x` and `y` such that `x < y`, the difference `f y - f x` is less than `C * (y - x)`. This means that the increase in the value of the function `f` is always less than `C` times the increase in the input value, demonstrating that the function's rate of change is bounded by `C`.
More concisely: If `f : ℝ → ℝ` is differentiable with `|df/dx(x)| < C` for some constant `C`, then `|f(y) - f(x)| < C * |y - x|` for all `x, y ∈ ℝ` with `x < y`.
|
Convex.norm_image_sub_le_of_norm_fderiv_le
theorem Convex.norm_image_sub_le_of_norm_fderiv_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f : E → G} {C : ℝ} {s : Set E} {x y : E},
(∀ x ∈ s, DifferentiableAt 𝕜 f x) →
(∀ x ∈ s, ‖fderiv 𝕜 f x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
This theorem, called the mean value theorem on a convex set, states the following: Given a convex set `s` and a function `f` that is differentiable at every point in `s`, if the norm of the derivative of `f` at any point is bounded by a real number `C`, then the function `f` is `C`-Lipschitz. In other words, for any two points `x` and `y` in the set `s`, the norm of the difference of the function values at `y` and `x` is less than or equal to `C` times the norm of the difference between `y` and `x`. This is a powerful statement about the rate of change of a function over a convex set.
More concisely: Given a convex set and a differentiable function with bounded derivative norm, the function is Lipschitz continuous with constant equal to the supremum of the derivative norm.
|
domain_mvt
theorem domain_mvt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x y : E}
{f' : E → E →L[ℝ] ℝ},
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
Convex ℝ s → x ∈ s → y ∈ s → ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
This theorem is a version of Lagrange's Mean Value Theorem, specifically applied to convex domains. In mathematical terms, given a normed additively commutative group `E` and a normed space over `E`, if `f` is a function from `E` to real numbers, `s` is a set in `E`, and `f'` is the derivative of `f` within the set `s`, the theorem states that if `x` and `y` are any two points in the set `s` and the set `s` is convex, then there exists a point `z` on the line segment between `x` and `y` such that the difference in function values at `y` and `x` is equal to the derivative of the function at point `z` applied to the difference between `y` and `x`. This theorem generalizes the usual Mean Value Theorem by allowing the domain to be a convex set in a vector space, rather than an interval on the real line.
More concisely: Given a convex set `s` in a normed vector space and a real-valued differentiable function `f` on `s`, there exists `z` in the line segment between any two points `x` and `y` in `s` such that `f(y) - f(x) = f'(z) * (y - x)`.
|
image_le_of_deriv_right_le_deriv_boundary
theorem image_le_of_deriv_right_le_deriv_boundary :
∀ {f f' : ℝ → ℝ} {a b : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
∀ {B B' : ℝ → ℝ},
f a ≤ B a →
ContinuousOn B (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, f' x ≤ B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
The theorem, "image_le_of_deriv_right_le_deriv_boundary", states the general fencing theorem for continuous functions with an estimate on the derivative. Given two continuous functions `f` and `B` on the closed interval [a, b] with the properties that `f(a) ≤ B(a)`, `B` has a derivative `B'` everywhere on ℝ, `f` has a right derivative `f'` at every point of the open interval [a, b), and `f'(x) ≤ B'(x)` on the open interval [a, b), then it follows that the function `f(x)` is less than or equal to `B(x)` everywhere on the closed interval [a, b]. The theorem therefore provides an upper bound for a function based on its derivative and a boundary function with its derivative.
More concisely: If continuous functions $f$ and $B$ on the closed interval $[a, b]$ satisfy $f(a) \leq B(a)$, $B$ is differentiable on $\mathbb{R}$, $f$ is right-differentiable on $[a, b)$, and $f'(x) \leq B'(x)$ for all $x \in (a, b)$, then $f(x) \leq B(x)$ for all $x \in [a, b]$.
|
image_le_of_deriv_right_lt_deriv_boundary'
theorem image_le_of_deriv_right_lt_deriv_boundary' :
∀ {f f' : ℝ → ℝ} {a b : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
∀ {B B' : ℝ → ℝ},
f a ≤ B a →
ContinuousOn B (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
The theorem states a general fencing condition for continuous functions with an estimate on the derivative. Suppose there are two continuous functions `f` and `B` on the closed interval `[a, b]` such that `f(a) ≤ B(a)`; `B` has a right derivative `B'` at every point in the half-open interval `[a, b)`; `f` also has a right derivative `f'` at every point in the half-open interval `[a, b)`; and whenever `f(x) = B(x)`, the derivative of `f` at `x` is less than the derivative of `B` at `x`. Then, for every real number `x` in the closed interval `[a, b]`, `f(x)` is less than or equal to `B(x)`. This theorem can be used to bound a function `f` by another function `B` given certain conditions on their derivatives.
More concisely: If functions `f` and `B` are continuous on `[a, b]` with `f(a) ≤ B(a)`, `B` has a right derivative on `[a, b)`, `f` has a right derivative on `[a, b)`, and `f(x) ≤ B'(x)` whenever `f(x) = B(x)`, then `f(x) ≤ B(x)` for all `x` in `[a, b]`.
|
norm_image_sub_le_of_norm_deriv_le_segment_01'
theorem norm_image_sub_le_of_norm_deriv_le_segment_01' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → E} {C : ℝ},
(∀ x ∈ Set.Icc 0 1, HasDerivWithinAt f (f' x) (Set.Icc 0 1) x) →
(∀ x ∈ Set.Ico 0 1, ‖f' x‖ ≤ C) → ‖f 1 - f 0‖ ≤ C
This theorem states that for any function `f` from real numbers to a normed additive commutative group `E`, if the derivative of `f` exists within the closed interval `[0, 1]`, and the norm of the derivative within the half-open interval `[0, 1)` is bounded by a real number `C`, then the norm of the difference between `f(1)` and `f(0)` is less than or equal to `C`. In other words, if a function has its derivative's norm controlled by `C` in the interval from 0 to 1, then the change in function values between 0 and 1 is also controlled by `C`.
More concisely: If `f` is a real-valued differentiable function on the interval [0, 1] with the property that the norm of its derivative is bounded by `C` on [0, 1), then the norm of `f(1) - f(0)` is less than or equal to `C`.
|
strictMonoOn_of_deriv_pos
theorem strictMonoOn_of_deriv_pos :
∀ {D : Set ℝ},
Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, 0 < deriv f x) → StrictMonoOn f D
The theorem `strictMonoOn_of_deriv_pos` states that if we have a function `f` that is continuous on a convex (or equivalently, connected) subset `D` of the real numbers, and if the derivative of `f` is strictly positive on the interior of `D`, then we can conclude that `f` is strictly monotone on `D`. This means that for any `a` and `b` in `D`, if `a < b`, then `f(a) < f(b)`. We do not require differentiability of `f` to be explicitly stated, as this is implied by the condition of the derivative being strictly positive. Essentially, the theorem says that a differentiable function with a strictly positive derivative over a convex subset of the real line is strictly increasing in that interval.
More concisely: If a real-valued function is continuous on a convex subset of the real numbers and has a strictly positive derivative on its interior, then it is strictly increasing on that subset.
|
Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le
theorem Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f : E → G} {s : Set E} {C : NNReal},
DifferentiableOn 𝕜 f s → (∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
This theorem is known as the mean value theorem on a convex set. It basically asserts that, if a function's derivative is bounded by a nonnegative real number `C` on a set `s`, then the function is `C`-Lipschitz on `s`. More specifically, this version of the theorem uses `fderivWithin` and `LipschitzOnWith`. It applies to a function `f` mapping from a normed additive commutative group `E` to another such group `G` and a convex set `s` of `E`. Here, `C`-Lipschitz means that for all `x` and `y` in `s`, the distance between `f(x)` and `f(y)` is at most `C` times the distance between `x` and `y`. Moreover, the function is differentiable on `s` and the norm of the derivative of `f` at any point in `s` is less than or equal to `C`.
More concisely: If a convex set `s` in a normed additive commutative group `E` and a function `f: E → G` between two normed additive commutative groups with bounded derivative `C` on `s`, then `f` is `C`-Lipschitz on `s`.
|
mul_sub_le_image_sub_of_le_deriv
theorem mul_sub_le_image_sub_of_le_deriv :
∀ {f : ℝ → ℝ},
Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), C ≤ deriv f x) → ∀ ⦃x y : ℝ⦄, x ≤ y → C * (y - x) ≤ f y - f x
The theorem `mul_sub_le_image_sub_of_le_deriv` states that for a real-valued function `f` that is differentiable on the real numbers, if there exists a real number `C` such that `C` is less than or equal to the derivative of `f` at any point, then the function `f` grows at least as fast as `C * x`. This means that for any real numbers `x` and `y` where `x` is less than or equal to `y`, the quantity `C * (y - x)` is less than or equal to `f y - f x`. This theorem is a formalization of the idea that the derivative of a function at a point gives us a lower bound on how fast the function is increasing at that point.
More concisely: For a real-valued, differentiable function `f` and any `x` and `y` with `x <= y`, `C * (y - x) <= f(y) - f(x)` holds if `C` is less than or equal to the derivative of `f` at every point.
|
norm_image_sub_le_of_norm_deriv_le_segment_01
theorem norm_image_sub_le_of_norm_deriv_le_segment_01 :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {C : ℝ},
DifferentiableOn ℝ f (Set.Icc 0 1) → (∀ x ∈ Set.Ico 0 1, ‖derivWithin f (Set.Icc 0 1) x‖ ≤ C) → ‖f 1 - f 0‖ ≤ C
The theorem `norm_image_sub_le_of_norm_deriv_le_segment_01` states that, for any real-valued function `f` defined on the closed interval `[0, 1]`, if `f` is differentiable on this interval and the norm of its derivative within this interval is bounded by a real number `C`, then the norm of the difference between the function values at the endpoints of the interval (i.e., `f(1) - f(0)`) is less than or equal to `C`. This is a formal statement of the property that the difference between the function values at the endpoints of the interval is controlled by the maximal rate of change of the function on the interval.
More concisely: If a real-valued function differentiable on $[0,1]$ with bounded derivative norm has norm of difference between endpoints less than or equal to the supremum of its derivative norm.
|
image_le_of_liminf_slope_right_lt_deriv_boundary
theorem image_le_of_liminf_slope_right_lt_deriv_boundary :
∀ {f f' : ℝ → ℝ} {a b : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) →
∀ {B B' : ℝ → ℝ},
f a ≤ B a →
(∀ (x : ℝ), HasDerivAt B (B' x) x) →
(∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
The theorem `image_le_of_liminf_slope_right_lt_deriv_boundary` states that for two continuous real-valued functions `f` and `B` defined on a closed interval `[a, b]`, and given that `f a ≤ B a`, `B` has a derivative `B'` everywhere on the real numbers, and for each `x` in the half-open interval `[a, b)`, the right-side limit inferior of `(f z - f x) / (z - x)` (the slope of `f` at `x`) is upper bounded by another function `f'`, such that whenever `f x = B x`, it holds that `f' x < B' x`. Under these conditions, the theorem states that `f x ≤ B x` holds for all `x` in the closed interval `[a, b]`.
In simpler terms, this theorem provides a boundary for the function `f` by another function `B` under certain conditions related to the slopes of `f` and `B` and the relationship between the functions at the endpoints of the interval.
More concisely: Under the given conditions of continuity, differentiability, and slope bounds on functions `f` and `B` on a closed interval, if `f(a) ≤ B(a)` holds and `f(x) ≤ B(x)` at every `x` in `[a, b)` where `f` takes the right-limit inferior of its slope, then `f(x) ≤ B(x)` for all `x` in the interval `[a, b]`.
|
Convex.lipschitzOnWith_of_nnnorm_deriv_le
theorem Convex.lipschitzOnWith_of_nnnorm_deriv_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f : 𝕜 → G} {s : Set 𝕜} {C : NNReal},
(∀ x ∈ s, DifferentiableAt 𝕜 f x) → (∀ x ∈ s, ‖deriv f x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
This theorem, known as the mean value theorem on a convex set in one dimensional space, states that if the derivative of a function `f` is bounded by a nonnegative real number `C` on a set `s`, then the function `f` is `C`-Lipschitz on `s`. Here, a function being `C`-Lipschitz means that for all `x, y` in `s`, the distance between `f(x)` and `f(y)` is less than or equal to `C` times the distance between `x` and `y`. The conditions for this theorem to hold are that every point `x` in `s` is differentiable and the norm of the derivative of `f` at any point `x` in `s` is less than or equal to `C`. Lastly, the set `s` needs to be convex in the real numbers.
More concisely: If a real-valued function `f` is differentiable with a bounded derivative on a convex set `s` in the real numbers, then `f` is `C`-Lipschitz on `s`.
|
image_norm_le_of_norm_deriv_right_lt_deriv_boundary
theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
∀ {B B' : ℝ → ℝ},
‖f a‖ ≤ B a →
(∀ (x : ℝ), HasDerivAt B (B' x) x) →
(∀ x ∈ Set.Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
The theorem `image_norm_le_of_norm_deriv_right_lt_deriv_boundary` is a general fencing theorem for continuous functions with an estimate on the norm of the derivative. It states that if we have two continuous functions `f` and `B` on a closed interval `[a, b]`, and the following conditions hold:
* The norm of `f` at `a` is less than or equal to `B` at `a`.
* The function `f` has a right derivative `f'` at every point in the half-open interval `[a, b)`.
* The function `B` has a derivative `B'` everywhere on the real line.
* Whenever the norm of `f` at a point equals `B` at that point, the norm of the derivative `f'` at that point is strictly less than `B'` at that point.
Then, it follows that the norm of `f` at any point `x` in the closed interval `[a, b]` is less than or equal to `B` at `x`. This theorem is useful for piecewise differentiable functions, as it uses one-sided derivatives in the assumptions.
More concisely: If `f` is a continuous function on a closed interval `[a, b]` with `f(a)` bounded by `B`, `B` being a differentiable function with strictly smaller derivative than `f'` whenever `f = B`, then `|f(x)| ≤ |B(x)|` for all `x ∈ [a, b]`.
|
Convex.norm_image_sub_le_of_norm_fderivWithin_le
theorem Convex.norm_image_sub_le_of_norm_fderivWithin_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f : E → G} {C : ℝ} {s : Set E} {x y : E},
DifferentiableOn 𝕜 f s →
(∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
The theorem, known as the Mean Value Theorem on a convex set, states that if a function `f` from `E` to `G` is differentiable on a set `s` and the norm of its derivative within `s` is bounded by a real number `C`, then the function `f` is `C`-Lipschitz. This means that the difference between the function values at any two points `x` and `y` in the set `s` is less than or equal to `C` times the distance between `x` and `y`. The derivative of the function `f` is taken with respect to the set `s`, and the set `s` is assumed to be convex.
More concisely: If a differentiable function `f` on a convex set `s` has a bounded derivative norm, then `f` is Lipschitz continuous on `s` with constant `C`.
|
Convex.lipschitzOnWith_of_nnnorm_derivWithin_le
theorem Convex.lipschitzOnWith_of_nnnorm_derivWithin_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f : 𝕜 → G} {s : Set 𝕜} {C : NNReal},
Convex ℝ s → DifferentiableOn 𝕜 f s → (∀ x ∈ s, ‖derivWithin f s x‖₊ ≤ C) → LipschitzOnWith C f s
The theorem `Convex.lipschitzOnWith_of_nnnorm_derivWithin_le` is a version of the mean value theorem in one dimension, applied on a convex set. It states that if a function `f` is differentiable on a convex set `s` and its derivative within `s` at any point `x` is bounded by a nonnegative real number `C`, then `f` is `C`-Lipschitz continuous on `s`. In other words, for all `x, y` in `s`, the distance between `f(x)` and `f(y)` is less than or equal to `C` times the distance between `x` and `y`.
More concisely: If a convex function `f` with a bounded derivative on a convex set `s` is differentiable at every point, then `f` is Lipschitz continuous on `s` with constant equal to the supremum of the derivatives' absolute values.
|
Convex.mul_sub_le_image_sub_of_le_deriv
theorem Convex.mul_sub_le_image_sub_of_le_deriv :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D →
DifferentiableOn ℝ f (interior D) →
∀ {C : ℝ}, (∀ x ∈ interior D, C ≤ deriv f x) → ∀ x ∈ D, ∀ y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x
The theorem `Convex.mul_sub_le_image_sub_of_le_deriv` states that if we have a function `f` which is continuous on a convex subset `D` of the real numbers, and is differentiable on the interior of `D` with `f'` being greater or equal to some real number `C`, then the growth of `f` is at least as fast as `C * x` on `D`. More formally, for any two points `x, y` in `D` where `x ≤ y`, the inequality `C * (y - x) ≤ f y - f x` holds true. This theorem encapsulates the idea that the slope of the function at any point in the interior of `D` gives a lower bound for the growth of the function.
More concisely: If a continuous, convex-domain function `f` with a differentiable interior is such that its derivative is greater than or equal to `C` on the interior, then for any `x, y` in `D` with `x ≤ y`, we have `C * (y - x) ≤ f y - f x`.
|
strictAntiOn_of_deriv_neg
theorem strictAntiOn_of_deriv_neg :
∀ {D : Set ℝ},
Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, deriv f x < 0) → StrictAntiOn f D
The theorem `strictAntiOn_of_deriv_neg` states that if a function `f` is continuous on a convex (or equivalently, connected) subset `D` of the real numbers, and if `f` is differentiable on the interior of `D` with a negative derivative, then `f` is a strictly decreasing function on `D`. In other words, for any given `a` and `b` in `D`, if `a` is less than `b`, then `f(b)` is less than `f(a)`.
More concisely: If a real-valued function `f` is continuous on a convex set `D` and differentiable on its interior with negatively valued derivatives, then `f` is strictly decreasing on `D`.
|
strictAnti_of_deriv_neg
theorem strictAnti_of_deriv_neg : ∀ {f : ℝ → ℝ}, (∀ (x : ℝ), deriv f x < 0) → StrictAnti f
The theorem named `strictAnti_of_deriv_neg` states that for any real-valued function `f` defined on the real numbers, if the derivative of `f` at any point `x` is less than zero, then `f` is strictly decreasing. In other words, `f` is a strictly antitone function, which means for any two real numbers `a` and `b` such that `a < b`, we have `f(a) > f(b)`. The requirement that `f` is differentiable is not explicitly stated as it is inherently implied by the condition that the derivative of `f` is strictly negative at each point.
More concisely: If a real-valued function `f` has strictly negative derivatives at every point, then `f` is a strictly decreasing function.
|
mul_sub_lt_image_sub_of_lt_deriv
theorem mul_sub_lt_image_sub_of_lt_deriv :
∀ {f : ℝ → ℝ},
Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), C < deriv f x) → ∀ ⦃x y : ℝ⦄, x < y → C * (y - x) < f y - f x
The theorem `mul_sub_lt_image_sub_of_lt_deriv` states that for a differentiable function `f` mapping real numbers to real numbers, if a given real number `C` is less than the derivative of `f` at any point, then `f` grows faster than `C` times `x`. More specifically, for any two real numbers `x` and `y` where `x` is less than `y`, the difference of `f(y)` and `f(x)` is greater than `C` times the difference of `y` and `x`. This means the increase in `f` over the interval from `x` to `y` is greater than what would be the increase for a linear function with slope `C` over the same interval.
More concisely: For a differentiable function `f` and real numbers `x` < `y`, if `f'(x)` < `C`, then `f(y) - f(x)` > `C * (y - x)`.
|
hasStrictDerivAt_of_hasDerivAt_of_continuousAt
theorem hasStrictDerivAt_of_hasDerivAt_of_continuousAt :
∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {G : Type u_4} [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f f' : 𝕜 → G} {x : 𝕜},
(∀ᶠ (y : 𝕜) in nhds x, HasDerivAt f (f' y) y) → ContinuousAt f' x → HasStrictDerivAt f (f' x) x
The theorem `hasStrictDerivAt_of_hasDerivAt_of_continuousAt` states that for any continuously differentiable function `f` with derivative `f'` in either the real or complex numbers, if for every point `y` in the neighborhood of a point `x`, `f` has a derivative `f'(y)` at `y`, and if `f'` is continuous at `x`, then `f` is strictly differentiable at `x` with the strict derivative being `f'(x)`. In mathematical terms, if `f` satisfies `f y - f z = (y - z) • f' + o(y - z)` as `y, z → x`, it is called strictly differentiable. This theorem links the concepts of differentiability and continuity to strict differentiability.
More concisely: If a continuously differentiable function with continuous derivative has the property that the difference `f(y) - f(z)` approaches `(y-z) * f'(x)` as `y, z` approach `x`, then `f` is strictly differentiable at `x` with strict derivative `f'(x)`.
|
Convex.lipschitzOnWith_of_nnnorm_fderiv_le
theorem Convex.lipschitzOnWith_of_nnnorm_fderiv_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f : E → G} {s : Set E} {C : NNReal},
(∀ x ∈ s, DifferentiableAt 𝕜 f x) → (∀ x ∈ s, ‖fderiv 𝕜 f x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
This theorem, known as the mean value theorem on a convex set, states that if a function's derivative is bounded by a constant `C` on a set `s`, then the function itself is `C`-Lipschitz on `s`. This version of the theorem incorporates the `fderiv` function (which gives a derivative of the function at a point) and `LipschitzOnWith` (which states that a function is Lipschitz continuous with a given constant on a specified set). Specifically, for a function `f` from a normed additive commutative group `E` to another `G`, both over a normed space `𝕜`, if every point `x` in set `s` is such that `f` is differentiable at `x` and the norm of the derivative at `x` is less than or equal to `C`, and if `s` is a convex set in the real numbers, then `f` is `C`-Lipschitz on `s`. This theorem gives a relationship between the boundedness of a function's derivative and its Lipschitz continuity.
More concisely: If a real-valued function on a convex set is differentiable with bounded derivative, then it is Lipschitz continuous with constant equal to the supremum of the derivative's absolute values.
|
Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
theorem Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{s : Set E} {x : E} {f' : E → E →L[𝕜] G},
Convex ℝ s →
∀ {f : E → G},
(∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) →
ContinuousWithinAt f' s x → ∀ (K : NNReal), ‖f' x‖₊ < K → ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
This theorem states that if `s` is a convex set in a real normed vector space `E`, and `f : E → G` is a function that is differentiable within `s` in a neighborhood of a point `x : E` with derivative `f'`, and assuming that `f'` is continuous within `s` at `x`, then for any nonnegative real number `K` greater than the nonnegative norm of `f' x`, there exists some neighborhood of `x` within `s` on which `f` is `K`-Lipschitz. In simpler terms, if we have a function that is differentiable and its derivative is continuous at a point within a convex set, then we can find a neighborhood of that point where the function does not change too quickly, for a specific rate specified by `K`. The rate `K` is chosen to be larger than the norm of the derivative at the point `x`.
More concisely: If `s` is a convex set in a real normed vector space, `f : E → G` is differentiable with continuous derivative `f'` within `s` at point `x`, then there exists a neighborhood `U` of `x` in `s` such that `|f(y) - f(z)| ≤ K ||y - z||` for all `y, z ∈ U`, where `K > ||f' x||`.
|
exists_ratio_hasDerivAt_eq_ratio_slope
theorem exists_ratio_hasDerivAt_eq_ratio_slope :
∀ (f f' : ℝ → ℝ) {a b : ℝ},
a < b →
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
∀ (g g' : ℝ → ℝ),
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
∃ c ∈ Set.Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
This is a statement of Cauchy's Mean Value Theorem in the context of real-valued functions. It states that given two functions `f` and `g` which are continuous on a closed interval `[a, b]` and differentiable on the open interval `(a, b)`, there exists a point `c` in the open interval `(a, b)` such that the ratio of the differences of `f` and `g` at the endpoints of the interval, i.e. `(g b - g a) / (f b - f a)`, equals the ratio of their derivatives at the point `c`, that is `(g' c) / (f' c)`. Here, `f'` and `g'` denote the derivatives of `f` and `g` respectively. The theorem essentially states that at some point in `(a, b)`, the rates of change of the two functions are proportional to the overall rate of change over the interval.
More concisely: Given two real-valued functions `f` and `g` that are continuous on a closed interval `[a, b]` and differentiable on the open interval `(a, b)`, there exists a point `c` in `(a, b)` such that `(g(b) - g(a)) / (f(b) - f(a)) = (g'(c)) / (f'(c))`.
|
exists_hasDerivAt_eq_slope
theorem exists_hasDerivAt_eq_slope :
∀ (f f' : ℝ → ℝ) {a b : ℝ},
a < b →
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) → ∃ c ∈ Set.Ioo a b, f' c = (f b - f a) / (b - a)
This Lean theorem is a version of Lagrange's Mean Value Theorem for real-valued functions using the `HasDerivAt` definition. It states that, for any two real-valued functions `f` and `f'` and any two real numbers `a` and `b` such that `a` is less than `b`, if `f` is a continuous function on the closed interval from `a` to `b` and for every `x` in the open interval from `a` to `b`, `f` has a derivative at `x` that equals `f'(x)`, there exists a `c` in the open interval from `a` to `b` such that `f'(c)` equals the slope of the secant line through `(a, f(a))` and `(b, f(b))`, that is, `(f(b) - f(a)) / (b - a)`. In other words, there is a point `c` in the open interval where the instantaneous rate of change of the function equals the average rate of change over the interval.
More concisely: If a real-valued function `f` is continuous on a closed interval [`a`, `b`] and differentiable on the open interval `(a, b)`, then there exists a `c` in `(a, b)` such that `f'(c) = (f(b) - f(a)) / (b - a)`.
|
Convex.image_sub_le_mul_sub_of_deriv_le
theorem Convex.image_sub_le_mul_sub_of_deriv_le :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D →
DifferentiableOn ℝ f (interior D) →
∀ {C : ℝ}, (∀ x ∈ interior D, deriv f x ≤ C) → ∀ x ∈ D, ∀ y ∈ D, x ≤ y → f y - f x ≤ C * (y - x)
The theorem `Convex.image_sub_le_mul_sub_of_deriv_le` states that given a convex subset `D` of the real numbers ℝ, and a function `f` that is continuous on `D` and differentiable on the interior of `D`, if the derivative of `f` is less than or equal to some real number `C` on the interior of `D`, then the function `f` does not grow faster than `C * x` on `D`. More formally, for any two real numbers `x` and `y` in `D` where `x` is less than or equal to `y`, the difference `f y - f x` is less than or equal to `C * (y - x)`. In other words, this theorem provides a bound on the growth of a function based on its derivative.
More concisely: If a continuous, differentiable function with derivative less than or equal to some constant on the interior of a convex domain satisfies the mean value theorem, then the function is bounded above by the constant times the difference of any two points in the domain.
|
monotoneOn_of_deriv_nonneg
theorem monotoneOn_of_deriv_nonneg :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D → DifferentiableOn ℝ f (interior D) → (∀ x ∈ interior D, 0 ≤ deriv f x) → MonotoneOn f D
The theorem `monotoneOn_of_deriv_nonneg` states that given a set `D` of real numbers that is convex, and a real-valued function `f` which is continuous on `D` and differentiable on the interior of `D`. If the derivative of `f` is nonnegative on the interior of `D`, then `f` is a monotone function on `D`. In simpler terms, if a function is continuous and its derivative is nonnegative within a convex set of real numbers, then the function is increasing or constant on that set.
More concisely: If a continuous, differentiable function with non-negative derivative on the interior of a convex set defines a relation that is monotonic on that set.
|
lipschitzWith_of_nnnorm_deriv_le
theorem lipschitzWith_of_nnnorm_deriv_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f : 𝕜 → G} {C : NNReal}, Differentiable 𝕜 f → (∀ (x : 𝕜), ‖deriv f x‖₊ ≤ C) → LipschitzWith C f
This theorem is a one-dimensional version of the Mean Value Theorem. It states that if a function `f` is differentiable over a field `𝕜` and its derivative at any point `x` in `𝕜` has a non-negative norm (`‖deriv f x‖₊`) bounded by a non-negative real number `C`, then the function `f` is `C`-Lipschitz continuous. In other words, for all points `x` and `y` in the field `𝕜`, the distance between `f(x)` and `f(y)` is less than or equal to `C` times the distance between `x` and `y`.
More concisely: If a differentiable function `f` over a field `𝕜` has a norm-bounded derivative with non-negative norm, then `f` is `C`-Lipschitz continuous. (The distance between `f(x)` and `f(y)` is less than or equal to `C` times the distance between `x` and `y` for all `x, y` in `𝕜`.)
|
exists_ratio_deriv_eq_ratio_slope'
theorem exists_ratio_deriv_eq_ratio_slope' :
∀ (f : ℝ → ℝ) {a b : ℝ},
a < b →
∀ (g : ℝ → ℝ) {lfa lga lfb lgb : ℝ},
DifferentiableOn ℝ f (Set.Ioo a b) →
DifferentiableOn ℝ g (Set.Ioo a b) →
Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa) →
Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga) →
Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb) →
Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb) →
∃ c ∈ Set.Ioo a b, (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c
The theorem `exists_ratio_deriv_eq_ratio_slope'` is an extended version of Cauchy's Mean Value Theorem involving derivatives. The theorem states that for two real-valued functions `f` and `g` which are differentiable in the open interval `(a, b)` of real numbers, if function `f` tends towards `lfa` and `lfb` at point `a` and `b` respectively within the open interval `(a, ∞)` and `(-∞, b)` respectively, and function `g` tends towards `lga` and `lgb` at point `a` and `b` respectively within the same intervals as `f`, then there exists a point `c` in the open interval `(a, b)` such that the difference in the limit values of `g` times the derivative of `f` at `c` is equal to the difference in the limit values of `f` times the derivative of `g` at `c`. In mathematical notation, `∃ c ∈ (a, b), (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c`.
More concisely: For real-valued functions `f` and `g` with open interval derivatives in `(a, b)`, if `f` and `g` approach `lfa`, `lfb`, `lga`, and `lgb` at `a` and `b` respectively, then there exists `c` in `(a, b)` such that `(lgb - lga) * f'(c) = (lfb - lfa) * g'(c)`.
|
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
theorem Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f : E → G} {C : ℝ} {s : Set E} {x y : E} {f' : E → E →L[𝕜] G},
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
(∀ x ∈ s, ‖f' x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
This theorem is a version of the Mean Value Theorem for a convex set. It states that if we have a function `f` from a normed additively commutative group `E` to another normed additively commutative group `G`, where `E` and `G` are normed spaces over some types `𝕜` and `ℝ` respectively, then given a real number `C`, a set `s` of type `E`, and two elements `x` and `y` of type `E`, if the function `f` has a derivative `f'` at every point in the set `s` and the norm of the derivative `f'` at every point in the set `s` is less than or equal to `C`, and if the set `s` is convex over real numbers, then the norm of the difference of the function `f` values at `y` and `x` is less than or equal to `C` times the norm of the difference between `y` and `x`. In simpler terms, if the derivative of a function is bounded by `C` on a convex set, then the function is `C`-Lipschitz.
More concisely: Given a convex set `s` in a normed additive commutative group `E` over `ℝ`, and a function `f` from `E` to another normed additive commutative group `G` over `𝕜`, if `f` has a Lipschitz continuous derivative `f'` of norm at most `C` on `s`, then `f` is `C`-Lipschitz on `s`.
|
Convex.eqOn_of_fderivWithin_eq
theorem Convex.eqOn_of_fderivWithin_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f g : E → G} {s : Set E} {x : E},
Convex ℝ s →
DifferentiableOn 𝕜 f s →
DifferentiableOn 𝕜 g s →
UniqueDiffOn 𝕜 s →
(∀ x ∈ s, fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x) → x ∈ s → f x = g x → Set.EqOn f g s
The theorem asserts that if two functions, say `f` and `g`, have the same Fréchet derivatives at every point in a convex set `s`, and they are equal at one point within that set `s`, then those two functions are equal everywhere in set `s`. Here, `f` and `g` are differentiable on `s`, `s` is a convex set, and `s` has the unique differential property (meaning, each tangent vector within `s` can be extended to a unique derivation of the algebra of smooth functions on `s`). This theorem essentially says that in a convex set, a function is entirely determined by its derivative and its value at one single point.
More concisely: If two differentiable functions on a convex set with the unique differential property have equal Fréchet derivatives at every point and are equal at one point, then they are equal everywhere on the set.
|
exists_deriv_eq_slope
theorem exists_deriv_eq_slope :
∀ (f : ℝ → ℝ) {a b : ℝ},
a < b →
ContinuousOn f (Set.Icc a b) →
DifferentiableOn ℝ f (Set.Ioo a b) → ∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)
This is a Lean 4 version of Lagrange's Mean Value Theorem specifically for real-valued functions. The theorem states that for any real-valued function `f`, if `f` is continuous on a closed interval `[a, b]` and differentiable on the open interval `(a, b)`, then there exists a point `c` in `(a, b)` such that the derivative of `f` at `c` is equal to the slope of the secant line through `(a, f(a))` and `(b, f(b))`. The slope of the secant line is given by `(f b - f a) / (b - a)`. This is the key result in calculus that provides a geometric interpretation for derivatives and leads to the fundamental theorem of calculus.
More concisely: If a real-valued function `f` is continuous on a closed interval `[a, b]` and differentiable on the open interval `(a, b)`, then there exists a point `c` in `(a, b)` such that `f'(c) = (f(b) - f(a)) / (b - a)`.
|
image_norm_le_of_norm_deriv_right_le_deriv_boundary
theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
∀ {B B' : ℝ → ℝ},
‖f a‖ ≤ B a →
(∀ (x : ℝ), HasDerivAt B (B' x) x) →
(∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
The theorem `image_norm_le_of_norm_deriv_right_le_deriv_boundary` is a general fencing principle for continuous functions with an estimate on the norm of the derivative. Suppose `f` and `B` are continuous functions on the closed interval `[a, b]` satisfying the following conditions:
1. The norm of `f` at `a` is less than or equal to `B` at `a`;
2. The function `f` has a right derivative `f'` at every point in the half-open interval `[a, b)`;
3. The function `B` has a derivative `B'` everywhere on the real numbers;
4. The norm of the derivative `f'` is less than or equal to `B` everywhere on the half-open interval `[a, b)`.
Then the theorem states that the norm of `f` at any `x` in the closed interval `[a, b]` is less than or equal to `B` at `x`. This theorem allows for piecewise differentiable functions by utilizing one-sided derivatives in its assumptions.
More concisely: If `f` is a continuous function on the closed interval `[a, b]` with a right derivative `f'` on `[a, b)`, and the norm of `f'` is less than or equal to a continuous function `B` with a derivative everywhere, such that `||f(a)|| <= ||B(a)||`, then `||f(x)|| <= ||B(x)||` for all `x` in `[a, b]`.
|
image_le_of_deriv_right_lt_deriv_boundary
theorem image_le_of_deriv_right_lt_deriv_boundary :
∀ {f f' : ℝ → ℝ} {a b : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
∀ {B B' : ℝ → ℝ},
f a ≤ B a →
(∀ (x : ℝ), HasDerivAt B (B' x) x) →
(∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
The theorem `image_le_of_deriv_right_lt_deriv_boundary` is a general fencing theorem for continuous functions with an estimate on the derivative. It states that given two real-valued continuous functions `f` and `B` on a closed interval `[a, b]` such that:
- `f` is less than or equal to `B` at the point `a`;
- `B` has a derivative `B'` at every point on the real line;
- `f` has a right derivative `f'` at every point of the semi-closed interval `[a, b)`;
- and whenever `f` and `B` are equal, `f'` is less than `B'`.
Then, `f` is less than or equal to `B` at every point on the closed interval `[a, b]`. This theorem essentially states that if `f` and `B` meet and `f` is increasing at a slower rate than `B`, then `f` cannot exceed `B`.
More concisely: If two real-valued continuous functions `f` and `B` on a closed interval `[a, b]` satisfy `f(a) <= B(a)`, `B` is differentiable, `f` is right-differentiable, and `f'(x) < B'(x)` whenever `f(x) = B(x)`, then `f(x) <= B(x)` for all `x` in `[a, b]`.
|
Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le
theorem Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f f' : 𝕜 → G} {s : Set 𝕜} {C : NNReal},
Convex ℝ s → (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → (∀ x ∈ s, ‖f' x‖₊ ≤ C) → LipschitzOnWith C f s
This theorem, named `Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le`, states that if we have a function whose derivative is bounded by some nonnegative number `C` on a convex set `s` in a real normed space, then the function is `C`-Lipschitz on `s`. Here, a function being `C`-Lipschitz means that the distance between the function values at any two points in `s` is at most `C` times the distance between the two points. This is a version of the mean value theorem in one dimension, but specified with the `HasDerivWithinAt` and `LipschitzOnWith` definitions. The exact conditions are that the set `s` is convex, the function `f` has a derivative `f'` at every point in `s`, and the norm of `f'` at every point in `s` is less than or equal to `C`.
More concisely: If a convex function on a real normed space has a derivative with norm bounded by `C` at every point, then it is `C`-Lipschitz on that set.
|
Convex.norm_image_sub_le_of_norm_deriv_le
theorem Convex.norm_image_sub_le_of_norm_deriv_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f : 𝕜 → G} {s : Set 𝕜} {x y : 𝕜} {C : ℝ},
(∀ x ∈ s, DifferentiableAt 𝕜 f x) →
(∀ x ∈ s, ‖deriv f x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
This theorem, known as the mean value theorem on a convex set in one dimension, states that if the derivative of a function `f` is bounded by a real number `C` at all points `x` in a set `s`, then the function `f` is `C`-Lipschitz on that set. In other words, for any two points `x` and `y` in the set `s`, the norm of the difference between the function values at `y` and `x` (i.e., `‖f y - f x‖`) is less than or equal to `C` times the norm of the difference between `y` and `x` (i.e., `C * ‖y - x‖`). This theorem requires that the set `s` is convex and the function `f` is differentiable at every point in the set.
More concisely: If a differentiable function on a convex set in one dimension has a bounded derivative, then it is Lipschitz continuous with constant equal to the supremum of its derivative.
|
Convex.norm_image_sub_le_of_norm_derivWithin_le
theorem Convex.norm_image_sub_le_of_norm_derivWithin_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f : 𝕜 → G} {s : Set 𝕜} {x y : 𝕜} {C : ℝ},
DifferentiableOn 𝕜 f s →
(∀ x ∈ s, ‖derivWithin f s x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
The theorem `Convex.norm_image_sub_le_of_norm_derivWithin_le` states that if you have a function `f` which is differentiable on a set `s` and the norm of the derivative of `f` within `s` is bounded by a real constant `C`, then if `s` is a convex set, for any two points `x` and `y` in `s`, the difference between the function values at `y` and `x` is bounded by `C` times the difference between `y` and `x`. This is a version of the mean value theorem on a convex set in dimension 1, and it essentially states that if the derivative of a function on a set is bounded, then the function is `C`-Lipschitz on that set.
More concisely: If a differentiable function on a convex set has a bounded derivative norm, then it is Lipschitz continuous on that set.
|
monotone_of_deriv_nonneg
theorem monotone_of_deriv_nonneg : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → (∀ (x : ℝ), 0 ≤ deriv f x) → Monotone f := by
sorry
The theorem `monotone_of_deriv_nonneg` states that given a function `f` from real numbers to real numbers that is differentiable (every point in its domain has a derivative), if the derivative of `f` at any point is nonnegative (i.e., greater than or equal to zero), then the function `f` is monotone. In mathematical terms, if `f'` is nonnegative (i.e., `0 ≤ f'(x)` for all `x` in the domain of `f`), then `f` is a monotone function, meaning that for any two real numbers `a` and `b`, if `a ≤ b`, then `f(a) ≤ f(b)`. This theorem is a statement about the connection between the sign of the derivative of a function and the monotonicity of the function itself.
More concisely: If a real-valued function `f` is differentiable with nonnegative derivative, then `f` is monotone.
|
Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
theorem Convex.norm_image_sub_le_of_norm_hasDerivWithin_le :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f f' : 𝕜 → G} {s : Set 𝕜} {x y : 𝕜} {C : ℝ},
(∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
(∀ x ∈ s, ‖f' x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
The theorem `Convex.norm_image_sub_le_of_norm_hasDerivWithin_le` is a version of the Mean Value Theorem on a convex set in one-dimensional space, stated with the `HasDerivWithinAt` notation. This theorem asserts that if the derivative of a function `f` is bounded by a real number `C` within a set `s`, then `f` is `C`-Lipschitz within `s`. More precisely, given two points `x` and `y` in `s`, the norm of the difference between the values of `f` at `y` and `x` is less than or equal to `C` times the norm of the difference between `y` and `x`. This condition holds for all `x` in `s` where `f` has a derivative at `x` within `s`, and `s` is a convex set in the real numbers.
More concisely: If a convex function on the real numbers has a derivative bounded by `C` within a convex set `s`, then it is `C`-Lipschitz on `s`.
|
Convex.image_sub_lt_mul_sub_of_deriv_lt
theorem Convex.image_sub_lt_mul_sub_of_deriv_lt :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D →
DifferentiableOn ℝ f (interior D) →
∀ {C : ℝ}, (∀ x ∈ interior D, deriv f x < C) → ∀ x ∈ D, ∀ y ∈ D, x < y → f y - f x < C * (y - x)
The theorem `Convex.image_sub_lt_mul_sub_of_deriv_lt` states that if `f` is a real-valued function that is continuous on a convex subset `D` of the real numbers and differentiable on the interior of `D`, and if the derivative of `f` at any point in the interior of `D` is less than some real number `C`, then for any two points `x` and `y` in `D` where `x` is less than `y`, the difference `f(y) - f(x)` is less than `C` times the difference `(y - x)`. In other words, if a continuous function's derivative is less than a constant `C` on the interior of a convex set, then the function grows slower than `C * x` on that set.
More concisely: If `f` is a real-valued, continuous function on a convex subset `D` of the real numbers with derivative less than `C` on the interior of `D`, then for any `x, y` in `D` with `x < y`, we have `f(y) - f(x) < C * (y - x)`.
|
image_le_of_liminf_slope_right_le_deriv_boundary
theorem image_le_of_liminf_slope_right_le_deriv_boundary :
∀ {f : ℝ → ℝ} {a b : ℝ},
ContinuousOn f (Set.Icc a b) →
∀ {B B' : ℝ → ℝ},
f a ≤ B a →
ContinuousOn B (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) →
∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
The theorem `image_le_of_liminf_slope_right_le_deriv_boundary` is a general fencing theorem for continuous functions with an estimate on the derivative. It states that if we have two continuous functions `f` and `B` on a closed interval `[a, b]` such that `f(a) ≤ B(a)`, `B` has a right derivative `B'` at every point in the half-open interval `[a, b)`, and for each `x` in `[a, b)` the right-side limit inferior (the infimum of the set of limits of all sequences that converge to `x` from the right) of the slope `(f(z) - f(x)) / (z - x)` is less than or equal to `B'`, then `f(x) ≤ B(x)` for all `x` in `[a, b]`. This theorem essentially provides a bound on the function `f` based on its slope and the derivative of the function `B`.
More concisely: If `f` and `B` are continuous functions on a closed interval `[a, b]` with `f(a) ≤ B(a)`, `B` has a right derivative `B'` on `[a, b)`, and for all `x` in `[a, b)`, the right-limit inferior of the slope `(f(z) - f(x)) / (z - x)` is less than or equal to `B'`, then `f(x) ≤ B(x)` for all `x` in `[a, b]`.
|
image_sub_le_mul_sub_of_deriv_le
theorem image_sub_le_mul_sub_of_deriv_le :
∀ {f : ℝ → ℝ},
Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), deriv f x ≤ C) → ∀ ⦃x y : ℝ⦄, x ≤ y → f y - f x ≤ C * (y - x)
The theorem `image_sub_le_mul_sub_of_deriv_le` states that for any differentiable real-valued function `f`, if the derivative of `f` at any point is less than or equal to some real number `C`, then the function `f` cannot grow faster than `C * x`. In other words, the difference between the function values at any two points `y` and `x` (with `y` greater than or equal to `x`) is always less than or equal to `C` times the difference between `y` and `x`.
More concisely: For any differentiable real-function `f` and real numbers `x` and `y` with `x <= y`, if `|f'(x)| <= C`, then `|f(y) - f(x)| <= C * |y - x|`.
|
is_const_of_deriv_eq_zero
theorem is_const_of_deriv_eq_zero :
∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
{f : 𝕜 → G}, Differentiable 𝕜 f → (∀ (x : 𝕜), deriv f x = 0) → ∀ (x y : 𝕜), f x = f y
The theorem `is_const_of_deriv_eq_zero` states that if a function `f` that maps from a domain `𝕜` to a range `G` is differentiable everywhere and its derivative is zero at all points in its domain, then it is a constant function. Here, `𝕜` can be either real numbers `R` or complex numbers `ℂ`, and `G` is a normed additive commutative group over `𝕜`. In other words, if the rate of change of a function is always zero, the function does not change and thus is constant.
More concisely: If a function is differentiable with zero derivative at all points in its domain over a normed additive commutative group, then it is a constant function.
|
Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
theorem Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
[inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
{f : E → G} {s : Set E} {f' : E → E →L[𝕜] G} {C : NNReal},
(∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → (∀ x ∈ s, ‖f' x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
This theorem, referred to as the mean value theorem on a convex set, states that if the derivative of a function is bounded by a real number `C` within a set `s`, then the function is `C`-Lipschitz continuous on `s`. In this context, a function is `C`-Lipschitz continuous on `s` means that for every pair of points `x, y` in `s`, the distance between the function values at `x` and `y` is less than or equal to `C` times the distance between `x` and `y`. This theorem requires that the set `s` is convex and the derivative of the function exists and is bounded within `s`. It is formulated using the concepts of `HasFDerivWithinAt` and `LipschitzOnWith`.
More concisely: If a real-valued function has a bounded derivative within a convex set, then it is Lipschitz continuous on that set with constant equal to the supremum of its derivative.
|
antitone_of_deriv_nonpos
theorem antitone_of_deriv_nonpos : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → (∀ (x : ℝ), deriv f x ≤ 0) → Antitone f := by
sorry
This theorem states that, given a function `f` mapping real numbers to real numbers, if `f` is differentiable and the derivative of `f` at any real number is less than or equal to zero, then `f` is an antitone function. In mathematical terms, an antitone function is one for which an increase in the input value results in a decrease in the output value. In other words, if the derivative of a function is nonpositive everywhere, then the function is decreasing or non-increasing.
More concisely: If a real-valued function `f` is differentiable with everywhere nonpositive derivative, then `f` is antitone.
|
image_norm_le_of_norm_deriv_right_lt_deriv_boundary'
theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
∀ {B B' : ℝ → ℝ},
‖f a‖ ≤ B a →
ContinuousOn B (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
(∀ x ∈ Set.Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
The theorem `image_norm_le_of_norm_deriv_right_lt_deriv_boundary'` is a general fencing theorem for continuous functions accompanied by an estimate on the norm of the derivative. It states that if you have two continuous functions `f` and `B` on a closed interval `[a, b]` with the properties:
* The norm of `f` at `a` is less than or equal to `B` at `a`;
* `f` and `B` have right-sided derivatives `f'` and `B'` respectively at every point in the right-closed left-open interval `[a, b)`;
* Whenever the norm of `f` at `x` equals `B` at `x`, the norm of `f'` is strictly less than `B'`.
Then the norm of `f` at any point `x` in the interval `[a, b]` is always less than or equal to `B` at `x`. This theorem is formulated with one-sided derivatives to accommodate piecewise differentiable functions.
More concisely: If two continuous functions `f` and `B` on a closed interval `[a, b]` satisfy the given conditions on their norms and derivatives, then the norm of `f(x)` is less than or equal to `B(x)` for all `x` in `[a, b]`.
|