The exponential transform on extended nonnegative reals and finite-subset excursion pgfs.

See Bertoin, Lévy Processes, Chapter IV.

noncomputable def BGW.StableTrees.expNeg (x : ENNReal) : ENNReal

exp (-x) on ℝ≥0∞, with exp (-∞) = 0.

Equations

• BGW.StableTrees.expNeg x = if x = ⊤ then 0 else ENNReal.ofReal (Real.exp (-x.toReal))

theorem BGW.StableTrees.expNeg_eq_ereal (x : ENNReal) : expNeg x = (-↑x).exp

The exponential transform is the continuous extended-real exponential of the negated input.

theorem BGW.StableTrees.continuous_expNeg : Continuous expNeg

The exponential transform is continuous, including its value zero at infinity.

theorem BGW.StableTrees.antitone_expNeg : Antitone expNeg

The exponential transform decreases with its argument.

@[simp]

theorem BGW.StableTrees.expNeg_zero : expNeg 0 = 1

The exponential transform at zero is one.

@[simp]

theorem BGW.StableTrees.expNeg_top : expNeg ⊤ = 0

The exponential transform at infinity is zero.

theorem BGW.StableTrees.expNeg_le_one (x : ENNReal) : expNeg x ≤ 1

Exponential transforms take values at most one.

theorem BGW.StableTrees.expNeg_add (x y : ENNReal) : expNeg (x + y) = expNeg x * expNeg y

The exponential transform takes sums to products.

theorem BGW.StableTrees.expNeg_mul_nat (x : ENNReal) (n : ℕ) : expNeg (x * ↑n) = expNeg x ^ n

Multiplication by a natural number becomes an exponential-transform power.

theorem BGW.StableTrees.excursion_pgf_subsets {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) (T ε : NNReal) (hε : 0 < ε) {k : ℕ} (B : Fin k → Set (NNReal × Excursion)) (hB : ∀ (i : Fin k), MeasurableSet (B i)) (hsub : ∀ (i : Fin k), B i ⊆ Set.Ioc 0 T ×ˢ {e : Excursion | ε < e.lifetime}) (hd : Pairwise (Function.onFun Disjoint B)) (z : Fin k → ℝ) (hz0 : ∀ (i : Fin k), 0 ≤ z i) (hz1 : ∀ (i : Fin k), z i ≤ 1) : ∫ (f : Skorokhod.DLoc), ∏ i : Fin k, z i ^ Probability.natCount (ξ f) (B i) ∂↑(stableLocalLaw θ) = Real.exp (∑ i : Fin k, ((lebNN.prod (excursionMeasure θ)) (B i)).toReal * (z i - 1))

Joint real pgfs for arbitrary disjoint measurable subsets of a bounded lifetime-slab box.