Actual Marked Counts and Poisson Events

Abstract

Theorem 1.1 (Forward count tails).

$\forall M, q, s, k : N a t, \forall r : R e a l, \forall S : Support (M, q), \forall m : Fin (k) \to Fin (M), 1 \leq q \land q < M \land 0 < r \land r < 1 \land compensation (M, q, r) < 1 \land injective (m) \land (k = 1 \lor k = 2) \land 64 \leq M \land \frac{s}{M ^{2}} \leq \frac{1}{256} \Rightarrow \forall e : Experiment (), \forall B : N a t, forwardTotalTail (r, S, m, s, e, B) + directionalPoissonTotalTail (r, S, m, \frac{s}{( 2 ) \cdot ( M )}, B) \leq \frac{( 3 ) \cdot ( exp (( k ) \cdot ( \frac{s}{( 2 ) \cdot ( M )} )))}{2 ^{B}}$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_forward_marked_count_tail (✓ std3). ∎

Source. Repository-derived.

Commentary.

The forward actual total-count tail plus the genuine product-Poisson tail at rates L(1+b(m(j)))/2 and L(1-b(m(j)))/2 is at most 3 exp(kL)/2^B. Both experiments share the same support and arbitrary integer s. The assumptions are M>=64, 1<=q<M, 0<r<1, compensation<1, distinct one or two marks, and s/M^2<=1/256.

Theorem 1.2 (Forward count events).

$\forall ka pp a, C zero : R e a l, 0 < ka pp a \land ka pp a < 1 \land 1 \leq C zero \Rightarrow \exists A : R e a l, \exists M zero : N a t, \exists e t a zero : R e a l, 0 < A \land 64 \leq M zero \land 0 < e t a zero \land \forall M, q, s, k : N a t, \forall r : R e a l, \forall S : Support (M, q), \forall m : Fin (k) \to Fin (M), 1 \leq q \land q < M \land 0 < r \land r \leq 1 - ka pp a \land compensation (M, q, r) \leq 1 - ka pp a \land injective (m) \land (k = 1 \lor k = 2) \land M zero \leq M \land 1 \leq \frac{s}{( 2 ) \cdot ( M )} \land \frac{\frac{s}{( 2 ) \cdot ( M )}}{M} \leq e t a zero \Rightarrow \forall e : Experiment (), \forall B : N a t, B \leq (C zero) \cdot (\frac{s}{( 2 ) \cdot ( M )}) \Rightarrow \forall E : Set (Sum (Fin (k), Fin (k)) \to N a t), ∣ forwardEvent (r, S, m, s, e, E) - directionalPoissonEvent (r, S, m, \frac{s}{( 2 ) \cdot ( M )}, E)∣ \leq (\frac{( A ) \cdot ( \frac{s}{( 2 ) \cdot ( M )} ^{k + 1} )}{M}) \cdot (directionalPoissonEvent (r, S, m, \frac{s}{( 2 ) \cdot ( M )}, E)) + \frac{( 3 ) \cdot ( exp (( k ) \cdot ( \frac{s}{( 2 ) \cdot ( M )} )))}{2 ^{B}}$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_forward_marked_every_event (✓ std3). ∎

Source. Repository-derived.

Commentary.

For fixed 0<kappa<1 and Czero>=1, choose constants A>0, Mzero>=64 and etazero>0 before the support, marks, experiment, tuple cutoff and event. Assume r<=1-kappa and compensation<=1-kappa. The scale L=s/(2M) is real, L>=1 and L/M<=etazero. The same fixed support defines both actual history mass and directional exact Poisson rates. Every count event has absolute discrepancy at most A L^(k+1)/M times its comparison mass plus 3 exp(kL)/2^B, whenever B<=Czero L.

Definition 1.3 (poissonProduct).

$\forall i o t a : T y p e, [Fintype (i o t a)] \forall m u : i o t a \to NonnegativeReal (), poissonProduct (m u) = productPoissonMeasures (m u)$

Formalization. D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.poissonProduct (✓ std3).

Source. Repository-derived.

Commentary.

For a finite coordinate type iota and nonnegative rates mu, poissonProduct(mu) is the product of the genuine Poisson probability measures on the natural numbers. It contains all count tuples, without truncation.

Theorem 1.4 (product poisson tail).

$\forall i o t a : T y p e, [Fintype (i o t a)] \forall m u : i o t a \to NonnegativeReal (), \forall B : N a t, productPoissonTotalTail (m u, B) \leq \frac{exp ( sum ( m u ))}{2 ^{B}}$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.product_poisson_tail (✓ std3). ∎

