Variation of a function over a countable or dense set of points

The variation of a function over a set is an uncountable supremum, so it is not measurable in a parameter for free. This file provides tools to compute it over a countable set of points instead. Measurability of the variation of a family of functions is deduced from these tools in the file BrownianMotion.StochasticIntegral.VariationProcess.

Main results

• eVariationOn_eq_iSup_fin: the variation over s as a supremum over monotone tuples with values in s.

Which dense sets suffice to compute the variation depends on the regularity of the function, and this file provides two independent sets of assumptions:

1. the first assumes continuity of the function together with separability of the domain — eVariationOn_eq_comp_val_of_dense;
2. the second assumes only right-continuity of the function, but requires the domain to be second countable — eVariationOn_eq_comp_val_of_dense_Ioi, together with the left-continuous counterpart eVariationOn_eq_comp_val_of_dense_Iio.

theorem eVariationOn_eq_iSup_fin {ι : Type u_1} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] {s : Set ι} (X : ι → E) : eVariationOn X s = ⨆ (n : ℕ), ⨆ (p : { u : Fin (n + 1) → ι // Monotone u ∧ ∀ (i : Fin (n + 1)), u i ∈ s }), ∑ i : Fin n, edist (X (↑p i.succ)) (X (↑p i.castSucc))

The variation over s, reindexed as a supremum over monotone tuples Fin (n + 1) → ι with values in s.

theorem eVariationOn_eq_comp_val_of_dense {ι : Type u_1} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] {s : Set ι} {t : Set ↑s} (ht : Dense t) {f : ι → E} (hf : ContinuousOn f s) : eVariationOn f s = eVariationOn f (Subtype.val '' t)

The variation of a function that is continuous within s at every point of s can be computed using only points of a dense subset t of s.

theorem nhdsGT_subtype_eq_bot_iff {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] {s : Set ι} {x : ι} (hx : x ∈ s) : nhdsWithin ⟨x, hx⟩ (Set.Ioi ⟨x, hx⟩) = ⊥ ↔ nhdsWithin x (s ∩ Set.Ioi x) = ⊥

A point of a subset s is isolated on the right in the subspace ↥s exactly when it is isolated on the right within s.

theorem eVariationOn_eq_comp_val_of_dense_Ioi {ι : Type u_1} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] {s : Set ι} {t : Set ↑s} (ht : Dense t) (hts : {x : ↑s | nhdsWithin x (Set.Ioi x) = ⊥} ⊆ t) {f : ι → E} (hf : ∀ x ∈ s, ContinuousWithinAt f (s ∩ Set.Ioi x) x) : eVariationOn f s = eVariationOn f (Subtype.val '' t)

The variation of a function that is right-continuous within s at every point of s can be computed using only points of a dense subset t of s, provided t contains every point of s that is isolated on the right.

theorem eVariationOn_eq_comp_val_of_dense_Iio {ι : Type u_1} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] {s : Set ι} {t : Set ↑s} (ht : Dense t) (hts : {x : ↑s | nhdsWithin x (Set.Iio x) = ⊥} ⊆ t) {f : ι → E} (hf : ∀ x ∈ s, ContinuousWithinAt f (s ∩ Set.Iio x) x) : eVariationOn f s = eVariationOn f (Subtype.val '' t)

The variation of a function that is left-continuous within s at every point of s can be computed using only points of a dense subset t of s, provided t contains every point of s that is isolated on the left.