Strong Markov property of the reflected process for the augmented filtration

The usual augmentation of the canonical filtration under the stable law: the raw right-continuous filtration joined with the null sets of the law, then regularized on the right, on the completed space. Every augmented event differs from a raw event by a null set, every augmented stopping time is almost surely equal to a raw one, and every event of an augmented stopped σ-algebra differs from a raw stopped event by a null set (through the stopping time equal to τ on the event and infinite off it). With integrals under the completed law, this transfers the strong Markov property of the reflected process X − I to stopping times of the augmented filtration (condExp_reflectedFutureAt_augmented, C20).

@[reducible, inline]

abbrev BGW.StableTrees.StableCompletedSpace (θ : ℝ) : Type

The canonical space with the completion σ-algebra of the stable law.

Equations

• BGW.StableTrees.StableCompletedSpace θ = MeasureTheory.NullMeasurableSpace BGW.Skorokhod.DLoc ↑(BGW.StableTrees.stableLocalLaw θ)

noncomputable def BGW.StableTrees.stableAugmentedBase (θ : ℝ) : MeasureTheory.Filtration NNReal inferInstance

The raw right-continuous filtration joined with the null sets of the stable law.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.stableAugmentedFiltration (θ : ℝ) : MeasureTheory.Filtration NNReal inferInstance

The usual augmentation of the canonical filtration under the stable law.

Equations

• BGW.StableTrees.stableAugmentedFiltration θ = (BGW.StableTrees.stableAugmentedBase θ).rightCont

theorem BGW.StableTrees.measurableSet_stableAugmentedFiltration_of_null {θ : ℝ} (t : NNReal) {A : Set Skorokhod.DLoc} (hA : ↑(stableLocalLaw θ) A = 0) : MeasurableSet A

Every null event belongs to every stage of the augmented filtration.

theorem BGW.StableTrees.stableAugmentedFiltration_le_completion (θ : ℝ) (t : NNReal) : ↑Skorokhod.DLoc.filtration t ≤ ↑(stableAugmentedFiltration θ) t

The raw right-continuous filtration is contained in its usual augmentation.

theorem BGW.StableTrees.condExp_reflectedFutureAt_augmented {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {τ : StableCompletedSpace θ → ENNReal} (hτ : MeasureTheory.IsStoppingTime (stableAugmentedFiltration θ) τ) (hfin : ∀ᵐ (f : StableCompletedSpace θ) ∂(↑(stableLocalLaw θ)).completion, τ f < ⊤) {G : Skorokhod.DLoc → ℝ} (hG : Measurable G) (hGb : ∃ (C : ℝ), ∀ (p : Skorokhod.DLoc), |G p| ≤ C) : (↑(stableLocalLaw θ)).completion[fun (f : StableCompletedSpace θ) => G (reflectedFutureAt τ f) | hτ.measurableSpace] =ᵐ[(↑(stableLocalLaw θ)).completion] fun (f : MeasureTheory.NullMeasurableSpace Skorokhod.DLoc ↑(stableLocalLaw θ)) => ∫ (g : Skorokhod.DLoc), G (reflectedFrom (reflectedStateAt τ f) g) ∂↑(stableLocalLaw θ)

C20.1, strong Markov property for the augmented filtration. For a stopping time of the usual augmentation, conditionally on its stopped σ-algebra, the post-τ reflected path has the reflected stable transition law started at its stopped reflected value.