The multiplicative Cauchy equation on nonnegative reals, and the no-arrival law.

theorem BGW.Probability.prob_noMark_exp_exists {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (hξ : IsTimeSimpleLevy P ξ) (hA : IsFiniteRate P ξ A) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (t : NNReal), (P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}).toReal = Real.exp (-↑t * c)