Documentation

Mathlib.Analysis.BoundedVariation

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 #

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.

noncomputable def eVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) :

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
    def BoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) :

    A function has bounded variation on a set s if its total variation there is finite.

    Equations
    Instances For
      def LocallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) :

      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
      Instances For

        Basic computations of variation #

        theorem eVariationOn.nonempty_monotone_mem {α : Type u_1} [LinearOrder α] {s : Set α} (hs : s.Nonempty) :
        Nonempty { u : α // Monotone u ∀ (i : ), u i s }
        theorem eVariationOn.eq_of_edist_zero_on {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {f' : αE} {s : Set α} (h : ∀ ⦃x : α⦄, x sedist (f x) (f' x) = 0) :
        theorem eVariationOn.eq_of_eqOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {f' : αE} {s : Set α} (h : Set.EqOn f f' s) :
        theorem eVariationOn.sum_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} (n : ) {u : α} (hu : Monotone u) (us : ∀ (i : ), u i s) :
        ((Finset.range n).sum fun (i : ) => edist (f (u (i + 1))) (f (u i))) eVariationOn f s
        theorem eVariationOn.sum_le_of_monotoneOn_Icc {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {m : } {n : } {u : α} (hu : MonotoneOn u (Set.Icc m n)) (us : iSet.Icc m n, u i s) :
        ((Finset.Ico m n).sum fun (i : ) => edist (f (u (i + 1))) (f (u i))) eVariationOn f s
        theorem eVariationOn.sum_le_of_monotoneOn_Iic {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {n : } {u : α} (hu : MonotoneOn u (Set.Iic n)) (us : in, u i s) :
        ((Finset.range n).sum fun (i : ) => edist (f (u (i + 1))) (f (u i))) eVariationOn f s
        theorem eVariationOn.mono {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {t : Set α} (hst : t s) :
        theorem BoundedVariationOn.mono {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (h : BoundedVariationOn f s) {t : Set α} (ht : t s) :
        theorem eVariationOn.edist_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {x : α} {y : α} (hx : x s) (hy : y s) :
        edist (f x) (f y) eVariationOn f s
        theorem eVariationOn.eq_zero_iff {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} :
        eVariationOn f s = 0 xs, ys, edist (f x) (f y) = 0
        theorem eVariationOn.constant_on {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : (f '' s).Subsingleton) :
        @[simp]
        theorem eVariationOn.subsingleton {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} (hs : s.Subsingleton) :
        theorem eVariationOn.lowerSemicontinuous_aux {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {ι : Type u_3} {F : ιαE} {p : Filter ι} {f : αE} {s : Set α} (Ffs : xs, Filter.Tendsto (fun (i : ι) => F i x) p (nhds (f x))) {v : ENNReal} (hv : v < eVariationOn f s) :
        ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
        theorem eVariationOn.lowerSemicontinuous {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (s : Set α) :
        LowerSemicontinuous fun (f : UniformOnFun α E (singleton '' s)) => eVariationOn f s

        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.

        theorem BoundedVariationOn.dist_le {α : Type u_1} [LinearOrder α] {E : Type u_3} [PseudoMetricSpace E] {f : αE} {s : Set α} (h : BoundedVariationOn f s) {x : α} {y : α} (hx : x s) (hy : y s) :
        dist (f x) (f y) (eVariationOn f s).toReal
        theorem BoundedVariationOn.sub_le {α : Type u_1} [LinearOrder α] {f : α} {s : Set α} (h : BoundedVariationOn f s) {x : α} {y : α} (hx : x s) (hy : y s) :
        f x - f y (eVariationOn f s).toReal
        theorem eVariationOn.add_point {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {x : α} (hx : x s) (u : α) (hu : Monotone u) (us : ∀ (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))

        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.

        theorem eVariationOn.add_le_union {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {t : Set α} (h : xs, yt, x y) :

        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.

        theorem eVariationOn.union {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {t : Set α} {x : α} (hs : IsGreatest s x) (ht : IsLeast t x) :

        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.

        theorem eVariationOn.Icc_add_Icc {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) {s : Set α} {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) (hb : b s) :
        theorem eVariationOn.comp_le_of_monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : αE) {s : Set α} {t : Set β} (φ : βα) (hφ : MonotoneOn φ t) (φst : Set.MapsTo φ t s) :
        theorem eVariationOn.comp_le_of_antitoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : αE) {s : Set α} {t : Set β} (φ : βα) (hφ : AntitoneOn φ t) (φst : Set.MapsTo φ t s) :
        theorem eVariationOn.comp_eq_of_monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : αE) {t : Set β} (φ : βα) (hφ : MonotoneOn φ t) :
        eVariationOn (f φ) t = eVariationOn f (φ '' t)
        theorem eVariationOn.comp_inter_Icc_eq_of_monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : αE) {t : Set β} (φ : βα) (hφ : MonotoneOn φ t) {x : β} {y : β} (hx : x t) (hy : y t) :
        eVariationOn (f φ) (t Set.Icc x y) = eVariationOn f (φ '' t Set.Icc (φ x) (φ y))
        theorem eVariationOn.comp_eq_of_antitoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : αE) {t : Set β} (φ : βα) (hφ : AntitoneOn φ t) :
        eVariationOn (f φ) t = eVariationOn f (φ '' t)
        theorem eVariationOn.comp_ofDual {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) :
        eVariationOn (f OrderDual.ofDual) (OrderDual.ofDual ⁻¹' s) = eVariationOn f s

        Monotone functions and bounded variation #

        theorem MonotoneOn.eVariationOn_le {α : Type u_1} [LinearOrder α] {f : α} {s : Set α} (hf : MonotoneOn f s) {a : α} {b : α} (as : a s) (bs : b s) :
        theorem MonotoneOn.locallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {f : α} {s : Set α} (hf : MonotoneOn f s) :
        noncomputable def variationOnFromTo {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) (a : α) (b : α) :

        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
        Instances For
          theorem variationOnFromTo.self {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) (a : α) :
          theorem variationOnFromTo.nonneg_of_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) {a : α} {b : α} (h : a b) :
          theorem variationOnFromTo.eq_neg_swap {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) (a : α) (b : α) :
          theorem variationOnFromTo.nonpos_of_ge {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) {a : α} {b : α} (h : b a) :
          theorem variationOnFromTo.eq_of_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) {a : α} {b : α} (h : a b) :
          variationOnFromTo f s a b = (eVariationOn f (s Set.Icc a b)).toReal
          theorem variationOnFromTo.eq_of_ge {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : αE) (s : Set α) {a : α} {b : α} (h : b a) :
          variationOnFromTo f s a b = -(eVariationOn f (s Set.Icc b a)).toReal
          theorem variationOnFromTo.add {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} {b : α} {c : α} (ha : a s) (hb : b s) (hc : c s) :
          theorem variationOnFromTo.edist_zero_of_eq_zero {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} {b : α} (ha : a s) (hb : b s) (h : variationOnFromTo f s a b = 0) :
          edist (f a) (f b) = 0
          theorem variationOnFromTo.eq_left_iff {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} {b : α} {c : α} (ha : a s) (hb : b s) (hc : c s) :
          theorem variationOnFromTo.eq_zero_iff_of_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} {b : α} (ha : a s) (hb : b s) (ab : a b) :
          variationOnFromTo f s a b = 0 ∀ ⦃x : α⦄, x s Set.Icc a b∀ ⦃y : α⦄, y s Set.Icc a bedist (f x) (f y) = 0
          theorem variationOnFromTo.eq_zero_iff_of_ge {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} {b : α} (ha : a s) (hb : b s) (ba : b a) :
          variationOnFromTo f s a b = 0 ∀ ⦃x : α⦄, x s Set.Icc b a∀ ⦃y : α⦄, y s Set.Icc b aedist (f x) (f y) = 0
          theorem variationOnFromTo.eq_zero_iff {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} {b : α} (ha : a s) (hb : b s) :
          variationOnFromTo f s a b = 0 ∀ ⦃x : α⦄, x s Set.uIcc a b∀ ⦃y : α⦄, y s Set.uIcc a bedist (f x) (f y) = 0
          theorem variationOnFromTo.monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a s) :
          theorem variationOnFromTo.antitoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : αE} {s : Set α} (hf : LocallyBoundedVariationOn f s) {b : α} (bs : b s) :
          AntitoneOn (fun (a : α) => variationOnFromTo f s a b) s
          theorem variationOnFromTo.sub_self_monotoneOn {α : Type u_1} [LinearOrder α] {f : α} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a s) :
          theorem variationOnFromTo.comp_eq_of_monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : αE) {t : Set β} (φ : βα) (hφ : MonotoneOn φ t) {x : β} {y : β} (hx : x t) (hy : y t) :
          variationOnFromTo (f φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
          theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn {α : Type u_1} [LinearOrder α] {f : α} {s : Set α} (h : LocallyBoundedVariationOn f s) :
          ∃ (p : α) (q : α), MonotoneOn p s MonotoneOn q s f = p - q

          If a real valued function has bounded variation on a set, then it is a difference of monotone functions there.

          Lipschitz functions and bounded variation #

          theorem LipschitzOnWith.comp_eVariationOn_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : EF} {C : NNReal} {t : Set E} (h : LipschitzOnWith C f t) {g : αE} {s : Set α} (hg : Set.MapsTo g s t) :
          eVariationOn (f g) s C * eVariationOn g s
          theorem LipschitzOnWith.comp_boundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : EF} {C : NNReal} {t : Set E} (hf : LipschitzOnWith C f t) {g : αE} {s : Set α} (hg : Set.MapsTo g s t) (h : BoundedVariationOn g s) :
          theorem LipschitzOnWith.comp_locallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : EF} {C : NNReal} {t : Set E} (hf : LipschitzOnWith C f t) {g : αE} {s : Set α} (hg : Set.MapsTo g s t) (h : LocallyBoundedVariationOn g s) :
          theorem LipschitzWith.comp_boundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : EF} {C : NNReal} (hf : LipschitzWith C f) {g : αE} {s : Set α} (h : BoundedVariationOn g s) :
          theorem LipschitzWith.comp_locallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : EF} {C : NNReal} (hf : LipschitzWith C f) {g : αE} {s : Set α} (h : LocallyBoundedVariationOn g s) :

          Almost everywhere differentiability of functions with locally bounded variation #

          A bounded variation function into is differentiable almost everywhere. Superseded by ae_differentiableWithinAt_of_mem.

          theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi {ι : Type u_4} [Fintype ι] {f : ι} {s : Set } (h : LocallyBoundedVariationOn f s) :
          ∀ᵐ (x : ), x sDifferentiableWithinAt f s x

          A bounded variation function into a finite dimensional product vector space is differentiable almost everywhere. Superseded by ae_differentiableWithinAt_of_mem.

          A real function into a finite dimensional real vector space with bounded variation on a set is differentiable almost everywhere in this set.

          theorem LocallyBoundedVariationOn.ae_differentiableWithinAt {V : Type u_3} [NormedAddCommGroup V] [NormedSpace V] [FiniteDimensional V] {f : V} {s : Set } (h : LocallyBoundedVariationOn f s) (hs : MeasurableSet s) :
          ∀ᵐ (x : ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt f s x

          A real function into a finite dimensional real vector space with bounded variation on a set is differentiable almost everywhere in this set.

          A real function into a finite dimensional real vector space with bounded variation is differentiable almost everywhere.

          A real function into a finite dimensional real vector space which is Lipschitz on a set is differentiable almost everywhere in this set. For the general Rademacher theorem assuming that the source space is finite dimensional, see LipschitzOnWith.ae_differentiableWithinAt_of_mem.

          theorem LipschitzOnWith.ae_differentiableWithinAt_real {V : Type u_3} [NormedAddCommGroup V] [NormedSpace V] [FiniteDimensional V] {C : NNReal} {f : V} {s : Set } (h : LipschitzOnWith C f s) (hs : MeasurableSet s) :
          ∀ᵐ (x : ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt f s x

          A real function into a finite dimensional real vector space which is Lipschitz on a set is differentiable almost everywhere in this set. For the general Rademacher theorem assuming that the source space is finite dimensional, see LipschitzOnWith.ae_differentiableWithinAt.

          A real Lipschitz function into a finite dimensional real vector space is differentiable almost everywhere. For the general Rademacher theorem assuming that the source space is finite dimensional, see LipschitzWith.ae_differentiableAt.