Theorems · Theorem · real analysis

BoundedVariationOn.tendsto_eVariationOn_Icc_right

∀ {α : 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.Ioi x)) (nhds l) →
        x ∈ s →
          Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc x y)) (nhdsWithin x (s ∩ Set.Ioi x))
            (nhds (edist (f x) l))

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

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpaceTopologicalSpaceOrderTopology