Samplinglib mathematical lesson

Actual countable unit-exponential product inputs

AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws · theorem · Teaching coverage

Read this first

Mathematical statement

Equip Ω=ℝ^ℕ with its canonical product measurable structure. Let μ=Exp(1) be the unit-rate exponential Borel measure on ℝ, define the actual countable product P=⊗_(k∈ℕ)μ, and define X_k(ω)=ω_k and ε_k(ω)=max{X_k(ω),0}, with ε_k regarded as a nonnegative real. There are no public mathematical premises. Then: (1) P is a probability measure; (2) for every k∈ℕ, X_k and ε_k are measurable and the real-coordinate pushforward (X_k)_#P equals μ exactly; (3) the entire real coordinate family (X_k) is mutually independent under P; (4) for P-almost every ω, simultaneously for every k, X_k(ω)>0 and the real coercion of ε_k(ω) equals X_k(ω); (5) for P-almost every ω, ∑_(k=0)^(n−1)ε_k(ω)→+∞ in ℝ as n→∞. The two almost-sure clauses may be intersected when used together. The sum at n=0 is zero. The carrier contains negative and zero coordinates, so positivity and clamp agreement are not universal pathwise claims. Source E_(k+1) is represented by X_k, and the actual waiting-time API may use ε_k on the simultaneous full-measure event. Explicit marginal and independence conjuncts concern X, not separately exported ε laws. This supplies the stochastic numerator background for AppendixA.1 Ex9; it does not assert an actual event-time comparison, nonaccumulation, global process, Markov property, invariant law, sampler error or expected query cost.

