4.2. 2. Analytic facts🔗

Theorem4.2.1

Group: The exponential race. (10)

Group member previews

Preview

Theorem 4.2.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 4.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

XL∃∀N

Tagspaper proof

Lemma R1 (interval theorem, Campbell formula and Laplace functional). Let D_1, D_2, \ldots be independent rate-one exponential variables, and let N = \{D_1 + \cdots + D_k : k \ge 1\}. Then N is a rate-one Poisson process: counts in disjoint Borel sets of finite Lebesgue measure are independent Poisson variables with those measures as means. For every nonnegative measurable g : (0,\infty) \to [0,\infty],

\mathbb E\sum_{t\in N}g(t)=\int_0^\infty g(t)\,dt,\qquad \mathbb E\exp\!\left(-\sum_{t\in N}g(t)\right) =\exp\!\left(-\int_0^\infty(1-e^{-g(t)})\,dt\right). \qquad \text{(R2)}

Extended nonnegative integrals are allowed and e^{-\infty} = 0.

Proof for Theorem 4.2.1

uses 0

Apply the interval theorem, calculate the formulas for simple functions using independent Poisson counts, and pass to general nonnegative functions by convergence. See the page section.

Lean: Lemma R1 is not stated in general. The arrival times are the partial sums arrivalTime of independent rate-one exponential increments under arrivalLaw (NaturalLatents/General/Definitions.lean), and the Laplace functional is stated only for the shifted power sums the race uses: race_shifted_arrival_laplace, with g(s)=v(t+s)^{-a}, and race_arrival_laplace, which evaluates the case t=0 in the Gamma form of (R20) and (R21) (NaturalLatents/General/RaceLaplace.lean). Lean has no Poisson process, interval theorem or Campbell formula; it obtains the transform from a renewal equation (race_arrival_laplace_renewal and race_renewal_unique).

Theorem4.2.2

Group: The exponential race. (10)

Group member previews

Preview

Theorem 4.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 4.3.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagspartly kernel-verified

Lemma R2 (Frullani logarithm identities). For every x \ge 0 and every r > 0,

\ln(1+x)=\int_0^\infty e^{-v}\frac{1-e^{-vx}}v\,dv,\qquad \ln r=\int_0^\infty\frac{e^{-v}-e^{-vr}}v\,dv. \qquad \text{(R4)}

If R > 0 almost surely and \mathbb E\lvert\ln R\rvert < \infty, then

\mathbb E\ln R=\int_0^\infty\frac{e^{-v}-\mathbb E e^{-vR}}v\,dv. \qquad \text{(R5)}

Lean code for Theorem4.2.2●2 theorems

theoremdefined in NaturalLatents/General/ExponentialRace.lean

complete

theorem NaturalLatents.General.race_frullani_log_one_add (x : ℝ) (hx : 0 ≤ x) :
  ∫⁻ (v : ℝ) in Set.Ioi 0,
      ENNReal.ofReal (Real.exp (-v) * v⁻¹ * (1 - Real.exp (-(v * x)))) =
    ENNReal.ofReal (Real.log (1 + x))

theorem NaturalLatents.General.race_frullani_log_one_add
  (x : ℝ) (hx : 0 ≤ x) :
  ∫⁻ (v : ℝ) in Set.Ioi 0,
      ENNReal.ofReal
        (Real.exp (-v) * v⁻¹ *
          (1 - Real.exp (-(v * x)))) =
    ENNReal.ofReal (Real.log (1 + x))

theoremdefined in NaturalLatents/General/ExponentialRace.lean

complete

theorem NaturalLatents.General.race_expected_log_one_add_laplace.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure μ] (V : Ω → ℝ)
  (hVm : Measurable V) (hVnn : 0 ≤ᵐ[μ] V)
  (hlog : MeasureTheory.Integrable (fun ω => Real.log (1 + V ω)) μ) :
  ENNReal.ofReal (∫ (ω : Ω), Real.log (1 + V ω) ∂μ) =
    ∫⁻ (v : ℝ) in Set.Ioi 0,
      ENNReal.ofReal
        (Real.exp (-v) * v⁻¹ *
          (1 - ∫ (ω : Ω), Real.exp (-(v * V ω)) ∂μ))

theorem NaturalLatents.General.race_expected_log_one_add_laplace.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure μ]
  (V : Ω → ℝ) (hVm : Measurable V)
  (hVnn : 0 ≤ᵐ[μ] V)
  (hlog :
    MeasureTheory.Integrable
      (fun ω => Real.log (1 + V ω)) μ) :
  ENNReal.ofReal
      (∫ (ω : Ω), Real.log (1 + V ω) ∂μ) =
    ∫⁻ (v : ℝ) in Set.Ioi 0,
      ENNReal.ofReal
        (Real.exp (-v) * v⁻¹ *
          (1 -
            ∫ (ω : Ω),
              Real.exp (-(v * V ω)) ∂μ))

Expected log gain from its Laplace transform. The identity is stated in
ENNReal so that Tonelli needs no product integrability hypothesis.

