Measurability of joint infimum occupation tests

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

theorem BGW.StableTrees.measurable_infimum_test {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : Measurable fun (p : NNReal × Skorokhod.DLoc) => F (localTime p.2 p.1) * G (↑(reflectedFrom 0 p.2) p.1)

Joint nonnegative tests of the infimum local time and the reflected position are measurable.

noncomputable def BGW.StableTrees.infimumTest (F G : ℝ → ENNReal) (p : NNReal × Skorokhod.DLoc) : ENNReal

A joint infimum occupation test, bundled before changing the time carrier.

Equations

• BGW.StableTrees.infimumTest F G p = F (BGW.StableTrees.localTime p.2 p.1) * G (↑(BGW.StableTrees.reflectedFrom 0 p.2) p.1)

theorem BGW.StableTrees.measurable_infimumTest {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : Measurable (infimumTest F G)

Measurability of the bundled joint infimum test.

noncomputable def BGW.StableTrees.infimumTestReal (F G : ℝ → ENNReal) (p : ℝ × Skorokhod.DLoc) : ENNReal

A joint infimum test read at a real-valued clock time.

Equations

• BGW.StableTrees.infimumTestReal F G p = BGW.StableTrees.infimumTest F G (p.1.toNNReal, p.2)

theorem BGW.StableTrees.measurable_infimumTestReal {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : Measurable (infimumTestReal F G)

Changing the clock carrier preserves measurability of the bundled test.