\[\Omega=\mathbb R^{\mathbb N},\quad P=\bigotimes_{k\in\mathbb N}\mathrm{Exp}(1),\quad X_k(\omega)=\omega_k,\quad\varepsilon_k(\omega)=\max\{X_k(\omega),0\}.\quad P(\Omega)=1,\quad(X_k)_\#P=\mathrm{Exp}(1),\quad(X_k)_{k\in\mathbb N}\text{ mutually independent}.\quad P\!\left(\forall k:\ X_k>0,\ \varepsilon_k=X_k\right)=1,\qquad\sum_{k=0}^{n-1}\varepsilon_k\xrightarrow[n\to\infty]{P\text{-a.s.}}+\infty.\]

Lean statement · unit_exponential_product_laws

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem unit_exponential_product_laws : unit_exponential_product_statement

Exact module and namespace context

Full Lean proposition (definition) · unit_exponential_product_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

Download module (.lean)

private def unit_exponential_product_statement : Prop :=
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let X : ℕ → (ℕ → ℝ) → ℝ := fun k ω => ω k
  let ε : ℕ → (ℕ → ℝ) → ℝ≥0 := fun k ω => Real.toNNReal (X k ω)
  IsProbabilityMeasure P ∧
  (∀ k : ℕ, Measurable (X k) ∧ Measurable (ε k) ∧
    Measure.map (X k) P = expMeasure (1 : ℝ)) ∧
  iIndepFun X P ∧
  (∀ᵐ ω ∂P, ∀ k : ℕ, 0 < X k ω ∧ (ε k ω : ℝ) = X k ω) ∧
  (∀ᵐ ω ∂P, Tendsto (fun n : ℕ => ∑ k ∈ Finset.range n, (ε k ω : ℝ))
    atTop atTop)

Exact module and namespace context

Proof roadmap

1Fix the actual product and threshold representatives
Use the canonical countable product of rate-one exponential measures on all real sequences. Coordinates are evaluations; ε is the total nonnegative truncation. Unfold the sealed five-clause proposition with these exact definitions. Probability, iid and good-event facts are conclusions to prove, not inputs.
2Construct probability, measurable coordinates and exact iid laws
The positive-rate exponential theorem makes every factor a probability measure, so the canonical infinite product is a probability measure. Coordinate evaluation is measurable and has exactly the factor pushforward law; composition with Real.toNNReal is measurable. Apply the actual infinite-product independence theorem to identity coordinate maps.
3Prove one simultaneous positive and faithful threshold event
The exponential CDF gives μ((−∞,0])=0. Pull this null event back by each coordinate law, then use countability to obtain a single full-measure event on which all coordinates are strictly positive. On that event max(X_k,0)=X_k, so the total NNReal threshold is faithful to the source clock.
4Build bounded iid indicators as an ASTIS sufficient OR-route
Define b(x)=1_{x>1} and B_k=b(X_k). Its measurability follows from the Borel half-line; integrability follows because it is an indicator of the integrable constant1 on a probability space. Measurable coordinate transforms preserve mutual independence and common law. This supplements the author route without asserting that the paper used indicators.
5Compute the positive indicator mean from the actual exponential tail
At1 the exponential CDF gives μ((1,∞))=1−F(1)=e^(−1). Push the integral of b through the exact coordinate marginal and integrate the indicator of this half-line. Thus E_P[B_0]=e^(−1)>0. No Exp first-moment calculation is supplied or assumed.
6Apply the real strong law to the proved integrable iid indicators
Invoke the pinned real strong law with the internal integrability proof, pairwise independence obtained from mutual independence, and the internally derived identical distributions. Substitute the exact mean. The sample averages converge almost surely to e^(−1).
7Deduce actual threshold-sum divergence and assemble all five clauses
Multiply the positive limiting average by n→∞ to obtain divergence of ∑B_k; handle n=0 separately when cancelling real division. For every real coordinate, B_k≤max(X_k,0)=ε_k: above1 use X_k>1, and otherwise B_k=0≤ε_k. Finite-sum domination therefore gives ∑ε_k→∞ on the strong-law event, even without restricting exceptional samples in the comparison. Combine the probability, marginal/measurability, independence, simultaneous good-event and divergence results.

Full assumptions and notation

All objects and hypotheses

Fixed carrier Ω=ℕ→ℝ, with the canonical product measurable space; ℝ and ℝ≥0 carry their canonical Borel measurable spaces. No dimension, potential, rate-cap, initialization, probability certificate, iid witness, integrability or convergence hypothesis is supplied.
The common rate is exactly1. The product, raw coordinate evaluations and total nonnegative clamp are literal definitions, with probability, measurable laws, independence and AE support proved internally.
Source E_(k+1) corresponds to X_k; range n contains exactly the first n clocks. Clamp/raw equality and positivity hold simultaneously for every k on a full-measure event, and may fail on exceptional samples.
The implementation proves divergence by the separately identified ASTIS bounded-indicator SLLN route: B_k=1_{X_k>1}, E[B_k]=exp(−1)>0 and B_k≤ε_k. The author direct Exp integrability/mean-one strong-law route is retained as an OPEN alternative source-background expansion.

Mathematical proof

1. Fix the actual product and threshold representatives

Use the canonical countable product of rate-one exponential measures on all real sequences. Coordinates are evaluations; ε is the total nonnegative truncation. Unfold the sealed five-clause proposition with these exact definitions. Probability, iid and good-event facts are conclusions to prove, not inputs.

\[\Omega=\mathbb R^{\mathbb N},\quad P=\bigotimes_{k\in\mathbb N}\mathrm{Exp}(1),\quad X_k(\omega)=\omega_k,\quad\varepsilon_k(\omega)=\max\{X_k(\omega),0\}.\]

Corresponding Lean step

  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let X : ℕ → (ℕ → ℝ) → ℝ := fun k ω => ω k
  let ε : ℕ → (ℕ → ℝ) → ℝ≥0 := fun k ω => Real.toNNReal (X k ω)
  change IsProbabilityMeasure P ∧
    (∀ k : ℕ, Measurable (X k) ∧ Measurable (ε k) ∧
      Measure.map (X k) P = expMeasure (1 : ℝ)) ∧
    iIndepFun X P ∧
    (∀ᵐ ω ∂P, ∀ k : ℕ, 0 < X k ω ∧ (ε k ω : ℝ) = X k ω) ∧
    (∀ᵐ ω ∂P, Tendsto (fun n : ℕ => ∑ k ∈ Finset.range n, (ε k ω : ℝ))
      atTop atTop)