eVariationOn.lowerSemicontinuous_uniformOn
theorem eVariationOn.lowerSemicontinuous_uniformOn :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (s : Set α),
LowerSemicontinuous fun f => eVariationOn f s
The theorem `eVariationOn.lowerSemicontinuous_uniformOn` states that for any set `s` in a linear order `α` and functions from `α` to a pseudo emetric space `E`, the function that maps `f` to its extended real-valued variation on `s`, denoted `(eVariationOn f s)`, is lower semicontinuous. In other words, for any `f` and any `ε > 0`, there exists a neighborhood of `f` such that for all `f'` in this neighborhood, the variation of `f'` on `s` is at least the variation of `f` on `s` minus `ε`. This is an important property in the study of variation of functions, ensuring that small changes in the function do not lead to a sudden jump in its variation.
More concisely: The function that maps a function from a linearly ordered set to its extended real-valued variation on that set is lower semicontinuous.
|
LipschitzOnWith.locallyBoundedVariationOn
theorem LipschitzOnWith.locallyBoundedVariationOn :
∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {C : NNReal} {s : Set ℝ},
LipschitzOnWith C f s → LocallyBoundedVariationOn f s
The theorem `LipschitzOnWith.locallyBoundedVariationOn` states that for any function `f` from real numbers to a type `E` (where `E` is a type equipped with a pseudo e-metric space structure), a nonnegative real number `C`, and a set `s` of real numbers, if the function `f` is Lipschitz continuous with constant `C` on the set `s`, then the function `f` has locally bounded variation on the set `s`. In more mathematical terms, for all `x, y` in `s`, if the extended distance between `f(x)` and `f(y)` is less than or equal to `C` times the extended distance between `x` and `y`, then for any interval `[a, b]` with endpoints in `s`, the function `f` has finite variation on the intersection of `s` and the closed interval from `a` to `b`.
More concisely: If a Lipschitz continuous function `f` on a set `s` of real numbers, with constant `C`, has its extended distance less than or equal to `C` times the regular difference between any two points in `s`, then `f` has finite variation on every closed interval within `s`.
|
eVariationOn.eq_zero_iff
theorem eVariationOn.eq_zero_iff :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α},
eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
This theorem states that for any type `α` having a linear order and any type `E` in a pseudo emetric space, and for any function `f` from `α` to `E`, the extended real valued variation of `f` on a set `s` of `α` is zero if and only if the extended distance between the image of any two elements `x` and `y` in `s` under `f` is zero. In other words, the variation of the function `f` on the set `s` is zero precisely when `f` is constant on `s`.
More concisely: For any function from a linearly ordered type to a pseudometric space, the variation of the function on a set is zero if and only if the images of any two distinct elements in the set have zero distance.
|
LocallyBoundedVariationOn.ae_differentiableWithinAt
theorem LocallyBoundedVariationOn.ae_differentiableWithinAt :
∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
{f : ℝ → V} {s : Set ℝ},
LocallyBoundedVariationOn f s →
MeasurableSet s → ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
The theorem `LocallyBoundedVariationOn.ae_differentiableWithinAt` states that for any real-valued function `f` mapping into a finite dimensional real vector space `V`, if `f` has locally bounded variation on a set `s` and `s` is a measurable set, then `f` is differentiable almost everywhere within this set `s` with respect to the measure defined by `MeasureTheory.volume.restrict s`. Here, "almost everywhere" means that the set of points in `s` where `f` is not differentiable has measure zero.
More concisely: If a real-valued function `f` on a measurable set `s` with finite dimensional real vector space values has locally bounded variation, then `f` is almost everywhere differentiable with respect to the Lebesgue measure restricted to `s`.
|
LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real
theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real :
∀ {f : ℝ → ℝ} {s : Set ℝ}, LocallyBoundedVariationOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x := by
sorry
This theorem states that if a function `f` mapping real numbers to real numbers has locally bounded variation on a set `s`, then, except possibly on a set of measure zero (almost everywhere), for each real number `x` in `s`, the function `f` is differentiable at `x` within the set `s`. In mathematical terms, this means that for almost all `x` in `s`, there exists a derivative of `f` at `x` within `s`. The term "locally bounded variation" means that the function does not oscillate too wildly within any given interval. The theorem is superseded by `ae_differentiableWithinAt_of_mem`, meaning that there is a more general or updated theorem that replaces this one.
More concisely: If a real-valued function `f` has locally bounded variation on a set `s`, then it is almost everywhere differentiable within `s`.
|
variationOnFromTo.eq_neg_swap
theorem variationOnFromTo.eq_neg_swap :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
(a b : α), variationOnFromTo f s a b = -variationOnFromTo f s b a
The theorem `variationOnFromTo.eq_neg_swap` states that for any function `f` mapping from an arbitrary type `α` (with a linear order structure) to another type `E` (with a pseudo emetric space structure), and for any set `s` of elements of type `α`, and any two elements `a` and `b` of type `α`, the signed variation of the function `f` on the interval from `a` to `b` intersected with the set `s` is equal to the negative of the signed variation of `f` on the interval from `b` to `a` intersected with the same set `s`. This essentially reflects the concept that reversing the order of the interval endpoints changes the sign of the variation.
More concisely: For any function `f` from a linearly ordered type `α` to a pseudo metric space `E`, and any set `s` and elements `a` and `b` in `α`, the signed variation of `f` on the interval `[a, b]` intersected with `s` equals the negative of the signed variation of `f` on the interval `[b, a]` intersected with `s`.
|
LipschitzOnWith.ae_differentiableWithinAt_of_mem_real
theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem_real :
∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
{C : NNReal} {f : ℝ → V} {s : Set ℝ},
LipschitzOnWith C f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
The theorem `LipschitzOnWith.ae_differentiableWithinAt_of_mem_real` states that for any real-valued function `f` mapping into a finite-dimensional real vector space `V`, if `f` is Lipschitz continuous with a non-negative constant `C` on a set `s`, then `f` is differentiable almost everywhere on `s`. In other words, for almost every real number `x` in `s`, the function `f` has a derivative at the point `x` within the set `s`. This is a particular case of the Rademacher's theorem, assuming that the target vector space is finite-dimensional.
More concisely: If a real-valued function on a set is Lipschitz continuous with a non-negative constant, then it is differentiable almost everywhere on that set (in the context of finite-dimensional real vector spaces).
|
variationOnFromTo.eq_of_le
theorem variationOnFromTo.eq_of_le :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
{a b : α}, a ≤ b → variationOnFromTo f s a b = (eVariationOn f (s ∩ Set.Icc a b)).toReal
This theorem states that for any type `α` with a linear order, any pseudo-emetric space `E`, any function `f` from `α` to `E`, and any set `s` of `α`, and for any `a` and `b` in `α` where `a` is less than or equal to `b`, the signed variation of `f` on the interval `[a, b]` (inclusive) intersected with the set `s` is equal to the real value conversion of the extended real-valued variation of `f` on the intersection of set `s` and the interval `[a, b]`. This is essentially expressing a property about how the function's variation behaves on a specific interval when the order of the endpoints is certain.
More concisely: For any linear order `α`, pseudo-metric space `E`, function `f` from `α` to `E`, set `s` of `α`, and `a ≤ b` in `α`, the signed variation of `f` on the interval `[a, b]` intersected with `s` equals the real value conversion of the extended real-valued variation of `f` on `s ∩ [a, b]`.
|
variationOnFromTo.add
theorem variationOnFromTo.add :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
LocallyBoundedVariationOn f s →
∀ {a b c : α},
a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c
This theorem states that for any function `f` of type `α → E`, where `α` has a linear order and `E` is a pseudo-emetric space, and any set `s` of type `α`, if the function `f` has locally bounded variation on the set `s`, then for any three elements `a`, `b`, `c` of the set `s`, the sum of the variation of `f` on the interval from `a` to `b` and the variation of `f` on the interval from `b` to `c` equals the variation of `f` on the interval from `a` to `c`. In mathematical terms, the theorem asserts that if `f` has locally bounded variation on `s`, then for all `a`, `b`, `c` in `s`, `V_f(a, b) + V_f(b, c) = V_f(a, c)`, where `V_f(a, b)` denotes the variation of `f` from `a` to `b`.
More concisely: Given a function `f` of type `α → E` on a linearly ordered set `α` with locally bounded variation, the sum of the variations of `f` between any three consecutive elements equals the variation between the first and the last. In other words, for all `a`, `b`, `c` in `α`, `V_f(a, b) + V_f(b, c) = V_f(a, c)`.
|
LipschitzOnWith.ae_differentiableWithinAt_real
theorem LipschitzOnWith.ae_differentiableWithinAt_real :
∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
{C : NNReal} {f : ℝ → V} {s : Set ℝ},
LipschitzOnWith C f s →
MeasurableSet s → ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
The theorem `LipschitzOnWith.ae_differentiableWithinAt_real` states that if you have a real function `f` mapping into a finite dimensional real vector space `V` that is Lipschitz continuous on a set `s`, then `f` is differentiable almost everywhere within this set `s`. 'Almost everywhere' means that the set of points where this property fails has measure zero. The Lipschitz continuity condition assures that the distance between the images of any two points in `s` is at most some constant `C` times the distance between the points themselves. The theorem applies specifically to the case where the source space is the real numbers (`ℝ`). The measurability condition on `s` enables us to make sense of the concept of 'almost everywhere'.
More concisely: If a real-valued function on a Lebesgue measurable set is Lipschitz continuous, then it is almost everywhere differentiable.
|
LipschitzWith.ae_differentiableAt_real
theorem LipschitzWith.ae_differentiableAt_real :
∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
{C : NNReal} {f : ℝ → V}, LipschitzWith C f → ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
The theorem states that if we have a function `f` from real numbers to a finite dimensional real vector space, which is Lipschitz continuous with a non-negative real constant `C`, then `f` is differentiable almost everywhere. This is a specific case of the Rademacher theorem. The more general version of this theorem, `LipschitzWith.ae_differentiableAt`, does not specify the dimensionality of the source space.
More concisely: A Lipschitz continuous real-valued function on a real vector space is almost everywhere differentiable.
|
LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn
theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn :
∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α},
LocallyBoundedVariationOn f s → ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
This theorem states that, for any real-valued function which has locally bounded variation on a set, it can be represented as the difference of two functions that are both monotone on the same set. More concretely, given a function `f` from a linearly ordered type `α` to real numbers, and a set `s` of type `α`, if `f` has locally bounded variation on `s`, then there exist two functions `p` and `q`, such that both `p` and `q` are monotone on `s`, and `f` is equal to the difference of `p` and `q`.
More concisely: Given a real-valued function `f` on a linearly ordered type `α` with locally bounded variation on a set `s`, there exist monotone functions `p` and `q` on `s` such that `f = p - q`.
|
eVariationOn.union
theorem eVariationOn.union :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s t : Set α}
{x : α}, IsGreatest s x → IsLeast t x → eVariationOn f (s ∪ t) = eVariationOn f s + eVariationOn f t
The theorem `eVariationOn.union` states that if for any two sets `s` and `t` in a linear order space, if `s` is located to the left of `t`, and both sets contain a common boundary point `x`; then the variation of a function `f` along the union of `s` and `t` is equal to the sum of the variations of `f` along `s` and `t`. Here, "variation of a function `f`" means the supremum of the sum of the extended distance (using the pseudo-emetric space structure) between `f` applied at consecutive terms over all finite increasing sequences in a set. The terms "greatest" and "least" refer to the unique maximum and minimum elements in a set under a pre-order structure.
More concisely: If sets $s$ and $t$ in a linear order space have a common boundary point $x$ with $s$ to the left of $t$, then the variation of a function $f$ on the union of $s$ and $t$ equals the sum of its variations on $s$ and $t$: $\operatorname{Var}_s(f) + \operatorname{Var}_t(f) = \operatorname{Var}_{s \cup t}(f)$.
|
eVariationOn.add_le_union
theorem eVariationOn.add_le_union :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s t : Set α},
(∀ x ∈ s, ∀ y ∈ t, x ≤ y) → eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
The theorem `eVariationOn.add_le_union` states that for any function `f` mapping from a type `α` (under a linear order) to a type `E` (under a pseudo emetric space), and for any two sets `s` and `t` of the type `α` such that every element `x` of `s` is less than or equal to every element `y` of `t`, then the sum of the extended real-valued variations of `f` over `s` and `t` is less than or equal to the variation of `f` over the union of `s` and `t`. Here, the variation of a function on a set is defined as the supremum of the sum of the extended distances between the function values at subsequent points over all finite increasing sequences in the set.
More concisely: For any function from a linearly ordered type to a pseudometric space, the variation of the function on the union of two sets is greater than or equal to the sum of the variations on each set, provided every element in the first set is less than or equal to every element in the second set.
|
eVariationOn.add_point
theorem eVariationOn.add_point :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
{x : α},
x ∈ s →
∀ (u : ℕ → α),
Monotone u →
(∀ (i : ℕ), u i ∈ s) →
∀ (n : ℕ),
∃ v m,
Monotone v ∧
(∀ (i : ℕ), v i ∈ s) ∧
x ∈ v '' Set.Iio m ∧
((Finset.range n).sum fun i => edist (f (u (i + 1))) (f (u i))) ≤
(Finset.range m).sum fun j => edist (f (v (j + 1))) (f (v j))
The theorem `eVariationOn.add_point` states that for any linearly ordered type `α` and pseudo-emetric space `E`, given a function `f` from `α` to `E`, a set `s` of `α`, and a point `x` in `s`; for any monotone sequence `u` of points in `s`, one can always find another monotone sequence `v` and a natural number `m`, such that `v` also encompasses all points in `s`, `x` is a member of the set of images of `v` over all points less than `m`, and the sum of the distances between consecutive points in `u` over the range `n` is less than or equal to the sum of the distances between consecutive points in `v` over the range `m`. Essentially, it says that the variation of `f` along `u` is bounded by its variation along `v` when an additional point `x` is added to the set `s`.
More concisely: For any linearly ordered type `α`, pseudo-metric space `E`, function `f` from `α` to `E`, set `s` of `α`, point `x` in `s`, and monotone sequences `u` and `v` in `s`, there exists a natural number `m` such that `v` encompasses all points in `s`, `x` is in the image of `v` over the first `m` elements, and the variation of `f` along `u` over `n` points is less than or equal to the variation of `f` along `v` over `m` points.
|
eVariationOn.sum_le
theorem eVariationOn.sum_le :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
(n : ℕ) {u : ℕ → α},
Monotone u →
(∀ (i : ℕ), u i ∈ s) → ((Finset.range n).sum fun i => edist (f (u (i + 1))) (f (u i))) ≤ eVariationOn f s
The theorem `eVariationOn.sum_le` states that for any linear order `α`, any pseudo eMetric space `E`, any function `f` from `α` to `E`, any set `s` of `α`, any natural number `n`, and any monotone function `u` from natural numbers to `α` such that every `u i` is in `s`, the sum over the range of `n` of the extended distance between `f (u (i + 1))` and `f (u i)` is less than or equal to the eVariation of `f` on `s`. In other words, the sum of extended distances over an increasing sequence in the set is bounded by the eVariation of the function on the set. This is a property related to the variation of functions in mathematical analysis.
More concisely: For any linear order α, pseudo metric space E, function f from α to E, set s of α, natural number n, and monotone function u from natural numbers to α with every ui in s, the sum of extended distances between f (ui+1) and f (ui) over the range of n is less than or equal to the eVariation of f on s.
|
LocallyBoundedVariationOn.ae_differentiableAt
theorem LocallyBoundedVariationOn.ae_differentiableAt :
∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
{f : ℝ → V}, LocallyBoundedVariationOn f Set.univ → ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
This theorem states that for any function `f` mapping real numbers to a finite-dimensional real vector space `V`, if `f` has locally bounded variation over the set of all real numbers (`Set.univ`), then `f` is differentiable at almost every point in the domain, i.e., the set of real numbers. Here, differentiability of `f` at a point means that `f` has a derivative at that point, and "almost everywhere" signifies that the set of points where this property fails has measure zero.
More concisely: If a real function `f` mapping to a finite-dimensional real vector space has locally bounded variation on the real numbers, then `f` is differentiable almost everywhere.
|
LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi
theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi :
∀ {ι : Type u_4} [inst : Fintype ι] {f : ℝ → ι → ℝ} {s : Set ℝ},
LocallyBoundedVariationOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
The theorem `LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi` asserts that if a function `f` mapping from real numbers to a finite-dimensional product vector space, indexed by `ι`, has locally bounded variation on a set `s` of real numbers, then almost everywhere in `s`, the function `f` is differentiable. In other words, for almost all real numbers `x` in the set `s`, there exists a derivative of the function `f` at the point `x` within the set `s`.
More concisely: If a real-valued function `f` on a set `s` has locally bounded variation, then it is almost everywhere differentiable on `s`.
|
LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem
theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem :
∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
{f : ℝ → V} {s : Set ℝ}, LocallyBoundedVariationOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
This theorem states that for any real-valued function `f` mapping into a finite dimensional real vector space `V`, if `f` has locally bounded variation on a set `s`, then `f` is differentiable almost everywhere within the set `s`. In simpler terms, if a function's output varies in a bounded manner within certain local regions of its domain, then the function is most likely differentiable at almost all points within those regions. This is a fundamental result in real analysis and the theory of functions of a real variable.
More concisely: If a real-valued function on a finite dimensional real vector space has locally bounded variation, then it is differentiable almost everywhere.
|
variationOnFromTo.eq_of_ge
theorem variationOnFromTo.eq_of_ge :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
{a b : α}, b ≤ a → variationOnFromTo f s a b = -(eVariationOn f (s ∩ Set.Icc b a)).toReal
This theorem states that for any types `α` and `E`, given that `α` has a linear order and `E` is a pseudo-emetric space, for any function `f` from `α` to `E` and for any set `s` of `α`, if `b ≤ a`, the signed variation of `f` on the interval from `a` to `b` intersected with the set `s` is equal to the negative of the real value of the variation of `f` on the set `s` intersected with the interval from `b` to `a`. The variation of a function on a set is defined as the supremum of the sum of the extended distances between the function values at the consecutive elements of all possible finite increasing sequences within the set.
More concisely: For functions from a linearly ordered type to a pseudo-metric space, the variation of a function on an interval intersected with a set is equal to the negative of the variation of the function on the set intersected with the opposite interval.
|
eVariationOn.lowerSemicontinuous
theorem eVariationOn.lowerSemicontinuous :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (s : Set α),
LowerSemicontinuous fun f => eVariationOn f s
The theorem `eVariationOn.lowerSemicontinuous` states that for any set `s` of elements from a type `α` with a linear order, and within the context of a pseudoemetrical space `E`, the mapping of a function `f` from `α` to `E` to its extended real-valued variation on the set `s` is lower semicontinuous. Here, lower semicontinuity is interpreted in terms of pointwise convergence on `s`. More specifically, if we perturb `f` slightly at any point in `s`, the variation of the perturbed function will not decrease too much. The concept of pointwise convergence is encoded as uniform convergence on the family consisting of singletons of elements of `s`.
More concisely: For any set `s` in a type `α` with a linear order and any function `f` from `α` to a pseudometric space `E`, the extended real-valued variation of `f` on `s` is lower semicontinuous with respect to uniform convergence on the family of singletons in `s`.
|
eVariationOn.edist_le
theorem eVariationOn.edist_le :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
{x y : α}, x ∈ s → y ∈ s → edist (f x) (f y) ≤ eVariationOn f s
The theorem `eVariationOn.edist_le` states that for any types `α` and `E` where `α` is a linear order and `E` is a pseudo emetric space, for any function `f` from `α` to `E` and any set `s` of type `α`, the extended distance between `f(x)` and `f(y)` is less than or equal to the extended variation of function `f` on set `s`, given that `x` and `y` are elements of set `s`. In mathematical terms, if $x, y \in s$, then $edist(f(x), f(y)) \leq eVariationOn(f, s)$.
More concisely: For any linear order type `α`, pseudo metric space `E`, function `f` from `α` to `E`, and set `s` of type `α`, the extended distance between `f(x)` and `f(y)` for any `x, y` in `s` is less than or equal to the extended variation of `f` on `s`. In symbols: $\forall x, y \in s, edist(f(x), f(y)) \leq eVariationOn(f, s)$.
|
variationOnFromTo.nonneg_of_le
theorem variationOnFromTo.nonneg_of_le :
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
{a b : α}, a ≤ b → 0 ≤ variationOnFromTo f s a b
This theorem states that for any type `α` that has a linear order and any type `E` that is a pseudo emetric space, for any function `f` from `α` to `E` and any set `s` of `α`, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b`, then the signed variation of `f` on the interval from `a` to `b` that intersects with the set `s`, which is converted to a real number, is always nonnegative. This means that the amount `f` changes (taking into account direction) over the interval `[a, b]` intersecting `s` is at least 0 if `a` is less than or equal to `b`.
More concisely: For any function `f` from a linearly ordered type `α` to a pseudo metric space `E`, and any set `s` of `α`, the signed variation of `f` on the interval of `α` intersecting `s` is nonnegative for any pair of elements `a` and `b` with `a` less than or equal to `b`.
|