Nonnegative-rational time shifts

This file translates a dense-time process by a nonnegative rational time. Translation is an isometry of NNRat, so the Kolmogorov increment condition is preserved with exactly the same exponents and constant. The final definitions and identities identify the unit-interval dyadic samples and canonical limit for the shifted process with samples of the original process on the interval starting at the shift.

No global path is glued here, and no measurability of the canonical limit or modification-law assertion is made.

def MarkovProcess.timeShift {Ω : Type u_1} {E : Type u_2} (k : ℚ≥0) (X : ℚ≥0 → Ω → E) : ℚ≥0 → Ω → E

Translate a dense-time process by a nonnegative rational time.

Equations

• MarkovProcess.timeShift k X q ω = X (k + q) ω

@[simp]

theorem MarkovProcess.timeShift_apply {Ω : Type u_1} {E : Type u_2} (k q : ℚ≥0) (X : ℚ≥0 → Ω → E) (ω : Ω) : timeShift k X q ω = X (k + q) ω

theorem MarkovProcess.IsKolmogorovProcess.timeShift {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : ℚ≥0 → Ω → E} {p q : ℝ} {M : NNReal} (hX : ProbabilityTheory.IsKolmogorovProcess X P p q M) (k : ℚ≥0) : ProbabilityTheory.IsKolmogorovProcess (MarkovProcess.timeShift k X) P p q M

Nonnegative-rational translation preserves the Kolmogorov condition without changing its exponents or constant.

noncomputable def MarkovProcess.shiftedUnitDyadicFloorValue (k : ℚ≥0) (n : ℕ) (t : ↑(Set.Icc 0 1)) : ℚ≥0

The level-n dyadic time in the unit interval, translated to the interval beginning at k.

Equations

• MarkovProcess.shiftedUnitDyadicFloorValue k n t = k + MarkovProcess.unitDyadicFloorValue n t

theorem MarkovProcess.timeShift_unitDyadicFloorValue_apply {Ω : Type u_1} {E : Type u_2} (k : ℚ≥0) (X : ℚ≥0 → Ω → E) (ω : Ω) (n : ℕ) (t : ↑(Set.Icc 0 1)) : timeShift k X (unitDyadicFloorValue n t) ω = X (shiftedUnitDyadicFloorValue k n t) ω

noncomputable def MarkovProcess.shiftedUnitDyadicFloorLimit {Ω : Type u_1} {E : Type u_2} [PseudoMetricSpace E] (k : ℚ≥0) (X : ℚ≥0 → Ω → E) (ω : Ω) : ↑(Set.Icc 0 1) → E

The canonical unit-interval dyadic-floor limit of the process translated by k. Its time parameter represents the original interval [k, k + 1].

Equations

• MarkovProcess.shiftedUnitDyadicFloorLimit k X ω = MarkovProcess.unitDyadicFloorLimit (MarkovProcess.timeShift k X) ω

@[simp]

theorem MarkovProcess.shiftedUnitDyadicFloorLimit_apply {Ω : Type u_1} {E : Type u_2} [PseudoMetricSpace E] (k : ℚ≥0) (X : ℚ≥0 → Ω → E) (ω : Ω) (t : ↑(Set.Icc 0 1)) : shiftedUnitDyadicFloorLimit k X ω t = unitDyadicFloorLimit (timeShift k X) ω t

theorem MarkovProcess.tendsto_shiftedUnitDyadicFloorLimit_of_cauchySeq {Ω : Type u_1} {E : Type u_2} [PseudoMetricSpace E] [CompleteSpace E] {k : ℚ≥0} {X : ℚ≥0 → Ω → E} {ω : Ω} {t : ↑(Set.Icc 0 1)} (h : CauchySeq fun (n : ℕ) => X (shiftedUnitDyadicFloorValue k n t) ω) : Filter.Tendsto (fun (n : ℕ) => X (shiftedUnitDyadicFloorValue k n t) ω) Filter.atTop (nhds (shiftedUnitDyadicFloorLimit k X ω t))

Cauchy control of samples of the original process at translated dyadic times gives convergence to the translated canonical unit-interval limit.