Proof for Theorem 4.2.2

uses 0

Lean proves: the \ln(1+x) identity of (R4) for x\ge0 and its expected-log analogue for measurable V\ge0 with integrable \ln(1+V), both as extended nonnegative integrals.

Differentiate the scalar integrals under domination, then apply Tonelli and Fubini using absolute log integrability. See the page section.

Lean: race_frullani_log_one_add (the first identity of (R4), as an extended nonnegative integral) and race_expected_log_one_add_laplace (the corresponding identity for \mathbb E\ln(1+V), for measurable V\ge0 almost surely with \mathbb E\ln(1+V)<\infty, also in extended nonnegative integral form), both in NaturalLatents/General/ExponentialRace.lean. The identity for \ln r and (R5) for a general positive R are not stated.

Theorem4.2.3

Group: The exponential race. (10)

Group member previews

Preview

Theorem 4.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 4.3.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagspartly kernel-verified

Lemma R3 (Gamma integral and Euler's logarithmic integral). Let b > 0, and let \gamma_E = \lim_{N\to\infty}\left(\sum_{k=1}^N 1/k-\ln N\right) be Euler's constant. The classical identities needed in the race calculation are

\Gamma(b)=\int_0^\infty e^{-y}y^{b-1}\,dy,\qquad \int_0^\infty e^{-y}\,dy=1,\qquad \int_0^\infty e^{-y}\ln y\,dy=-\gamma_E. \qquad \text{(R6)}

Lean code for Theorem4.2.3●4 theorems

theoremdefined in NaturalLatents/General/RaceLaplace.lean

complete

theorem NaturalLatents.General.race_scalar_exp_log_integrable_mean :
  MeasureTheory.Integrable Real.log (ProbabilityTheory.expMeasure 1) ∧
    ∫ (t : ℝ), Real.log t ∂ProbabilityTheory.expMeasure 1 =
      -Real.eulerMascheroniConstant

theorem NaturalLatents.General.race_scalar_exp_log_integrable_mean :
  MeasureTheory.Integrable Real.log
      (ProbabilityTheory.expMeasure 1) ∧
    ∫ (t : ℝ),
        Real.log
          t ∂ProbabilityTheory.expMeasure
          1 =
      -Real.eulerMascheroniConstant

theoremdefined in Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

complete

theorem Real.Gamma_eq_integral {s : ℝ} (hs : 0 < s) :
  Real.Gamma s = ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x) * x ^ (s - 1)

theorem Real.Gamma_eq_integral {s : ℝ}
  (hs : 0 < s) :
  Real.Gamma s =
    ∫ (x : ℝ) in Set.Ioi 0,
      Real.exp (-x) * x ^ (s - 1)

theoremdefined in Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

complete

theorem Real.GammaIntegral_convergent {s : ℝ} (h : 0 < s) :
  MeasureTheory.IntegrableOn (fun x => Real.exp (-x) * x ^ (s - 1))
    (Set.Ioi 0) MeasureTheory.volume

theorem Real.GammaIntegral_convergent {s : ℝ}
  (h : 0 < s) :
  MeasureTheory.IntegrableOn
    (fun x => Real.exp (-x) * x ^ (s - 1))
    (Set.Ioi 0) MeasureTheory.volume

The Euler integral for the `Γ` function converges for positive real `s`.

theoremdefined in NaturalLatents/General/RaceLaplace.lean

complete

theorem NaturalLatents.General.race_exp_rpow_moment (p : ℝ) (hp : -1 < p) :
  MeasureTheory.Integrable (fun y => y ^ p)
      (ProbabilityTheory.expMeasure 1) ∧
    ∫ (y : ℝ), y ^ p ∂ProbabilityTheory.expMeasure 1 =
      Real.Gamma (1 + p)

theorem NaturalLatents.General.race_exp_rpow_moment
  (p : ℝ) (hp : -1 < p) :
  MeasureTheory.Integrable
      (fun y => y ^ p)
      (ProbabilityTheory.expMeasure 1) ∧
    ∫ (y : ℝ),
        y ^
          p ∂ProbabilityTheory.expMeasure
          1 =
      Real.Gamma (1 + p)

Proof for Theorem 4.2.3

uses 0

Lean proves: the Gamma integral and its convergence for b>0, \mathbb E\ln T=-\gamma_E with integrable \ln T for T\sim\mathrm{Exp}(1), and \mathbb ET^p=\Gamma(1+p) for p>-1.

Use Euler’s Gamma and logarithmic integrals, checking absolute convergence separately at zero and infinity. See the page section.

Lean: race_scalar_exp_log_integrable_mean (NaturalLatents/General/RaceLaplace.lean) states the integrability and the mean of \ln T under T\sim\mathrm{Exp}(1), equivalently the density-weighted integral in (R6). The Gamma integral is Mathlib's Real.Gamma_eq_integral for positive arguments, with integrability Real.GammaIntegral_convergent; the race uses them through race_exp_rpow_moment (NaturalLatents/General/RaceLaplace.lean). No single declaration combines the three integrals.