The variation process

Main definitions

• variationProcess: the pathwise variation of X from a starting time a, as a process.

Main results

• measurable_eVariationOn_of_countable: the variation of a family of functions over a countable set of points is measurable in the parameter.
• measurable_eVariationOn_of_continuousWithinAt, ..._of_continuousWithinAt_Ioi and ..._of_continuousWithinAt_Iio: the variation of a family of functions over a set s is measurable in the parameter, assuming continuous, right-continuous and left-continuous functions respectively. The first result assumes separability of the domain, the other two require it to be second countable.
• variationProcess_nonneg: for a ≤ t the variation process is nonnegative.
• monotone_variationProcess: the variation process of a path of locally bounded variation is monotone in time.
• MeasureTheory.StronglyAdapted.measurable_variationProcess_of_continuous, ..._of_continuousWithinAt_Ioi and ..._of_continuousWithinAt_Iio: for a ≤ t, the value at time t of the variation process of a strongly adapted process is 𝓕 t-measurable, assuming continuous, right-continuous and left-continuous paths respectively.

theorem measurable_eVariationOn_of_countable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] {s : Set ι} (hs : s.Countable) {X : ι → Ω → E} (hX : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (X i)) : Measurable fun (ω : Ω) => eVariationOn (fun (x : ι) => X x ω) s

The variation of a family of functions over a countable set of points is measurable in the parameter.

noncomputable def variationProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] (X : ι → Ω → E) (a : ι) : ι → Ω → ℝ

The variation process of X from the starting time a.

Equations

• variationProcess X a t ω = variationOnFromTo (fun (x : ι) => X x ω) Set.univ a t

theorem variationProcess_eq_toReal_eVariationOn_Icc {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] (X : ι → Ω → E) {a t : ι} (hat : a ≤ t) (ω : Ω) : variationProcess X a t ω = (eVariationOn (fun (x : ι) => X x ω) (Set.Icc a t)).toReal

For a ≤ t, the variation process at time t is the total variation of the path on Icc a t, converted to a real number.

theorem variationProcess_nonneg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] (X : ι → Ω → E) {a t : ι} (hat : a ≤ t) (ω : Ω) : 0 ≤ variationProcess X a t ω

For a ≤ t the variation process is nonnegative. It can be negative for t < a, where it takes the signed value -(eVariationOn (X · ω) (Icc t a)).toReal.

theorem monotone_variationProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [PseudoEMetricSpace E] {X : ι → Ω → E} {ω : Ω} (hX : LocallyBoundedVariationOn (fun (x : ι) => X x ω) Set.univ) (a : ι) : Monotone fun (t : ι) => variationProcess X a t ω

The variation process of a path of locally bounded variation is monotone in time. Monotonicity holds on all of ι, not just above the starting time a, since the variation is signed.

theorem measurable_eVariationOn_of_continuousWithinAt {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [TopologicalSpace.SeparableSpace ι] {s : Set ι} {X : ι → Ω → E} (hX : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (X i)) (hcont : ∀ (ω : Ω), ContinuousOn (fun (x : ι) => X x ω) s) : Measurable fun (ω : Ω) => eVariationOn (fun (x : ι) => X x ω) s

The variation of a family of functions that are continuous within s at every point of s, over the points of a set s, is measurable in the parameter.

theorem MeasureTheory.StronglyAdapted.measurable_variationProcess_of_continuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [TopologicalSpace.SeparableSpace ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : StronglyAdapted 𝓕 X) {a t : ι} (hcont : ∀ (ω : Ω), ContinuousOn (fun (x : ι) => X x ω) (Set.Ici a)) (hat : a ≤ t) : Measurable (variationProcess X a t)

For a ≤ t, the value at time t of the variation process of a strongly adapted process with continuous paths is 𝓕 t-measurable.

theorem MeasureTheory.StronglyAdapted.adapted_variationProcess_of_continuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [TopologicalSpace.SeparableSpace ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : StronglyAdapted 𝓕 X) (hcont : ∀ (ω : Ω), Continuous fun (x : ι) => X x ω) : Adapted 𝓕 (variationProcess X ⊥)

If the index set has a bottom element, then the variation process of a strongly adapted process with continuous paths is adapted.

theorem measurable_eVariationOn_of_continuousWithinAt_Ioi {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {s : Set ι} {X : ι → Ω → E} (hX : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (X i)) (hcont : ∀ (ω : Ω), ∀ i ∈ s, ContinuousWithinAt (fun (x : ι) => X x ω) (s ∩ Set.Ioi i) i) : Measurable fun (ω : Ω) => eVariationOn (fun (x : ι) => X x ω) s

The variation of a family of right-continuous functions over the points of a set s is measurable in the parameter.

theorem measurable_eVariationOn_of_continuousWithinAt_Iio {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {s : Set ι} {X : ι → Ω → E} (hX : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (X i)) (hcont : ∀ (ω : Ω), ∀ i ∈ s, ContinuousWithinAt (fun (x : ι) => X x ω) (s ∩ Set.Iio i) i) : Measurable fun (ω : Ω) => eVariationOn (fun (x : ι) => X x ω) s

The variation of a family of left-continuous functions over the points of a set s is measurable in the parameter.

theorem MeasureTheory.StronglyAdapted.measurable_variationProcess_of_continuousWithinAt_Ioi {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : StronglyAdapted 𝓕 X) (hcont : ∀ (ω : Ω) (i : ι), ContinuousWithinAt (fun (x : ι) => X x ω) (Set.Ioi i) i) {a t : ι} (hat : a ≤ t) : Measurable (variationProcess X a t)

For a ≤ t, the value at time t of the variation process of a strongly adapted process with right-continuous paths is 𝓕 t-measurable.

theorem MeasureTheory.StronglyAdapted.adapted_variationProcess_of_continuousWithinAt_Ioi {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : StronglyAdapted 𝓕 X) (hcont : ∀ (ω : Ω) (i : ι), ContinuousWithinAt (fun (x : ι) => X x ω) (Set.Ioi i) i) : Adapted 𝓕 (variationProcess X ⊥)

If the index set has a bottom element, then the variation process of a strongly adapted process with right-continuous paths is adapted.

theorem MeasureTheory.StronglyAdapted.measurable_variationProcess_of_continuousWithinAt_Iio {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : StronglyAdapted 𝓕 X) (hcont : ∀ (ω : Ω) (i : ι), ContinuousWithinAt (fun (x : ι) => X x ω) (Set.Iio i) i) {a t : ι} (hat : a ≤ t) : Measurable (variationProcess X a t)

For a ≤ t, the value at time t of the variation process of a strongly adapted process with left-continuous paths is 𝓕 t-measurable.

theorem MeasureTheory.StronglyAdapted.adapted_variationProcess_of_continuousWithinAt_Iio {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [PseudoEMetricSpace E] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : StronglyAdapted 𝓕 X) (hcont : ∀ (ω : Ω) (i : ι), ContinuousWithinAt (fun (x : ι) => X x ω) (Set.Iio i) i) : Adapted 𝓕 (variationProcess X ⊥)

If the index set has a bottom element, then the variation process of a strongly adapted process with right-continuous paths is adapted.