Markov property of the stable process on local càdlàg paths

This module establishes the simple Markov property of the local stable process for its natural right-continuous filtration, together with its integral and conditional-expectation forms, the germ zero-one law, and the exponential martingale (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter I, Proposition 6 and Chapter VIII; R. M. Blumenthal, An extended Markov property, Trans. Amer. Math. Soc. 85 (1957), for the zero-one law).

theorem BGW.Skorokhod.DLoc.measurable_shift_fixed (s : NNReal) : Measurable (shift s)

The centered shift by a fixed time is measurable (restriction of measurable_shift).

theorem BGW.Skorokhod.DLoc.eval_shift (s u : NNReal) (f : DLoc) : eval u (shift s f) = eval (s + u) f - eval s f

Evaluation of the shift: eval u (shift s f) = eval (s + u) f - eval s f.

theorem BGW.StableTrees.map_shift_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s : NNReal) : MeasureTheory.Measure.map (Skorokhod.DLoc.shift s) ↑(stableLocalLaw θ) = ↑(stableLocalLaw θ)

Law of the future. After any deterministic time s ≥ 0 the centered path has the original law (s = 0 included).

theorem BGW.StableTrees.integral_shiftIncrement_mul_past_stableProcessLaw {θ T s : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hs : 0 ≤ s) (hsT : s ≤ T) (P : MeasureTheory.Measure (Skorokhod.D T ℝ)) (hP : P = ↑(stableProcessLaw θ T)) (Q : MeasureTheory.Measure (Skorokhod.D (T - s) ℝ)) (hQ : Q = ↑(stableProcessLaw θ (T - s))) {m : MeasurableSpace (Skorokhod.D T ℝ)} (hm : m ≤ MeasurableSpace.comap (Skorokhod.restrict hsT) inferInstance) {A : Set (Skorokhod.D T ℝ)} (hA : MeasurableSet A) {F : Skorokhod.D (T - s) ℝ → ℝ} (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (x : Skorokhod.D (T - s) ℝ), |F x| ≤ C) : ∫ (f : Skorokhod.D T ℝ) in A, F (Skorokhod.shiftIncrement hs hsT f) ∂P = P.real A * ∫ (g : Skorokhod.D (T - s) ℝ), F g ∂Q

Bounded-test form. For every sub-σ-algebra m ≤ comap (restrict hsT) of the natural past, A m-measurable and bounded Borel F on the future path space, ∫_A F(future) dP = P(A) · ∫ F d(law of the future). The measures P, Q are bound before m (with equations to the stable laws) so that they carry the Borel σ-algebra, not m, which would otherwise become the local MeasurableSpace (D T ℝ) instance.

theorem BGW.StableTrees.indep_comap_restrict_shiftIncrement_stableProcessLaw {θ T s : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hs : 0 ≤ s) (hsT : s ≤ T) : ProbabilityTheory.Indep (MeasurableSpace.comap (Skorokhod.restrict hsT) inferInstance) (MeasurableSpace.comap (Skorokhod.shiftIncrement hs hsT) inferInstance) ↑(stableProcessLaw θ T)

Past/future independence in σ-algebra form on D T ℝ: the σ-algebra pulled back by restrict hsT (natural past up to s) is independent of the σ-algebra of the future increment path.

theorem BGW.StableTrees.indep_rawFiltration_shift_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s : NNReal) : ProbabilityTheory.Indep (↑Skorokhod.DLoc.rawFiltration s) (MeasurableSpace.comap (Skorokhod.DLoc.shift s) inferInstance) ↑(stableLocalLaw θ)

The same independence from the raw past F_s = DLoc.rawFiltration s (the first, easier step; follows from the compact simple Markov property).

theorem BGW.StableTrees.indep_filtration_shift_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s : NNReal) : ProbabilityTheory.Indep (↑Skorokhod.DLoc.filtration s) (MeasurableSpace.comap (Skorokhod.DLoc.shift s) inferInstance) ↑(stableLocalLaw θ)

Simple Markov property, σ-algebra form. The future increment path after s is independent of the right-continuous past F_s^+ = DLoc.filtration s.

