4.3. 3. The race
Lemma R4 (calibrated exponential winner). Let r = (r_i)_{i=1}^n be a strictly positive probability vector and let
E_1, \ldots, E_n be independent rate-one exponential variables. With any fixed ordering to resolve ties, put
W = \arg\min_i E_i/r_i and T = \min_i E_i/r_i. Then
\Pr(W=i,\ T\in dt)
=r_i e^{-r_i t}\prod_{k\ne i}e^{-r_k t}\,dt
=r_i e^{-t}\,dt.
\qquad \text{(R7)}
Consequently W has law r, T has law \mathrm{Exp}(1), W and T are independent, and E_i = r_i T on
W = i. For every finite source with positive rows r_z, the maps A_E(z) = \arg\min_i E_i/r_z(i), with E
independent of the source, are calibrated.
Lean code for Theorem4.3.1●4 theorems
Associated Lean declarations
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_clock_probability {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hpos : ∀ (i : κ), 0 < r i) (i : κ) : ∫ (E : κ → ℝ), if stoch_to_det.SharedRace.clockArgmin r E = i then 1 else 0 ∂stoch_to_det.clockLaw κ = r i
theorem NaturalLatents.General.race_clock_probability {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hpos : ∀ (i : κ), 0 < r i) (i : κ) : ∫ (E : κ → ℝ), if stoch_to_det.SharedRace.clockArgmin r E = i then 1 else 0 ∂stoch_to_det.clockLaw κ = r i
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_seed_probability {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hpos : ∀ (i : κ), 0 < r i) (i : κ) : ∫ (G : κ → ℝ), if stoch_to_det.SharedRace.weightedLexWinner r G = i then 1 else 0 ∂stoch_to_det.seedLaw κ = r i
theorem NaturalLatents.General.race_seed_probability {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hpos : ∀ (i : κ), 0 < r i) (i : κ) : ∫ (G : κ → ℝ), if stoch_to_det.SharedRace.weightedLexWinner r G = i then 1 else 0 ∂stoch_to_det.seedLaw κ = r i
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_map_calibrated {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) : ∃ F, F.seedLaw = fun A => ∫ (G : L.ι → ℝ), if stoch_to_det.SharedRace.sharedWinner (fun z i => NaturalLatents.General.posterior L i z) G = A then 1 else 0 ∂stoch_to_det.seedLaw L.ι
theorem NaturalLatents.General.race_map_calibrated {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) : ∃ F, F.seedLaw = fun A => ∫ (G : L.ι → ℝ), if stoch_to_det.SharedRace.sharedWinner (fun z i => NaturalLatents.General.posterior L i z) G = A then 1 else 0 ∂stoch_to_det.seedLaw L.ι
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_selected_coordinate_average {κ Ξ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] [MeasurableSpace Ξ] (ν : MeasureTheory.Measure Ξ) [MeasureTheory.IsProbabilityMeasure ν] (r : κ → ℝ) (hrpos : ∀ (i : κ), 0 < r i) (hrtotal : ∑ i, r i = 1) (f : κ → ℝ × Ξ → ℝ) (hfmeas : ∀ (i : κ), Measurable (f i)) (hfint : ∀ (i : κ), MeasureTheory.Integrable (f i) (NaturalLatents.General.expOne.prod ν)) : have νκ := MeasureTheory.Measure.pi fun x => ν; have ρ := (stoch_to_det.clockLaw κ).prod νκ; have selected := fun w => f (stoch_to_det.SharedRace.clockArgmin r w.1) (w.1 (stoch_to_det.SharedRace.clockArgmin r w.1), w.2 (stoch_to_det.SharedRace.clockArgmin r w.1)); MeasureTheory.Integrable selected ρ ∧ ∫ (w : (κ → ℝ) × (κ → Ξ)), selected w ∂ρ = ∑ i, r i * ∫ (t : ℝ), ∫ (ξ : Ξ), f i (r i * t, ξ) ∂ν ∂NaturalLatents.General.expOne
theorem NaturalLatents.General.race_selected_coordinate_average {κ Ξ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] [MeasurableSpace Ξ] (ν : MeasureTheory.Measure Ξ) [MeasureTheory.IsProbabilityMeasure ν] (r : κ → ℝ) (hrpos : ∀ (i : κ), 0 < r i) (hrtotal : ∑ i, r i = 1) (f : κ → ℝ × Ξ → ℝ) (hfmeas : ∀ (i : κ), Measurable (f i)) (hfint : ∀ (i : κ), MeasureTheory.Integrable (f i) (NaturalLatents.General.expOne.prod ν)) : have νκ := MeasureTheory.Measure.pi fun x => ν; have ρ := (stoch_to_det.clockLaw κ).prod νκ; have selected := fun w => f (stoch_to_det.SharedRace.clockArgmin r w.1) (w.1 (stoch_to_det.SharedRace.clockArgmin r w.1), w.2 (stoch_to_det.SharedRace.clockArgmin r w.1)); MeasureTheory.Integrable selected ρ ∧ ∫ (w : (κ → ℝ) × (κ → Ξ)), selected w ∂ρ = ∑ i, r i * ∫ (t : ℝ), ∫ (ξ : Ξ), f i (r i * t, ξ) ∂ν ∂NaturalLatents.General.expOne
A general coordinate statistic selected by the race can be averaged by first integrating the independent appendages and then using the exact winning-cell residual-clock law. No cardinality lower bound is needed.
Lean proves: \Pr(W=i)=r_i, calibration of the map-valued race seed, and the selected-clock averaging identity \mathbb Ef_W(E_W,\Omega_W)=\sum_i r_i\mathbb E_{T,\Omega}f_i(r_iT,\Omega) for measurable integrable statistics.
Multiply the winner density by the other clocks’ survival probabilities and exclude the finite union of tie events. See the page section.
Lean: race_clock_probability (the winner has law r), race_seed_probability (the same in Gumbel coordinates) and
race_map_calibrated (the calibrated family), all in NaturalLatents/General/RaceTransport.lean. Lean runs the race in
Gumbel coordinates G_i=-\ln E_i under stoch_to_det.seedLaw (NaturalLatents/Upstream/Seed.lean), with winner
stoch_to_det.SharedRace.weightedLexWinner, the lexicographic maximizer of \ln r_i+G_i
(NaturalLatents/Upstream/SharedRace/Definitions.lean) (from pull request #5 by Satya Benson), which is \arg\min_iE_i/r_i with a fixed tie rule. The
density (R7) and the independence of W and T are not stated; their consequence for averages of a statistic of the
winning clock is race_selected_coordinate_average (NaturalLatents/General/ExponentialRace.lean).
Lemma R5 (appended reference masses are finite). Let a > 1, let \pi = (\pi_i)_{i=1}^n be a strictly positive
probability vector, and let E_i be independent rate-one exponential variables. Append to each E_i independent
rate-one exponential spacings, independent across labels and of all E_i. Let T_{i1} = E_i, T_{i2}, \ldots be the
resulting arrival times, and set
J_i=\pi_i^aE_i^{-a},\quad
S_i=\pi_i^a\sum_{k\ge1}T_{ik}^{-a},\quad
S=\sum_iS_i,\quad Q_i=S_i/S.
\qquad \text{(R8)}
Then every S_i and S is finite and strictly positive almost surely, so Q is a strictly positive probability
vector. For a separate rate-one Poisson process N, define
V_t=\sum_{v\in N}\left(\frac{t}{t+v}\right)^a\ (t>0),
\quad V_0=0,\qquad m_a(t)=\mathbb E\ln(1+V_t).
\qquad \text{(R9)}
Conditionally on E_i = t > 0, S_i = J_i(1 + V_t^{(i)}), where V_t^{(i)} uses the appended process for label
i, and
\mathbb EV_t
=\int_0^\infty\left(\frac{t}{t+v}\right)^a\,dv
=t\int_0^\infty(1+s)^{-a}\,ds
=\frac{t}{a-1}.
\qquad \text{(R10)}
Lean code for Theorem4.3.2●2 theorems
Associated Lean declarations
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_arrival_mass_ae_summable (a : ℝ) (ha : 1 < a) : ∀ᵐ (ω : ℕ → ℝ) ∂NaturalLatents.General.arrivalLaw, ∀ (t : ℝ), 0 ≤ t → Summable fun n => (t + NaturalLatents.General.arrivalTime ω (n + 1)) ^ (-a)
theorem NaturalLatents.General.race_arrival_mass_ae_summable (a : ℝ) (ha : 1 < a) : ∀ᵐ (ω : ℕ → ℝ) ∂NaturalLatents.General.arrivalLaw, ∀ (t : ℝ), 0 ≤ t → Summable fun n => (t + NaturalLatents.General.arrivalTime ω (n + 1)) ^ (-a)
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_reference_isPMF {κ : Type} [Fintype κ] [Nonempty κ] (π : κ → ℝ) (hπpos : ∀ (i : κ), 0 < π i) (a : ℝ) (w : (κ → ℝ) × (κ → ℕ → ℝ)) : have S := fun i => π i ^ a * Real.exp (-w.1 i) ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a (Real.exp (-w.1 i)) (w.2 i))); have Q := fun i => S i / ∑ k, S k; stoch_to_det.IsPMF Q ∧ ∀ (i : κ), 0 < Q i
theorem NaturalLatents.General.race_reference_isPMF {κ : Type} [Fintype κ] [Nonempty κ] (π : κ → ℝ) (hπpos : ∀ (i : κ), 0 < π i) (a : ℝ) (w : (κ → ℝ) × (κ → ℕ → ℝ)) : have S := fun i => π i ^ a * Real.exp (-w.1 i) ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a (Real.exp (-w.1 i)) (w.2 i))); have Q := fun i => S i / ∑ k, S k; stoch_to_det.IsPMF Q ∧ ∀ (i : κ), 0 < Q i
The max only totalizes invalid appendage sequences; it is inactive a.s. for positive spacings.
Lean proves: the shifted arrival power sums are almost surely summable for a>1, and the totalized reference Q is a strictly positive probability vector at every seed.
Use Campbell’s formula for the appended process; finite conditional expectation gives almost sure finiteness and the first arrival gives positivity. See the page section.
Lean: tailSum, logGain and arrivalLaw (NaturalLatents/General/Definitions.lean) are V_t, m_a and the law of the
appended spacings. race_arrival_mass_ae_summable (NaturalLatents/General/RaceLaplace.lean) gives almost-sure
finiteness of the appended sums, and race_reference_isPMF (NaturalLatents/General/RaceTransport.lean) states that
Q is a strictly positive probability vector. Lean totalizes the reference: it uses 1+\max(0,V_t), and a divergent
series has value zero, so Q is a positive probability vector at every seed. The mean (R10) is not stated.
-
NaturalLatents.General.race_logGain_zero[complete] -
NaturalLatents.General.race_logGain_nonneg[complete] -
NaturalLatents.General.race_gain_scaling_of_shifted_transform[complete] -
NaturalLatents.General.race_tailSum_laplace_of_shifted_transform[complete] -
NaturalLatents.General.race_expected_log_gain_scaling_of_laplace[complete] -
NaturalLatents.General.race_laplace_gain_scalar_concavity[complete] -
NaturalLatents.General.race_unit_log_integrable[complete] -
NaturalLatents.General.race_scalar_log_integrable_of_stable_laplace[complete]
Lemma R6 (concave gain and absolute log integrability). Let a > 1 and define V_t, m_a by (R9). Then
m_a(0) = 0, 0 \le m_a(t) \le t/(a-1) for t \ge 0, m_a is concave on [0,\infty), and
m_a(rt)\ge r\,m_a(t)\qquad(t\ge0,\ 0\le r\le1).
\qquad \text{(R11)}
For every strictly positive probability vector \pi and reference masses S_i, S constructed as in (R8),
\mathbb E\lvert\ln S_i\rvert < \infty, \mathbb E\lvert\ln J_i\rvert < \infty, and
\mathbb E\lvert\ln S\rvert < \infty.
Lean code for Theorem4.3.3●8 theorems
Associated Lean declarations
-
NaturalLatents.General.race_logGain_zero[complete]
-
NaturalLatents.General.race_logGain_nonneg[complete]
-
NaturalLatents.General.race_gain_scaling_of_shifted_transform[complete]
-
NaturalLatents.General.race_tailSum_laplace_of_shifted_transform[complete]
-
NaturalLatents.General.race_expected_log_gain_scaling_of_laplace[complete]
-
NaturalLatents.General.race_laplace_gain_scalar_concavity[complete]
-
NaturalLatents.General.race_unit_log_integrable[complete]
-
NaturalLatents.General.race_scalar_log_integrable_of_stable_laplace[complete]
-
NaturalLatents.General.race_logGain_zero[complete] -
NaturalLatents.General.race_logGain_nonneg[complete] -
NaturalLatents.General.race_gain_scaling_of_shifted_transform[complete] -
NaturalLatents.General.race_tailSum_laplace_of_shifted_transform[complete] -
NaturalLatents.General.race_expected_log_gain_scaling_of_laplace[complete] -
NaturalLatents.General.race_laplace_gain_scalar_concavity[complete] -
NaturalLatents.General.race_unit_log_integrable[complete] -
NaturalLatents.General.race_scalar_log_integrable_of_stable_laplace[complete]
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_logGain_zero (a : ℝ) (ha : a ≠ 0) : NaturalLatents.General.logGain a 0 = 0
theorem NaturalLatents.General.race_logGain_zero (a : ℝ) (ha : a ≠ 0) : NaturalLatents.General.logGain a 0 = 0
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_logGain_nonneg (a t : ℝ) (ht : 0 ≤ t) : 0 ≤ NaturalLatents.General.logGain a t
theorem NaturalLatents.General.race_logGain_nonneg (a t : ℝ) (ht : 0 ≤ t) : 0 ≤ NaturalLatents.General.logGain a t
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_gain_scaling_of_shifted_transform (a : ℝ) (ha : 1 < a) (t r : ℝ) (ht : 0 ≤ t) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * NaturalLatents.General.logGain a t ≤ NaturalLatents.General.logGain a (r * t)
theorem NaturalLatents.General.race_gain_scaling_of_shifted_transform (a : ℝ) (ha : 1 < a) (t r : ℝ) (ht : 0 ≤ t) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * NaturalLatents.General.logGain a t ≤ NaturalLatents.General.logGain a (r * t)
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_tailSum_laplace_of_shifted_transform (a : ℝ) (ha : 1 < a) (t : ℝ) : 0 ≤ t → ∀ (v : ℝ), 0 < v → ∫ (ω : ℕ → ℝ), Real.exp (-(v * NaturalLatents.General.tailSum a t ω)) ∂NaturalLatents.General.arrivalLaw = Real.exp (-(t * ∫ (u : ℝ) in Set.Ioi 0, 1 - Real.exp (-(v * (1 + u) ^ (-a)))))
theorem NaturalLatents.General.race_tailSum_laplace_of_shifted_transform (a : ℝ) (ha : 1 < a) (t : ℝ) : 0 ≤ t → ∀ (v : ℝ), 0 < v → ∫ (ω : ℕ → ℝ), Real.exp (-(v * NaturalLatents.General.tailSum a t ω)) ∂NaturalLatents.General.arrivalLaw = Real.exp (-(t * ∫ (u : ℝ) in Set.Ioi 0, 1 - Real.exp (-(v * (1 + u) ^ (-a)))))
The renewal transform implies a linear-in-t Laplace exponent for the scaled shifted tail tailSum. t=0 is handled directly from a>1.
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_expected_log_gain_scaling_of_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (V : ℝ → Ω → ℝ) (Φ : ℝ → ℝ) (hVm : ∀ (t : ℝ), 0 ≤ t → Measurable (V t)) (hVnn : ∀ (t : ℝ), 0 ≤ t → 0 ≤ᵐ[μ] V t) (hlog : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.Integrable (fun ω => Real.log (1 + V t ω)) μ) (hlap : ∀ (t : ℝ), 0 ≤ t → ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * V t ω)) ∂μ = Real.exp (-(t * Φ v))) (t r : ℝ) (ht : 0 ≤ t) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * ∫ (ω : Ω), Real.log (1 + V t ω) ∂μ ≤ ∫ (ω : Ω), Real.log (1 + V (r * t) ω) ∂μ
theorem NaturalLatents.General.race_expected_log_gain_scaling_of_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (V : ℝ → Ω → ℝ) (Φ : ℝ → ℝ) (hVm : ∀ (t : ℝ), 0 ≤ t → Measurable (V t)) (hVnn : ∀ (t : ℝ), 0 ≤ t → 0 ≤ᵐ[μ] V t) (hlog : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.Integrable (fun ω => Real.log (1 + V t ω)) μ) (hlap : ∀ (t : ℝ), 0 ≤ t → ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * V t ω)) ∂μ = Real.exp (-(t * Φ v))) (t r : ℝ) (ht : 0 ≤ t) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * ∫ (ω : Ω), Real.log (1 + V t ω) ∂μ ≤ ∫ (ω : Ω), Real.log (1 + V (r * t) ω) ∂μ
Sublinear clock scaling of expected log gain, assuming a linear Laplace exponent in clock intensity. No condition on Phi is necessary: nonnegativity of V already makes both kernels nonnegative.
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_laplace_gain_scalar_concavity (x r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * (1 - Real.exp (-x)) ≤ 1 - Real.exp (-(r * x))
theorem NaturalLatents.General.race_laplace_gain_scalar_concavity (x r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * (1 - Real.exp (-x)) ≤ 1 - Real.exp (-(r * x))
Scalar concavity of 1-exp(-x), valid for every real x.
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_unit_log_integrable (a : ℝ) (ha : 1 < a) : MeasureTheory.Integrable (fun z => Real.log (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2)))) (NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw)
theorem NaturalLatents.General.race_unit_log_integrable (a : ℝ) (ha : 1 < a) : MeasureTheory.Integrable (fun z => Real.log (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2)))) (NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw)
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_scalar_log_integrable_of_stable_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (hR : Measurable R) (hRpos : ∀ᵐ (ω : Ω) ∂μ, 0 < R ω) (alpha c : ℝ) (halpha : 0 < alpha) (hc : 0 < c) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(c * v ^ alpha))) : MeasureTheory.Integrable (fun ω => Real.log (R ω)) μ
theorem NaturalLatents.General.race_scalar_log_integrable_of_stable_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (hR : Measurable R) (hRpos : ∀ᵐ (ω : Ω) ∂μ, 0 < R ω) (alpha c : ℝ) (halpha : 0 < alpha) (hc : 0 < c) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(c * v ^ alpha))) : MeasureTheory.Integrable (fun ω => Real.log (R ω)) μ
Lean proves: m_a(0)=0, m_a(t)\ge0 for t\ge0, the scaling inequality (R11), and log-integrability of the unit appended mass and of positive measurable variables with the stated stable Laplace transform.
Use the Laplace functional and Frullani identity to obtain concavity; bound the positive and negative logarithmic parts separately. See the page section.
Lean: race_logGain_zero, race_logGain_nonneg and race_gain_scaling_of_shifted_transform (the scaling inequality (R11)), in
NaturalLatents/General/ExponentialRace.lean. The proof of (R11) uses race_tailSum_laplace_of_shifted_transform, which is (R13),
race_expected_log_gain_scaling_of_laplace, which is (R14) followed by the concavity step, and
race_laplace_gain_scalar_concavity. Lean states neither the upper bound m_a(t)\le t/(a-1) nor concavity of
m_a itself, only (R11). It obtains log-integrability from the stable Laplace transform rather than from (R15) and (R16):
race_unit_log_integrable (NaturalLatents/General/RaceLaplace.lean) applies
race_scalar_log_integrable_of_stable_laplace to the unit appended mass.
Lemma R7 (log mean from a Laplace transform). Let 0 < \alpha < 1, c > 0, and let R > 0 almost surely satisfy
\mathbb E\lvert\ln R\rvert < \infty and \mathbb Ee^{-vR} = e^{-cv^\alpha} for every v > 0. Then
\mathbb E\ln R=\frac{\ln c}{\alpha}
+\left(\frac1\alpha-1\right)\gamma_E.
\qquad \text{(R17)}
Lean code for Theorem4.3.4●2 theorems
Associated Lean declarations
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_scalar_log_mean_of_stable_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (hR : Measurable R) (hRpos : ∀ᵐ (ω : Ω) ∂μ, 0 < R ω) (hlogR : MeasureTheory.Integrable (fun ω => Real.log (R ω)) μ) (alpha c : ℝ) (halpha : 0 < alpha) (hc : 0 < c) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(c * v ^ alpha))) : ∫ (ω : Ω), Real.log (R ω) ∂μ = Real.log c / alpha + (1 / alpha - 1) * Real.eulerMascheroniConstant
theorem NaturalLatents.General.race_scalar_log_mean_of_stable_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (hR : Measurable R) (hRpos : ∀ᵐ (ω : Ω) ∂μ, 0 < R ω) (hlogR : MeasureTheory.Integrable (fun ω => Real.log (R ω)) μ) (alpha c : ℝ) (halpha : 0 < alpha) (hc : 0 < c) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(c * v ^ alpha))) : ∫ (ω : Ω), Real.log (R ω) ∂μ = Real.log c / alpha + (1 / alpha - 1) * Real.eulerMascheroniConstant
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_scalar_log_ratio_law_of_stable_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (hR : Measurable R) (hRpos : ∀ᵐ (ω : Ω) ∂μ, 0 < R ω) (alpha c : ℝ) (halpha : 0 < alpha) (hc : 0 < c) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(c * v ^ alpha))) : have ν := ProbabilityTheory.expMeasure 1; have H := fun z => Real.log z.2 - Real.log (R z.1); have K := fun t => (Real.log t - Real.log c) / alpha; MeasureTheory.Measure.map H (μ.prod ν) = MeasureTheory.Measure.map K ν
theorem NaturalLatents.General.race_scalar_log_ratio_law_of_stable_laplace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (hR : Measurable R) (hRpos : ∀ᵐ (ω : Ω) ∂μ, 0 < R ω) (alpha c : ℝ) (halpha : 0 < alpha) (hc : 0 < c) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(c * v ^ alpha))) : have ν := ProbabilityTheory.expMeasure 1; have H := fun z => Real.log z.2 - Real.log (R z.1); have K := fun t => (Real.log t - Real.log c) / alpha; MeasureTheory.Measure.map H (μ.prod ν) = MeasureTheory.Measure.map K ν
The stable Laplace transform of a positive random variable determines its logarithmic mean. Only `0 < alpha` is needed; the race uses `0 < alpha < 1`.
Apply Frullani, integrate by parts, change variables, and use Euler’s logarithmic integral with both boundary terms controlled. See the page section.
Lean: race_scalar_log_mean_of_stable_laplace (NaturalLatents/General/RaceLaplace.lean), which drops the
restriction \alpha<1 and keeps measurability, positivity and log-integrability of R, and c>0. Its proof differs from the page: race_scalar_log_ratio_law_of_stable_laplace shows that, for an
independent rate-one exponential variable E, the law of \ln E-\ln R is the law of (\ln E-\ln c)/\alpha,
and the mean follows from the logarithmic integral of (R6); neither (R5) nor integration by parts is used.
-
NaturalLatents.General.race_gamma_price[complete] -
NaturalLatents.General.race_unit_log_mean_eq_gammaPriceET[complete] -
NaturalLatents.General.race_unit_arrival_laplace[complete] -
NaturalLatents.General.race_gamma_price_of_unit_laplace[complete] -
NaturalLatents.General.race_superposition_pi_laplace[complete] -
NaturalLatents.General.race_superposition_clock_append_laplace[complete]
Lemma R8 (identification of the race price). Let a > 1, \alpha = 1/a, G = \Gamma(1-\alpha), and let
S_i, S, J_i be constructed from a strictly positive probability vector \pi and independent original and appended
exponential clocks as in (R8). With m_a from (R9),
\mathbb E\ln S=a\ln G+(a-1)\gamma_E,\qquad
\mathbb E\ln S_i-\mathbb E\ln J_i=j(a),\qquad
\mathbb E_{T\sim\mathrm{Exp}(1)}m_a(T)=j(a)\ge0.
\qquad \text{(R19)}
Lean code for Theorem4.3.5●6 theorems
Associated Lean declarations
-
NaturalLatents.General.race_gamma_price[complete]
-
NaturalLatents.General.race_unit_log_mean_eq_gammaPriceET[complete]
-
NaturalLatents.General.race_unit_arrival_laplace[complete]
-
NaturalLatents.General.race_gamma_price_of_unit_laplace[complete]
-
NaturalLatents.General.race_superposition_pi_laplace[complete]
-
NaturalLatents.General.race_superposition_clock_append_laplace[complete]
-
NaturalLatents.General.race_gamma_price[complete] -
NaturalLatents.General.race_unit_log_mean_eq_gammaPriceET[complete] -
NaturalLatents.General.race_unit_arrival_laplace[complete] -
NaturalLatents.General.race_gamma_price_of_unit_laplace[complete] -
NaturalLatents.General.race_superposition_pi_laplace[complete] -
NaturalLatents.General.race_superposition_clock_append_laplace[complete]
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_gamma_price (a : ℝ) (ha : 1 < a) : NaturalLatents.General.gammaPriceET a = NaturalLatents.General.gammaPrice a
theorem NaturalLatents.General.race_gamma_price (a : ℝ) (ha : 1 < a) : NaturalLatents.General.gammaPriceET a = NaturalLatents.General.gammaPrice a
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_unit_log_mean_eq_gammaPriceET (a : ℝ) (hInt : MeasureTheory.Integrable (fun z => Real.log (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2)))) (NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw)) : ∫ (z : ℝ × (ℕ → ℝ)), Real.log (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2))) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = a * Real.eulerMascheroniConstant + NaturalLatents.General.gammaPriceET a
theorem NaturalLatents.General.race_unit_log_mean_eq_gammaPriceET (a : ℝ) (hInt : MeasureTheory.Integrable (fun z => Real.log (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2)))) (NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw)) : ∫ (z : ℝ × (ℕ → ℝ)), Real.log (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2))) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = a * Real.eulerMascheroniConstant + NaturalLatents.General.gammaPriceET a
The logarithmic mean of the unit-prior appended mass is a*gamma+gammaPriceET. The only analytic hypothesis needed here is log integrability of that mass. The max extension is inactive on the proved a.e. nonnegative-increment event.
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_unit_arrival_laplace (a v : ℝ) (ha : 1 < a) (hv : 0 < v) : ∫ (z : ℝ × (ℕ → ℝ)), Real.exp (-(v * (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2))))) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = Real.exp (-(Real.Gamma (1 - 1 / a) * v ^ (1 / a)))
theorem NaturalLatents.General.race_unit_arrival_laplace (a v : ℝ) (ha : 1 < a) (hv : 0 < v) : ∫ (z : ℝ × (ℕ → ℝ)), Real.exp (-(v * (z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2))))) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = Real.exp (-(Real.Gamma (1 - 1 / a) * v ^ (1 / a)))
Final unit mass transform, once the actual head/tail transport helper is checked. This supplies the Laplace component of the old analytic primitive.
-
theoremdefined in NaturalLatents/General/RaceLaplace.leancomplete
theorem NaturalLatents.General.race_gamma_price_of_unit_laplace (a : ℝ) (ha : 1 < a) : have R := fun z => z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2)); Measurable R → MeasureTheory.Integrable (fun z => Real.log (R z)) (NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw) → (∀ (v : ℝ), 0 < v → ∫ (z : ℝ × (ℕ → ℝ)), Real.exp (-(v * R z)) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = Real.exp (-(Real.Gamma (1 - 1 / a) * v ^ (1 / a)))) → NaturalLatents.General.gammaPriceET a = NaturalLatents.General.gammaPrice a
theorem NaturalLatents.General.race_gamma_price_of_unit_laplace (a : ℝ) (ha : 1 < a) : have R := fun z => z.1 ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a z.1 z.2)); Measurable R → MeasureTheory.Integrable (fun z => Real.log (R z)) (NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw) → (∀ (v : ℝ), 0 < v → ∫ (z : ℝ × (ℕ → ℝ)), Real.exp (-(v * R z)) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = Real.exp (-(Real.Gamma (1 - 1 / a) * v ^ (1 / a)))) → NaturalLatents.General.gammaPriceET a = NaturalLatents.General.gammaPrice a
Explicit unit-arrivalTime stable Laplace and log-integrability inputs imply `gammaPriceET a = gammaPrice a`.
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_superposition_pi_laplace {κ Ω : Type} [Fintype κ] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (a : ℝ) (ha : 0 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (G : ℝ) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(G * v ^ (1 / a)))) (v : ℝ) (hv : 0 < v) : (∫ (ω : κ → Ω), Real.exp (-(v * ∑ i, π i ^ a * R (ω i))) ∂MeasureTheory.Measure.pi fun x => μ) = Real.exp (-(G * v ^ (1 / a)))
theorem NaturalLatents.General.race_superposition_pi_laplace {κ Ω : Type} [Fintype κ] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (R : Ω → ℝ) (a : ℝ) (ha : 0 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (G : ℝ) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (ω : Ω), Real.exp (-(v * R ω)) ∂μ = Real.exp (-(G * v ^ (1 / a)))) (v : ℝ) (hv : 0 < v) : (∫ (ω : κ → Ω), Real.exp (-(v * ∑ i, π i ^ a * R (ω i))) ∂MeasureTheory.Measure.pi fun x => μ) = Real.exp (-(G * v ^ (1 / a)))
Scaling each iid stable mass by π_i^a preserves its stable law when π is a PMF, because (π_i^a)^(1/a)=π_i.
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_superposition_clock_append_laplace {κ : Type} [Fintype κ] (R : ℝ × (ℕ → ℝ) → ℝ) (a : ℝ) (ha : 0 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (G : ℝ) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (w : ℝ × (ℕ → ℝ)), Real.exp (-(v * R w)) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = Real.exp (-(G * v ^ (1 / a)))) (v : ℝ) (hv : 0 < v) : ∫ (w : (κ → ℝ) × (κ → ℕ → ℝ)), Real.exp (-(v * ∑ i, π i ^ a * R (w.1 i, w.2 i))) ∂(stoch_to_det.clockLaw κ).prod (MeasureTheory.Measure.pi fun x => NaturalLatents.General.arrivalLaw) = Real.exp (-(G * v ^ (1 / a)))
theorem NaturalLatents.General.race_superposition_clock_append_laplace {κ : Type} [Fintype κ] (R : ℝ × (ℕ → ℝ) → ℝ) (a : ℝ) (ha : 0 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (G : ℝ) (hLaplace : ∀ (v : ℝ), 0 < v → ∫ (w : ℝ × (ℕ → ℝ)), Real.exp (-(v * R w)) ∂NaturalLatents.General.expOne.prod NaturalLatents.General.arrivalLaw = Real.exp (-(G * v ^ (1 / a)))) (v : ℝ) (hv : 0 < v) : ∫ (w : (κ → ℝ) × (κ → ℕ → ℝ)), Real.exp (-(v * ∑ i, π i ^ a * R (w.1 i, w.2 i))) ∂(stoch_to_det.clockLaw κ).prod (MeasureTheory.Measure.pi fun x => NaturalLatents.General.arrivalLaw) = Real.exp (-(G * v ^ (1 / a)))
Lean proves: \mathbb E_{T\sim\mathrm{Exp}(1)}m_a(T)=j(a) (the third identity of (R19)), the unit appended-mass log mean a\gamma_E+\mathrm{gammaPriceET}(a), and the unit and superposition Laplace transforms.
Evaluate the power-sum Laplace exponent, multiply the independent transforms, and subtract their log means. See the page section.
Lean: race_gamma_price (NaturalLatents/General/RaceLaplace.lean) states gammaPriceET a = gammaPrice a, the third identity of
(R19), where gammaPriceET (NaturalLatents/General/Definitions.lean) is \mathbb E_{T\sim\mathrm{Exp}(1)}m_a(T). It is proved through
race_unit_log_mean_eq_gammaPriceET (the log mean of one appended mass with \pi_i=1 is a\gamma_E plus gammaPriceET a),
race_unit_arrival_laplace (the Laplace transform (R21) of that mass) and race_gamma_price_of_unit_laplace. The
superposition step of (R21) is race_superposition_pi_laplace and race_superposition_clock_append_laplace
(NaturalLatents/General/ExponentialRace.lean). The other identities of (R19) appear only inside proofs.
Lemma R9 (rowwise reference loss, not a rowwise entropy bound). Let a > 1, let r, \pi be strictly positive
probability vectors on the same finite label set, and construct the winner W = \arg\min_i E_i/r_i and the
reference Q from (R8) using the same original clocks and independent appendages. Write \Omega for all appended
spacings. Then
\mathbb E_{E,\Omega}\left[-\ln Q_W\right]
\le aD(r\Vert\pi)+j(a)\left(1-\sum_i r_i^2\right).
\qquad \text{(R23)}
Lean code for Theorem4.3.6●3 theorems
Associated Lean declarations
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_reference_loss_bound {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (a : ℝ) (ha : 1 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hrpos : ∀ (i : κ), 0 < r i) : have ν := MeasureTheory.Measure.pi fun x => NaturalLatents.General.arrivalLaw; have ρ := (stoch_to_det.seedLaw κ).prod ν; have S := fun w i => π i ^ a * Real.exp (-w.1 i) ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a (Real.exp (-w.1 i)) (w.2 i))); have Q := fun w i => S w i / ∑ k, S w k; MeasureTheory.Integrable (fun w => Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1))) ρ ∧ ∫ (w : (κ → ℝ) × (κ → ℕ → ℝ)), Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1)) ∂ρ ≤ a * ∑ i, r i * Real.log (r i / π i) + NaturalLatents.General.gammaPrice a * (1 - ∑ i, r i ^ 2)
theorem NaturalLatents.General.race_reference_loss_bound {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (a : ℝ) (ha : 1 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hrpos : ∀ (i : κ), 0 < r i) : have ν := MeasureTheory.Measure.pi fun x => NaturalLatents.General.arrivalLaw; have ρ := (stoch_to_det.seedLaw κ).prod ν; have S := fun w i => π i ^ a * Real.exp (-w.1 i) ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a (Real.exp (-w.1 i)) (w.2 i))); have Q := fun w i => S w i / ∑ k, S w k; MeasureTheory.Integrable (fun w => Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1))) ρ ∧ ∫ (w : (κ → ℝ) × (κ → ℕ → ℝ)), Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1)) ∂ρ ≤ a * ∑ i, r i * Real.log (r i / π i) + NaturalLatents.General.gammaPrice a * (1 - ∑ i, r i ^ 2)
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_appended_logloss_of_unit_laplace {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (a : ℝ) (ha : 1 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hrpos : ∀ (i : κ), 0 < r i) : have ν := MeasureTheory.Measure.pi fun x => NaturalLatents.General.arrivalLaw; have ρ := (stoch_to_det.seedLaw κ).prod ν; have S := fun w i => π i ^ a * Real.exp (-w.1 i) ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a (Real.exp (-w.1 i)) (w.2 i))); have Q := fun w i => S w i / ∑ k, S w k; MeasureTheory.Integrable (fun w => Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1))) ρ ∧ ∫ (w : (κ → ℝ) × (κ → ℕ → ℝ)), Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1)) ∂ρ = a * ∑ i, r i * Real.log (r i / π i) + NaturalLatents.General.gammaPriceET a - ∑ i, r i * ∫ (t : ℝ), NaturalLatents.General.logGain a (r i * t) ∂NaturalLatents.General.expOne
theorem NaturalLatents.General.race_appended_logloss_of_unit_laplace {κ : Type} [Fintype κ] [DecidableEq κ] [Nonempty κ] (a : ℝ) (ha : 1 < a) (π : κ → ℝ) (hπ : stoch_to_det.IsPMF π) (hπpos : ∀ (i : κ), 0 < π i) (r : κ → ℝ) (hr : stoch_to_det.IsPMF r) (hrpos : ∀ (i : κ), 0 < r i) : have ν := MeasureTheory.Measure.pi fun x => NaturalLatents.General.arrivalLaw; have ρ := (stoch_to_det.seedLaw κ).prod ν; have S := fun w i => π i ^ a * Real.exp (-w.1 i) ^ (-a) * (1 + max 0 (NaturalLatents.General.tailSum a (Real.exp (-w.1 i)) (w.2 i))); have Q := fun w i => S w i / ∑ k, S w k; MeasureTheory.Integrable (fun w => Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1))) ρ ∧ ∫ (w : (κ → ℝ) × (κ → ℕ → ℝ)), Real.log (1 / Q w (stoch_to_det.SharedRace.weightedLexWinner r w.1)) ∂ρ = a * ∑ i, r i * Real.log (r i / π i) + NaturalLatents.General.gammaPriceET a - ∑ i, r i * ∫ (t : ℝ), NaturalLatents.General.logGain a (r i * t) ∂NaturalLatents.General.expOne
The exponential/Gumbel map transports the proved clock loss to the original-seed expression, including the exact lexicographic winner.
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_gain_average (a : ℝ) (ha : 1 < a) (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * NaturalLatents.General.gammaPrice a ≤ ∫ (t : ℝ), NaturalLatents.General.logGain a (r * t) ∂NaturalLatents.General.expOne
theorem NaturalLatents.General.race_gain_average (a : ℝ) (ha : 1 < a) (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : r * NaturalLatents.General.gammaPrice a ≤ ∫ (t : ℝ), NaturalLatents.General.logGain a (r * t) ∂NaturalLatents.General.expOne
Condition on the winning clock, subtract the selected log mass from the total log mass, and apply concave gain scaling. See the page section.
Lean: race_reference_loss_bound (NaturalLatents/General/ExponentialRace.lean) states the integrability and (R23), with the
clocks in Gumbel coordinates. The exact identity of (R24), with the price written gammaPriceET a, is
race_appended_logloss_of_unit_laplace, and the scaling step is race_gain_average, which states
r\,j(a)\le\mathbb E\,m_a(rT) for 0\le r\le1, both in the same file.
Lemma R10 (fixed-seed mixture entropy). Let \mathcal Z, \mathcal I be finite nonempty sets, \nu a probability
law positive on \mathcal Z (here \nu is the source law; in Lemma R11 it is p), and r_z strictly positive probability rows on \mathcal I. Put
\pi_i = \sum_z\nu(z)r_z(i), let Z \sim \nu, and let L \mid Z = z \sim r_z. For a > 1, take original
independent exponential clocks E, independent of Z, and define A_E(z) = \arg\min_iE_i/r_z(i). Then
H(A_E(Z)\mid E)=\mathbb E_E H(\mu_E)
\le aI(Z;L)+j(a)\sum_z\nu(z)\left(1-\sum_i r_z(i)^2\right),
\quad
\mu_e(i)=\sum_z\nu(z)\mathbf 1_{\{A_e(z)=i\}}.
\qquad \text{(R25)}
Lean code for Theorem4.3.7●4 theorems
Associated Lean declarations
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.race_single_law {Ω κ : Type} [Fintype Ω] [Fintype κ] [DecidableEq Ω] [DecidableEq κ] [Nonempty κ] (a : ℝ) (ha : 1 < a) {μ : Ω → ℝ} {r : Ω → κ → ℝ} (hμ : stoch_to_det.IsPMF μ) (hr : ∀ (z : Ω), μ z ≠ 0 → stoch_to_det.IsPMF (r z)) (hrpos : ∀ (z : Ω), μ z ≠ 0 → ∀ (i : κ), 0 < r z i) : NaturalLatents.General.sharedRaceEntropyNat μ r ≤ a * NaturalLatents.General.MINat Prod.fst Prod.snd (stoch_to_det.SharedRace.posteriorJoint μ r) + NaturalLatents.General.gammaPrice a * stoch_to_det.SharedRace.categoricalMismatch μ r
theorem NaturalLatents.General.race_single_law {Ω κ : Type} [Fintype Ω] [Fintype κ] [DecidableEq Ω] [DecidableEq κ] [Nonempty κ] (a : ℝ) (ha : 1 < a) {μ : Ω → ℝ} {r : Ω → κ → ℝ} (hμ : stoch_to_det.IsPMF μ) (hr : ∀ (z : Ω), μ z ≠ 0 → stoch_to_det.IsPMF (r z)) (hrpos : ∀ (z : Ω), μ z ≠ 0 → ∀ (i : κ), 0 < r z i) : NaturalLatents.General.sharedRaceEntropyNat μ r ≤ a * NaturalLatents.General.MINat Prod.fst Prod.snd (stoch_to_det.SharedRace.posteriorJoint μ r) + NaturalLatents.General.gammaPrice a * stoch_to_det.SharedRace.categoricalMismatch μ r
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_gibbs_nats {Ω κ : Type} [Fintype Ω] [Fintype κ] [DecidableEq κ] {μ : Ω → ℝ} (hμ : stoch_to_det.IsPMF μ) (A : Ω → κ) {q : κ → ℝ} (hq : stoch_to_det.IsPMF q) (hqpos : ∀ (i : κ), 0 < q i) : NaturalLatents.General.HNat (stoch_to_det.push A μ) ≤ ∑ z, μ z * Real.log (1 / q (A z))
theorem NaturalLatents.General.race_gibbs_nats {Ω κ : Type} [Fintype Ω] [Fintype κ] [DecidableEq κ] {μ : Ω → ℝ} (hμ : stoch_to_det.IsPMF μ) (A : Ω → κ) {q : κ → ℝ} (hq : stoch_to_det.IsPMF q) (hqpos : ∀ (i : κ), 0 < q i) : NaturalLatents.General.HNat (stoch_to_det.push A μ) ≤ ∑ z, μ z * Real.log (1 / q (A z))
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_entropy_from_reference {Ω κ Ξ : Type} [Fintype Ω] [Fintype κ] [DecidableEq Ω] [DecidableEq κ] [Nonempty κ] [MeasurableSpace Ξ] (ν : MeasureTheory.Measure Ξ) [MeasureTheory.IsProbabilityMeasure ν] (a c : ℝ) {μ : Ω → ℝ} {r : Ω → κ → ℝ} (hμ : stoch_to_det.IsPMF μ) (hr : ∀ (z : Ω), μ z ≠ 0 → stoch_to_det.IsPMF (r z)) (hrpos : ∀ (z : Ω), μ z ≠ 0 → ∀ (i : κ), 0 < r z i) (Q : (κ → ℝ) × Ξ → κ → ℝ) (hQ : ∀ᵐ (w : (κ → ℝ) × Ξ) ∂(stoch_to_det.seedLaw κ).prod ν, stoch_to_det.IsPMF (Q w) ∧ ∀ (i : κ), 0 < Q w i) (hInt : ∀ (z : Ω), μ z ≠ 0 → MeasureTheory.Integrable (fun w => Real.log (1 / Q w (stoch_to_det.SharedRace.sharedWinner r w.1 z))) ((stoch_to_det.seedLaw κ).prod ν)) (hLoss : ∀ (z : Ω), μ z ≠ 0 → ∫ (w : (κ → ℝ) × Ξ), Real.log (1 / Q w (stoch_to_det.SharedRace.sharedWinner r w.1 z)) ∂(stoch_to_det.seedLaw κ).prod ν ≤ a * ∑ i, r z i * Real.log (r z i / stoch_to_det.SharedRace.posteriorMean μ r i) + c * (1 - ∑ i, r z i ^ 2)) : NaturalLatents.General.sharedRaceEntropyNat μ r ≤ a * NaturalLatents.General.MINat Prod.fst Prod.snd (stoch_to_det.SharedRace.posteriorJoint μ r) + c * stoch_to_det.SharedRace.categoricalMismatch μ r
theorem NaturalLatents.General.race_entropy_from_reference {Ω κ Ξ : Type} [Fintype Ω] [Fintype κ] [DecidableEq Ω] [DecidableEq κ] [Nonempty κ] [MeasurableSpace Ξ] (ν : MeasureTheory.Measure Ξ) [MeasureTheory.IsProbabilityMeasure ν] (a c : ℝ) {μ : Ω → ℝ} {r : Ω → κ → ℝ} (hμ : stoch_to_det.IsPMF μ) (hr : ∀ (z : Ω), μ z ≠ 0 → stoch_to_det.IsPMF (r z)) (hrpos : ∀ (z : Ω), μ z ≠ 0 → ∀ (i : κ), 0 < r z i) (Q : (κ → ℝ) × Ξ → κ → ℝ) (hQ : ∀ᵐ (w : (κ → ℝ) × Ξ) ∂(stoch_to_det.seedLaw κ).prod ν, stoch_to_det.IsPMF (Q w) ∧ ∀ (i : κ), 0 < Q w i) (hInt : ∀ (z : Ω), μ z ≠ 0 → MeasureTheory.Integrable (fun w => Real.log (1 / Q w (stoch_to_det.SharedRace.sharedWinner r w.1 z))) ((stoch_to_det.seedLaw κ).prod ν)) (hLoss : ∀ (z : Ω), μ z ≠ 0 → ∫ (w : (κ → ℝ) × Ξ), Real.log (1 / Q w (stoch_to_det.SharedRace.sharedWinner r w.1 z)) ∂(stoch_to_det.seedLaw κ).prod ν ≤ a * ∑ i, r z i * Real.log (r z i / stoch_to_det.SharedRace.posteriorMean μ r i) + c * (1 - ∑ i, r z i ^ 2)) : NaturalLatents.General.sharedRaceEntropyNat μ r ≤ a * NaturalLatents.General.MINat Prod.fst Prod.snd (stoch_to_det.SharedRace.posteriorJoint μ r) + c * stoch_to_det.SharedRace.categoricalMismatch μ r
Fixed-seed Gibbs and finite source averaging; the auxiliary seed changes only the reference.
Apply Gibbs inequality to the actual fixed-seed source image and average the rowwise reference losses. See the page section.
Lean: race_single_law (NaturalLatents/General/ExponentialRace.lean) states (R25) for a probability law \nu with strictly
positive rows wherever \nu(z)>0, so \nu may vanish at some atoms; like exists_race it is stated in nats, through
sharedRaceEntropyNat and MINat (NaturalLatents/General/Nats.lean). The Gibbs step (R26) is race_gibbs_nats and the averaging (R27) is
race_entropy_from_reference, both in NaturalLatents/General/RaceTransport.lean, with the integrability of the
fixed-seed entropy from stoch_to_det.SharedRace.integrable_sharedWinner_code (from pull request #6 by Jeremy Gillen)
(NaturalLatents/Upstream/CoordinateRace.lean).
-
NaturalLatents.General.exists_race[complete] -
NaturalLatents.General.race_of_single_law[complete] -
NaturalLatents.General.race_map_calibrated[complete] -
stoch_to_det.SharedRace.conditional_entropy_le_of_uniform_entropy_bound[complete] -
NaturalLatents.General.race_condMI_transport[complete] -
NaturalLatents.General.race_condMI_coordinate_sum[complete]
Lemma R11 (the race bound, with the original clocks on both fibers). Let X, Y, L be finite random variables, let
Z = (X,Y), write p(z)=\Pr(Z=z), and suppose r_z(i) = \Pr(L = i \mid Z = z) > 0 for every z with
p(z) > 0; then \pi_i = \Pr(L = i) = \sum_zp(z)r_z(i) > 0, since the support of p is nonempty. Let
a > 1, let E_i be independent rate-one exponential clocks independent of (X,Y,L), and put A_E(z) = \arg\min_iE_i/r_z(i). With B, d, h, j(a) exactly as in section 1, this
calibrated family satisfies
h\le aB+2j(a)d.
\qquad \text{(R28)}
It also induces a finite-valued random deterministic map F = (A_E(z))_{z\in\mathrm{supp}\,p}, independent of Z,
with the same calibration and the same h.
Lean code for Theorem4.3.8●6 theorems
Associated Lean declarations
-
NaturalLatents.General.exists_race[complete]
-
NaturalLatents.General.race_of_single_law[complete]
-
NaturalLatents.General.race_map_calibrated[complete]
-
stoch_to_det.SharedRace.conditional_entropy_le_of_uniform_entropy_bound[complete]
-
NaturalLatents.General.race_condMI_transport[complete]
-
NaturalLatents.General.race_condMI_coordinate_sum[complete]
-
NaturalLatents.General.exists_race[complete] -
NaturalLatents.General.race_of_single_law[complete] -
NaturalLatents.General.race_map_calibrated[complete] -
stoch_to_det.SharedRace.conditional_entropy_le_of_uniform_entropy_bound[complete] -
NaturalLatents.General.race_condMI_transport[complete] -
NaturalLatents.General.race_condMI_coordinate_sum[complete]
-
theoremdefined in NaturalLatents/General/ExponentialRace.leancomplete
theorem NaturalLatents.General.exists_race {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) (a : ℝ) (ha : 1 < a) : ∃ F, NaturalLatents.General.seedEntropy F ≤ a * NaturalLatents.General.redundancy L + 2 * NaturalLatents.General.gammaPrice a * NaturalLatents.General.mismatch L
theorem NaturalLatents.General.exists_race {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) (a : ℝ) (ha : 1 < a) : ∃ F, NaturalLatents.General.seedEntropy F ≤ a * NaturalLatents.General.redundancy L + 2 * NaturalLatents.General.gammaPrice a * NaturalLatents.General.mismatch L
The exponential race: for `a > 1`, a latent with positive prior and positive posterior rows has a calibrated seeded family `F` with `seedEntropy F ≤ a * redundancy L + 2 * gammaPrice a * mismatch L`.
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_of_single_law {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) (a b : ℝ) (hsingle : ∀ (μ : X × Y → ℝ) (r : X × Y → L.ι → ℝ), stoch_to_det.IsPMF μ → (∀ (z : X × Y), μ z ≠ 0 → stoch_to_det.IsPMF (r z)) → (∀ (z : X × Y), μ z ≠ 0 → ∀ (i : L.ι), 0 < r z i) → NaturalLatents.General.sharedRaceEntropyNat μ r ≤ a * NaturalLatents.General.MINat Prod.fst Prod.snd (stoch_to_det.SharedRace.posteriorJoint μ r) + b * stoch_to_det.SharedRace.categoricalMismatch μ r) : ∃ F, NaturalLatents.General.seedEntropy F ≤ a * NaturalLatents.General.redundancy L + 2 * b * NaturalLatents.General.mismatch L
theorem NaturalLatents.General.race_of_single_law {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) (a b : ℝ) (hsingle : ∀ (μ : X × Y → ℝ) (r : X × Y → L.ι → ℝ), stoch_to_det.IsPMF μ → (∀ (z : X × Y), μ z ≠ 0 → stoch_to_det.IsPMF (r z)) → (∀ (z : X × Y), μ z ≠ 0 → ∀ (i : L.ι), 0 < r z i) → NaturalLatents.General.sharedRaceEntropyNat μ r ≤ a * NaturalLatents.General.MINat Prod.fst Prod.snd (stoch_to_det.SharedRace.posteriorJoint μ r) + b * stoch_to_det.SharedRace.categoricalMismatch μ r) : ∃ F, NaturalLatents.General.seedEntropy F ≤ a * NaturalLatents.General.redundancy L + 2 * b * NaturalLatents.General.mismatch L
The complete-map and coordinate transport needs only the single-law analytic comparison.
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_map_calibrated {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) : ∃ F, F.seedLaw = fun A => ∫ (G : L.ι → ℝ), if stoch_to_det.SharedRace.sharedWinner (fun z i => NaturalLatents.General.posterior L i z) G = A then 1 else 0 ∂stoch_to_det.seedLaw L.ι
theorem NaturalLatents.General.race_map_calibrated {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (hrows : ∀ z ∈ stoch_to_det.support p, ∀ (i : L.ι), 0 < NaturalLatents.General.posterior L i z) : ∃ F, F.seedLaw = fun A => ∫ (G : L.ι → ℝ), if stoch_to_det.SharedRace.sharedWinner (fun z i => NaturalLatents.General.posterior L i z) G = A then 1 else 0 ∂stoch_to_det.seedLaw L.ι
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_condMI_transport {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (L : stoch_to_det.Latent p) {Γ : Type} [Fintype Γ] [DecidableEq Γ] (g : X × Y → Γ) : stoch_to_det.condMI Prod.fst Prod.snd (fun zi => g zi.1) (stoch_to_det.SharedRace.posteriorJoint p fun z i => NaturalLatents.General.posterior L i z) = stoch_to_det.condMI Prod.fst Prod.snd (fun lz => g lz.2) L.joint
theorem NaturalLatents.General.race_condMI_transport {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (L : stoch_to_det.Latent p) {Γ : Type} [Fintype Γ] [DecidableEq Γ] (g : X × Y → Γ) : stoch_to_det.condMI Prod.fst Prod.snd (fun zi => g zi.1) (stoch_to_det.SharedRace.posteriorJoint p fun z i => NaturalLatents.General.posterior L i z) = stoch_to_det.condMI Prod.fst Prod.snd (fun lz => g lz.2) L.joint
-
theoremdefined in NaturalLatents/General/RaceTransport.leancomplete
theorem NaturalLatents.General.race_condMI_coordinate_sum {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (L : stoch_to_det.Latent p) : NaturalLatents.General.nats (stoch_to_det.condMI Prod.fst Prod.snd (fun lz => lz.2.1) L.joint + stoch_to_det.condMI Prod.fst Prod.snd (fun lz => lz.2.2) L.joint) = NaturalLatents.General.redundancy L
theorem NaturalLatents.General.race_condMI_coordinate_sum {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {p : NaturalLatents.General.Law X Y} (L : stoch_to_det.Latent p) : NaturalLatents.General.nats (stoch_to_det.condMI Prod.fst Prod.snd (fun lz => lz.2.1) L.joint + stoch_to_det.condMI Prod.fst Prod.snd (fun lz => lz.2.2) L.joint) = NaturalLatents.General.redundancy L
Lean proves: there exists a finite map-valued CalibratedSeededFamily with h\le aB+2j(a)d, and separately identifies the law of a calibrated map-valued seed as the pushforward of the shared Gumbel winner.
Apply the single-source entropy estimate on both coordinate fibers with the same clocks, then pass to the finite map-valued seed. See the page section.
Lean: exists_race (NaturalLatents/General/ExponentialRace.lean): for every finite latent L of a law p whose posterior rows
posterior L i z are positive on the support, and every a>1, there is a CalibratedSeededFamily L with
h\le aB+2j(a)d. It states existence only: that the
family is the race map with the original clocks on both fibers is in the proof, not in the statement. The proof is
race_of_single_law (NaturalLatents/General/RaceTransport.lean), which takes the family from race_map_calibrated,
conditions Lemma R10 on X and on Y through stoch_to_det.SharedRace.conditional_entropy_le_of_uniform_entropy_bound (from pull request #6 by Jeremy Gillen)
(NaturalLatents/Upstream/CoordinateRace.lean), and identifies the two conditional mutual informations with B by
race_condMI_transport and race_condMI_coordinate_sum.
The race inequality (R28) retains the exact price j(a); a separate cap page supplies the explicit
bound on j(a) for every a>1 (racePrice_lt_capC3b, NaturalLatents/General/Cap.lean) that the assembly uses at
a=211/45.