Equivariance of the continuous-path process

Let P be a conservative Feller sub-Markov kernel semigroup on alpha with a Kolmogorov-regular continuous-path process, let e : alpha ≃ₜ beta be a homeomorphism onto a second state space and c > 0 a time factor, and let P' be the rescaled conjugate of P on beta, that is P' t x = ((P (c * t)) (e.symm x)).map e. Then the continuous-path process of P' is the continuous-path process of P started at e.symm x and pushed forward by the path map omega ↦ fun t ↦ e (omega (c * t)).

The proof goes through the uniqueness theorem of MarkovProcess/Main.lean: the pushed-forward kernel is a Markov kernel whose finite-dimensional distributions are computed from the Feller marginal theorem for P at the rescaled times together with the finite-dimensional transfer SubMarkovKernelSemigroup.IsRescaledConjugate.finiteSetKernel_eq.

Main results: ContinuousPath.rescale and its continuity and measurability; SubMarkovKernelSemigroup.IsFellerKernelSemigroup.continuousProcess_map_finiteEvaluation_ordered, the marginal of the continuous-path process at an arbitrary strictly increasing finite family of times; SubMarkovKernelSemigroup.IsConservative.continuousProcess_eq_map_rescale and its pointwise form continuousProcess_apply_rescale; the intrinsic form continuousProcess_eq_map_rescale_of_hasKolmogorovMoments, whose only regularity hypothesis is a Kolmogorov moment bound on P when e is an isometry; and the two degenerate corollaries, pure time rescaling (continuousProcess_eq_map_timeRescale) and pure conjugation (continuousProcess_eq_map_conjugate).

No scaling limit is asserted: c is a fixed positive factor and both semigroups are given in advance. The two state spaces may coincide; the degenerate corollaries are stated on one space.

def MarkovProcess.ContinuousPath.timeScaling (c : NNReal) : C(NNReal, NNReal)

Multiplication of nonnegative time by a fixed factor, as a continuous self-map of NNReal.

Equations

• MarkovProcess.ContinuousPath.timeScaling c = { toFun := fun (t : NNReal) => c * t, continuous_toFun := ⋯ }

@[simp]

theorem MarkovProcess.ContinuousPath.timeScaling_apply (c t : NNReal) : (timeScaling c) t = c * t

Time scaling, evaluated.

