Functions of bounded variation #
We study functions of bounded variation. In particular, we show that a bounded variation function is a difference of monotone functions, and differentiable almost everywhere. This implies that Lipschitz functions from the real line into finite-dimensional vector space are also differentiable almost everywhere.
Main definitions and results #
eVariationOn f s
is the total variation of the functionf
on the sets
, inℝ≥0∞
.BoundedVariationOn f s
registers that the variation off
ons
is finite.LocallyBoundedVariationOn f s
registers thatf
has finite variation on any compact subinterval ofs
.variationOnFromTo f s a b
is the signed variation off
ons ∩ Icc a b
, converted toℝ
.eVariationOn.Icc_add_Icc
states that the variation off
on[a, c]
is the sum of its variations on[a, b]
and[b, c]
.LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn
proves that a function with locally bounded variation is the difference of two monotone functions.LipschitzWith.locallyBoundedVariationOn
shows that a Lipschitz function has locally bounded variation.
We also give several variations around these results.
Implementation #
We define the variation as an extended nonnegative real, to allow for infinite variation. This makes
it possible to use the complete linear order structure of ℝ≥0∞
. The proofs would be much
more tedious with an ℝ
-valued or ℝ≥0
-valued variation, since one would always need to check
that the sets one uses are nonempty and bounded above as these are only conditionally complete.
The (extended-real-valued) variation of a function f
on a set s
inside a linear order is
the supremum of the sum of edist (f (u (i+1))) (f (u i))
over all finite increasing
sequences u
in s
.
Equations
Instances For
A function has bounded variation on a set s
if its total variation there is finite.
Equations
- BoundedVariationOn f s = (eVariationOn f s ≠ ⊤)
Instances For
A function has locally bounded variation on a set s
if, given any interval [a, b]
with
endpoints in s
, then the function has finite variation on s ∩ [a, b]
.
Equations
- LocallyBoundedVariationOn f s = ∀ (a b : α), a ∈ s → b ∈ s → BoundedVariationOn f (s ∩ Set.Icc a b)
Instances For
Basic computations of variation #
The map (eVariationOn · s)
is lower semicontinuous for pointwise convergence on s
.
Pointwise convergence on s
is encoded here as uniform convergence on the family consisting of the
singletons of elements of s
.
The map (eVariationOn · s)
is lower semicontinuous for uniform convergence on s
.
Consider a monotone function u
parameterizing some points of a set s
. Given x ∈ s
, then
one can find another monotone function v
parameterizing the same points as u
, with x
added.
In particular, the variation of a function along u
is bounded by its variation along v
.
The variation of a function on the union of two sets s
and t
, with s
to the left of t
,
bounds the sum of the variations along s
and t
.
If a set s
is to the left of a set t
, and both contain the boundary point x
, then
the variation of f
along s ∪ t
is the sum of the variations.
Monotone functions and bounded variation #
The signed variation of f
on the interval Icc a b
intersected with the set s
,
squashed to a real (therefore only really meaningful if the variation is finite)
Equations
- variationOnFromTo f s a b = if a ≤ b then (eVariationOn f (s ∩ Set.Icc a b)).toReal else -(eVariationOn f (s ∩ Set.Icc b a)).toReal
Instances For
If a real-valued function has bounded variation on a set, then it is a difference of monotone functions there.