Theorems · Theorem · real analysis

LocallyBoundedVariationOn.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},
  LocallyBoundedVariationOn 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 locally 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 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderPseudoEMetricSpaceTopologicalSpaceOrderTopology