Source. Repository-derived.

Commentary.

The total-count tail is at most exp(sum_i mu(i))/2^B for every natural B, including zero rates. The proof evaluates the coordinate exponential series at tilt 2, forms the product integral and applies Markov inequality.

Theorem 1.5 (actual reverse marked count tail).

$\forall M, q, s, k : N a t, \forall r : R e a l, \forall S : Support (M, q), \forall m : Fin (k) \to Fin (M), 1 \leq q \land q < M \land 0 < r \land r < 1 \land compensation (M, q, r) < 1 \land injective (m) \land (k = 1 \lor k = 2) \land 64 \leq M \land \frac{s}{M ^{2}} \leq \frac{1}{256} \Rightarrow \forall e : Experiment (), \forall B : N a t, reverseTotalTail (r, S, m, s, e, B) + fairPoissonTotalTail (k, \frac{s}{( 2 ) \cdot ( M )}, B) \leq \frac{( 3 ) \cdot ( exp (( k ) \cdot ( \frac{s}{( 2 ) \cdot ( M )} )))}{2 ^{B}}$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_reverse_marked_count_tail (✓ std3). ∎

Source. Repository-derived.

Commentary.

L=s/(2M), and all 2k comparison rates are exactly L/2. The actual term sums reverse history masses with total marked count greater than B. The comparison term is the tail of the genuine product Poisson law. For M>=64 and s/M^2<=1/256 their sum is at most 3 exp(kL)/2^B, uniformly over the same fixed support, distinct marks and both experiments.

Theorem 1.6 (actual reverse marked every event).

$\forall C zero : R e a l, 1 \leq C zero \Rightarrow \exists A : R e a l, \exists M zero : N a t, \exists e t a zero : R e a l, 0 < A \land 64 \leq M zero \land 0 < e t a zero \land \forall M, q, s, k : N a t, \forall r : R e a l, \forall S : Support (M, q), \forall m : Fin (k) \to Fin (M), 1 \leq q \land q < M \land 0 < r \land r < 1 \land compensation (M, q, r) < 1 \land injective (m) \land (k = 1 \lor k = 2) \land M zero \leq M \land 1 \leq \frac{s}{( 2 ) \cdot ( M )} \land \frac{\frac{s}{( 2 ) \cdot ( M )}}{M} \leq e t a zero \Rightarrow \forall e : Experiment (), \forall B : N a t, B \leq (C zero) \cdot (\frac{s}{( 2 ) \cdot ( M )}) \Rightarrow \forall E : Set (Sum (Fin (k), Fin (k)) \to N a t), ∣ reverseEvent (r, S, m, s, e, E) - fairPoissonEvent (k, \frac{s}{( 2 ) \cdot ( M )}, E)∣ \leq (\frac{( A ) \cdot ( \frac{s}{( 2 ) \cdot ( M )} ^{k + 1} )}{M}) \cdot (fairPoissonEvent (k, \frac{s}{( 2 ) \cdot ( M )}, E)) + \frac{( 3 ) \cdot ( exp (( k ) \cdot ( \frac{s}{( 2 ) \cdot ( M )} )))}{2 ^{B}}$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_reverse_marked_every_event (✓ std3). ∎

Source. Repository-derived.

Commentary.

For Czero>=1 there exist A>0, Mzero>=64 and etazero>0. Whenever L=s/(2M)>=1, L/M<=etazero and k=1 or 2, every natural B<=Czero L and every count event E satisfy the displayed bound. The count vector uses two copies of Fin(k), one per destination parity. ReverseEvent sums actual reverse history masses whose vector belongs to E. nu is the independent Poisson product with all rates L/2. The relative term is A L^(k+1)/M times nu(E); the additive term is 3 exp(kL)/2^B. Local estimates are summed on the finite total-count box, and both tails control its complement.

References

Truth anchor: D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_forward_marked_count_tail
Truth anchor: D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_forward_marked_every_event
Truth anchor: D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_reverse_marked_count_tail
Truth anchor: D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.actual_reverse_marked_every_event
Truth anchor: D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.poissonProduct
Truth anchor: D5/S3/Estimation/TimeArrow/MarkedPoissonEventComparison.product_poisson_tail
Dependency: D5/S3/Estimation/TimeArrow/ActualReverseMarkedPath
Dependency: D5/S3/Estimation/TimeArrow/ArbitraryMarkedCountPoissonRelative

Keyboard shortcuts

trureturing — Discovering truth

Actual Marked Counts and Poisson Events

Abstract

References