def MarkovProcess.ContinuousPath.rescale {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (e : alpha ≃ₜ beta) (c : NNReal) (omega : ContinuousPath alpha) : ContinuousPath beta

Speed a continuous path up by the factor c and conjugate its state by the homeomorphism e.

Equations

• MarkovProcess.ContinuousPath.rescale e c omega = (↑e).comp (ContinuousMap.comp omega (MarkovProcess.ContinuousPath.timeScaling c))

@[simp]

theorem MarkovProcess.ContinuousPath.rescale_apply {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (e : alpha ≃ₜ beta) (c : NNReal) (omega : ContinuousPath alpha) (t : NNReal) : (rescale e c omega) t = e (omega (c * t))

The rescaled path, evaluated: e applied to the path at the sped-up time.

@[simp]

theorem MarkovProcess.ContinuousPath.rescale_refl_one {alpha : Type u_1} [TopologicalSpace alpha] (omega : ContinuousPath alpha) : rescale (Homeomorph.refl alpha) 1 omega = omega

Rescaling by the identity homeomorphism and the factor one is the identity.

theorem MarkovProcess.ContinuousPath.rescale_refl_apply {alpha : Type u_1} [TopologicalSpace alpha] (c : NNReal) (omega : ContinuousPath alpha) (t : NNReal) : (rescale (Homeomorph.refl alpha) c omega) t = omega (c * t)

Rescaling by the identity homeomorphism speeds the path up without touching the state.

theorem MarkovProcess.ContinuousPath.rescale_one_apply {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (e : alpha ≃ₜ beta) (omega : ContinuousPath alpha) (t : NNReal) : (rescale e 1 omega) t = e (omega t)

Rescaling by the time factor one conjugates the state without touching the time.

theorem MarkovProcess.ContinuousPath.rescale_rescale {alpha : Type u_1} {beta : Type u_2} {gamma : Type u_3} [TopologicalSpace alpha] [TopologicalSpace beta] [TopologicalSpace gamma] (e : beta ≃ₜ gamma) (d : alpha ≃ₜ beta) (c b : NNReal) (omega : ContinuousPath alpha) : rescale e c (rescale d b omega) = rescale (d.trans e) (b * c) omega

Rescaling is jointly functorial in the homeomorphism and the time factor.

theorem MarkovProcess.ContinuousPath.continuous_rescale {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (e : alpha ≃ₜ beta) (c : NNReal) : Continuous (rescale e c)

Rescaling is continuous for the compact-open topology.

theorem MarkovProcess.ContinuousPath.measurable_rescale {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (e : alpha ≃ₜ beta) (c : NNReal) : Measurable (rescale e c)

Rescaling is Borel measurable on continuous-path space.

theorem MarkovProcess.ContinuousPath.finsetEvaluation_rescale {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (e : alpha ≃ₜ beta) (c : NNReal) (I : Finset NNReal) (omega : ContinuousPath alpha) : finsetEvaluation I (rescale e c omega) = fun (t : ↥I) => e (omega (c * ↑t))

Reading a rescaled path at a finite set of times reads the original path at the sped-up times and conjugates the states.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.continuousProcess_map_finiteEvaluation_ordered {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) {n : ℕ} (times : FiniteOrderedTimes n) : (IsConservative.continuousProcess P hP).map (ContinuousPath.finiteEvaluation fun (i : Fin n) => times i) = P.finiteTimeKernel times

Marginals at arbitrary ordered times. The law of the continuous-path process of a conservative Feller semigroup, read at a strictly increasing finite family of nonnegative times, is the finite-time kernel of P at those times. This is the finite-set marginal theorem of MarkovProcess/Main.lean transported to an arbitrary strictly increasing indexing.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess_eq_map_rescale {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {beta : Type u_2} [MetricSpace beta] [CompleteSpace beta] [MeasurableSpace beta] [BorelSpace beta] [SecondCountableTopology beta] [Nonempty beta] (P' : SubMarkovKernelSemigroup beta) (hP' : P'.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (hK' : P'.KolmogorovRegular hP') {e : alpha ≃ₜ beta} {c : NNReal} (hc : 0 < c) (h : P.IsRescaledConjugate P' e c) : continuousProcess P' hP' = ((continuousProcess P hP).comap ⇑e.symm ⋯).map (ContinuousPath.rescale e c)

Equivariance of the continuous-path process. If P' is the rescaled conjugate of a conservative Feller semigroup P by the homeomorphism e and the positive time factor c, then the continuous-path process of P' is the continuous-path process of P, started at the e-preimage of the initial state and pushed forward by the path map ContinuousPath.rescale e c.

The Feller hypothesis is needed only for P, because only the marginals of P at arbitrary real times are used; P' enters through its Kolmogorov regularity alone.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess_apply_rescale {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {beta : Type u_2} [MetricSpace beta] [CompleteSpace beta] [MeasurableSpace beta] [BorelSpace beta] [SecondCountableTopology beta] [Nonempty beta] (P' : SubMarkovKernelSemigroup beta) (hP' : P'.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (hK' : P'.KolmogorovRegular hP') {e : alpha ≃ₜ beta} {c : NNReal} (hc : 0 < c) (h : P.IsRescaledConjugate P' e c) (x : beta) : (continuousProcess P' hP') x = MeasureTheory.Measure.map (ContinuousPath.rescale e c) ((continuousProcess P hP) (e.symm x))

The equivariance identity at a fixed starting state: the law of the process of P' started at x is the law of the process of P started at e.symm x, pushed forward by the rescaling map.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess_eq_map_rescale_of_hasKolmogorovMoments {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {beta : Type u_2} [MetricSpace beta] [CompleteSpace beta] [MeasurableSpace beta] [BorelSpace beta] [SecondCountableTopology beta] [Nonempty beta] (P' : SubMarkovKernelSemigroup beta) (hP' : P'.IsConservative) (hFeller : P.IsFellerKernelSemigroup) {p q : ℝ} {M : NNReal} (hmom : P.HasKolmogorovMoments p q M) {e : alpha ≃ₜ beta} (he : Isometry ⇑e) {c : NNReal} (hc : 0 < c) (h : P.IsRescaledConjugate P' e c) : continuousProcess P' hP' = ((continuousProcess P hP).comap ⇑e.symm ⋯).map (ContinuousPath.rescale e c)

Intrinsic form of the equivariance theorem. When the state map is an isometry, the Kolmogorov moment criterion for P alone gives the regularity of both processes, by IsRescaledConjugate.hasKolmogorovMoments; no hypothesis on P' beyond conservativity and the intertwining is then needed.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess_eq_map_timeRescale {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (P' : SubMarkovKernelSemigroup alpha) (hP' : P'.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (hK' : P'.KolmogorovRegular hP') {c : NNReal} (hc : 0 < c) (htime : ∀ (t : NNReal), P'.kernel t = P.kernel (c * t)) : continuousProcess P' hP' = (continuousProcess P hP).map (ContinuousPath.rescale (Homeomorph.refl alpha) c)

Pure time rescaling. If the transition kernels of P' are those of P at the sped-up times, then the continuous-path process of P' is the continuous-path process of P pushed forward by the time change omega ↦ fun t ↦ omega (c * t). No state map is involved, so no starting point has to be relabelled.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess_eq_map_conjugate {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (P' : SubMarkovKernelSemigroup alpha) (hP' : P'.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (hK' : P'.KolmogorovRegular hP') {e : alpha ≃ₜ alpha} (hconj : ∀ (t : NNReal) (x : alpha), (P'.kernel t) x = MeasureTheory.Measure.map (⇑e) ((P.kernel t) (e.symm x))) : continuousProcess P' hP' = ((continuousProcess P hP).comap ⇑e.symm ⋯).map (ContinuousPath.rescale e 1)

Pure conjugation. If the transition kernels of P' are those of P conjugated by a homeomorphism e of the state space, then the continuous-path process of P' is the process of P started at e.symm x and read through e at every time.