Common Laplace half-line for two nonnegative discounts under unbounded variation

Proved

AvramDividend.Classical.unbounded_psi_two_discounts_common_tail

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-classicallaplace-exponentlevyresolventscale-function

For any pair of nonnegative discount rates, an unbounded-variation spectrally negative Lévy process admits a common right-hand Laplace-transform domain where both discount rates lie strictly below its Laplace exponent. This discharges the shared-tail hypothesis of the proved real-space scale resolvent theorem.

Preamble

import Mathlib.Tactic.Linarith
import Theorems.Thm_AvramDividend_Classical_unbounded_psi_discount_denominator_eventually_linear
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_psi_two_discounts_common_tail
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (hnbv : ¬ X.BoundedVariation)
    (q₁ q₂ : ℝ) (hq₁ : 0 ≤ q₁) (hq₂ : 0 ≤ q₂) :
    ∃ b : ℝ, 0 ≤ b ∧ ∀ θ : ℝ, b < θ →
      0 ≤ θ ∧ q₁ < X.ψ θ ∧ q₂ < X.ψ θ := by sorry

Source

Direct consequence of the already Proved unbounded_psi_discount_denominator_eventually_linear at C = 0, combined with max of the two thresholds.

View graph