Theorems · Theorem · real analysis

BoundedVariationOn.tendsto_eVariationOn_Icc_left

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {l : E},
  BoundedVariationOn f s →
    ∀ {x : α},
      Filter.Tendsto f (nhdsWithin x (s ∩ Set.Iio x)) (nhds l) →
        x ∈ s →
          Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc y x)) (nhdsWithin x (s ∩ Set.Iio x))
            (nhds (edist (f x) l))

If a function has bounded variation, then the variation on small closed intervals to the left of this point tends to the contribution of the point, i.e., the distance between the left limit and the value at the point

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

2 results in Mathlib

Foundations

Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderPseudoEMetricSpaceTopologicalSpaceOrderTopology