theorem BGW.StableTrees.integral_shift_mul_past {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s : NNReal) {A : Set Skorokhod.DLoc} (hA : MeasurableSet A) {F : Skorokhod.DLoc → ℝ} (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (x : Skorokhod.DLoc), |F x| ≤ C) : ∫ (f : Skorokhod.DLoc) in A, F (Skorokhod.DLoc.shift s f) ∂↑(stableLocalLaw θ) = (↑(stableLocalLaw θ)).real A * ∫ (f : Skorokhod.DLoc), F f ∂↑(stableLocalLaw θ)

Bounded-test corollary (whole future). For A ∈ F_s^+ and bounded Borel F on DLoc, ∫_A F(shift_s f) dP = P(A) · ∫ F dP.

theorem BGW.StableTrees.integral_futureSegment_mul_past {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s U : NNReal) {A : Set Skorokhod.DLoc} (hA : MeasurableSet A) {F : Skorokhod.D ↑U ℝ → ℝ} (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (x : Skorokhod.D ↑U ℝ), |F x| ≤ C) : ∫ (f : Skorokhod.DLoc) in A, F (Skorokhod.DLoc.restrict U (Skorokhod.DLoc.shift s f)) ∂↑(stableLocalLaw θ) = (↑(stableLocalLaw θ)).real A * ∫ (g : Skorokhod.D ↑U ℝ), F g ∂↑(stableProcessLaw θ ↑U)

Bounded-test corollary (compact future window). The blueprint form: the future after s centered and cut at horizon U, tested by bounded Borel F on D U ℝ. The right side uses stableProcessLaw θ U.

theorem BGW.StableTrees.integral_mul_shift_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s : NNReal) {G : Skorokhod.DLoc → ℝ} (hG : Measurable G) (hGb : ∃ (C : ℝ), ∀ (x : Skorokhod.DLoc), |G x| ≤ C) {F : Skorokhod.DLoc → ℝ} (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (x : Skorokhod.DLoc), |F x| ≤ C) : ∫ (f : Skorokhod.DLoc), G f * F (Skorokhod.DLoc.shift s f) ∂↑(stableLocalLaw θ) = (∫ (f : Skorokhod.DLoc), G f ∂↑(stableLocalLaw θ)) * ∫ (f : Skorokhod.DLoc), F f ∂↑(stableLocalLaw θ)

Product form: E[G · F(shift_s)] = E[G] · E[F] for G bounded F_s^+-measurable and F bounded Borel.

theorem BGW.StableTrees.condExp_shift_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s : NNReal) {F : Skorokhod.DLoc → ℝ} (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (x : Skorokhod.DLoc), |F x| ≤ C) : (↑(stableLocalLaw θ))[fun (f : Skorokhod.DLoc) => F (Skorokhod.DLoc.shift s f) | ↑Skorokhod.DLoc.filtration s] =ᵐ[↑(stableLocalLaw θ)] fun (x : Skorokhod.DLoc) => ∫ (f : Skorokhod.DLoc), F f ∂↑(stableLocalLaw θ)

Conditional-expectation form. Given F_s^+, a bounded Borel functional of the future has the constant conditional expectation ∫ F dP.

theorem BGW.StableTrees.measure_zeroOne_filtration_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {A : Set Skorokhod.DLoc} (hA : MeasurableSet A) : ↑(stableLocalLaw θ) A = 0 ∨ ↑(stableLocalLaw θ) A = 1

Germ zero-one law (s = 0): every event of F_0^+ has probability 0 or 1.

theorem BGW.StableTrees.martingale_exp_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {u : ℝ} (hu : 0 ≤ u) : MeasureTheory.Martingale (fun (t : NNReal) (f : Skorokhod.DLoc) => Real.exp (-u * Skorokhod.DLoc.eval t f - ↑t * u ^ θ)) Skorokhod.DLoc.filtration ↑(stableLocalLaw θ)

Martingale export: for u ≥ 0 the exponential process exp(-u X_t - t u^θ) is a martingale for the right-continuous filtration.