Second moments of reflected occupation resolvents

The signed occupation identity is the generic resolvent moment theorem specialized to the reflected family.

Reference: A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 8.

theorem BGW.StableTrees.integral_sq_discountedOccupation_supOccupation_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : ∫ (f : Skorokhod.DLoc), Probability.discountedOccupation (fun (t : NNReal) (f : Skorokhod.DLoc) => supReflectedFrom x f t) (fun (r : ℝ) => supOccKernel ε r - supOccKernel η r) f ^ 2 ∂↑(stableLocalLaw θ) = 2 * ∫ (f : Skorokhod.DLoc), ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-2 * t) * ((supOccKernel ε (supReflectedFrom x f t.toNNReal) - supOccKernel η (supReflectedFrom x f t.toNNReal)) * (supOccupationResolvent θ 1 ε (supReflectedFrom x f t.toNNReal) - supOccupationResolvent θ 1 η (supReflectedFrom x f t.toNNReal))) ∂↑(stableLocalLaw θ)

Signed second-moment identity for the difference of two positive occupation cutoffs.