Signed variation

We define variationOnFromTo f s a b : ℝ as the signed variation of f between a and b, i.e., its variation if a ≤ b, and its opposite otherwise. We establish basic properties of this notion, and use it to show that a bounded variation real function is the difference of two monotone functions.

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

• 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

theorem variationOnFromTo.self {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) (a : α) : variationOnFromTo f s a a = 0

theorem variationOnFromTo.nonneg_of_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : a ≤ b) : 0 ≤ variationOnFromTo f s a b

theorem variationOnFromTo.eq_neg_swap {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) (a b : α) : variationOnFromTo f s a b = -variationOnFromTo f s b a

theorem variationOnFromTo.nonpos_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 ≤ 0

theorem variationOnFromTo.abs_le_eVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) {a b : α} : |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

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) : variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c

theorem variationOnFromTo.sub_right {α : 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) : variationOnFromTo f s a b - variationOnFromTo f s a c = variationOnFromTo f s c b

theorem variationOnFromTo.sub_left {α : 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) : variationOnFromTo f s a b - variationOnFromTo f s c b = variationOnFromTo f s a c

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) : variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0

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 b → edist (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 a → edist (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 b → edist (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) : MonotoneOn (variationOnFromTo f s 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.abs_sub_le_sub_of_le {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (as : a ∈ s) (bs : b ∈ s) (cs : c ∈ s) (bc : b ≤ c) : |f c - f b| ≤ variationOnFromTo f s a c - variationOnFromTo f s a b

theorem variationOnFromTo.add_self_monotoneOn {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) : MonotoneOn (variationOnFromTo f s a + f) s

theorem variationOnFromTo.sub_self_monotoneOn {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) : MonotoneOn (variationOnFromTo f s a - f) 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 variationOnFromTo.tendsto_left {α : Type u_1} [LinearOrder α] {s : Set α} {E : Type u_3} [PseudoMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {l : E} {a b : α} (ha : a ∈ s) (hb : b ∈ s) (hf : LocallyBoundedVariationOn f s) (h'f : Filter.Tendsto f (nhdsWithin b (s ∩ Set.Iio b)) (nhds l)) : Filter.Tendsto (variationOnFromTo f s a) (nhdsWithin b (s ∩ Set.Iio b)) (nhds (variationOnFromTo f s a b - dist (f b) l))

The jump of variationOnFromTo on the left of a point is given by the distance between the left limit and the value of the function.

theorem variationOnFromTo.tendsto_right {α : Type u_1} [LinearOrder α] {s : Set α} {E : Type u_3} [PseudoMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {l : E} {a b : α} (ha : a ∈ s) (hb : b ∈ s) (hf : LocallyBoundedVariationOn f s) (h'f : Filter.Tendsto f (nhdsWithin b (s ∩ Set.Ioi b)) (nhds l)) : Filter.Tendsto (variationOnFromTo f s a) (nhdsWithin b (s ∩ Set.Ioi b)) (nhds (variationOnFromTo f s a b + dist (f b) l))

The jump of variationOnFromTo on the right of a point is given by the distance between the right limit and the value of the function.

theorem variationOnFromTo.leftLim_eq {α : Type u_1} [LinearOrder α] {E : Type u_3} [PseudoMetricSpace E] [CompleteSpace E] {f : α → E} {a b : α} (hf : BoundedVariationOn f Set.univ) : Function.leftLim (variationOnFromTo f Set.univ a) b = variationOnFromTo f Set.univ a b - dist (f b) (Function.leftLim f b)

The jump of variationOnFromTo on the left of a point is given by the distance between the left limit and the value of the function.

theorem variationOnFromTo.rightLim_eq {α : Type u_1} [LinearOrder α] {E : Type u_3} [PseudoMetricSpace E] [CompleteSpace E] {f : α → E} {a b : α} (hf : BoundedVariationOn f Set.univ) : Function.rightLim (variationOnFromTo f Set.univ a) b = variationOnFromTo f Set.univ a b + dist (f b) (Function.rightLim f b)

The jump of variationOnFromTo on the right of a point is given by the distance between the right limit and the value of the function.

theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} [TopologicalSpace α] [OrderTopology α] (hf : BoundedVariationOn f Set.univ) {a x : α} (hx : ContinuousWithinAt f (Set.Ici x) x) : ContinuousWithinAt (variationOnFromTo f Set.univ a) (Set.Ici x) x

theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} [TopologicalSpace α] [OrderTopology α] [T3Space E] [CompleteSpace E] (hf : BoundedVariationOn f Set.univ) {a x : α} : ContinuousWithinAt (variationOnFromTo (Function.rightLim f) Set.univ a) (Set.Ici x) x

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 ∧ ∀ x ∈ s, ∀ y ∈ s, p y - p x + (q y - q x) = variationOnFromTo f s x y

If a real-valued function has bounded variation on a set, then it is a difference of monotone functions there. Moreover, one can make sure that the two monotone functions add up to the variation of f.

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.