Finite event probability

The uniform probability of a finite event over T random bits, |E| / 2^T, defined once as eventProb and related to Finset.card and to the existing rational PTM acceptance probability NTM.acceptProb.

Main results

• eventProb with eventProb_nonneg, eventProb_mono, eventProb_le_one, eventProb_empty, eventProb_univ, the complement identity eventProb_compl, and the union bound eventProb_union_le
• eventProb_le_uniformAverage_div — finite-uniform Markov inequality
• eventProb_biUnion, eventProb_eq_sum_fiberwise — finite additivity and the conditioning-by-partition identity
• eventProb_filter_of_constant_fibers, eventProb_repeatRandomSeed — cancel uniformly ignored random bits, including the fixed-time repetition schedule
• eventProb_block — independence across blocks: a prefix/suffix-separable event's probability is the product of the two block probabilities
• eventProb_blockMajority_eq_false — the exact weighted binomial tail for majority failure across an odd number of independent blocks
• eventProb_blockMajority_false_le_two_pow — 12k + 1 independent repetitions reduce error from at most 1/3 to at most 1 / 2^k
• eventProb_blockMajority_true_ge_one_sub_two_pow, eventProb_blockMajority_true_le_two_pow — the corresponding amplified yes- and no-instance bounds
• exists_good_seed_of_sum_eventProb_lt_one, exists_good_seed_of_eventProb_le_two_pow_succ — probabilistic-method adapters from bad-event bounds to one seed that works on every input
• NTM.acceptProb_eq_eventProb — the PTM acceptance probability is the event probability of its set of accepting choice sequences
• NTM.traceEventProb_eq_of_le_of_allChoicesHalt — extending an observation clock after every path has halted preserves every event on the final state; in particular, acceptance and output probabilities are clock-invariant
• NTM.acceptProb_eq_eventProb_repeatRandomSeed — remove administrative random bits when a machine's acceptance factors through the compact repetition seed

def Complexity.eventProb {T : ℕ} (E : Finset (Fin T → Bool)) : ℚ

The uniform probability of a finite event E ⊆ (Fin T → Bool): the fraction of the 2^T random bit strings that lie in E.

Equations

• Complexity.eventProb E = ↑E.card / 2 ^ T

theorem Complexity.eventProb_nonneg {T : ℕ} (E : Finset (Fin T → Bool)) : 0 ≤ eventProb E

theorem Complexity.eventProb_mono {T : ℕ} {E F : Finset (Fin T → Bool)} (h : E ⊆ F) : eventProb E ≤ eventProb F

Probability is monotone under event inclusion.

theorem Complexity.card_le_pow {T : ℕ} (E : Finset (Fin T → Bool)) : E.card ≤ 2 ^ T

Every finite event has cardinality at most the size of the sample space.

theorem Complexity.eventProb_le_one {T : ℕ} (E : Finset (Fin T → Bool)) : eventProb E ≤ 1

theorem Complexity.eventProb_le_uniformAverage_div {T : ℕ} (E : Finset (Fin T → Bool)) (weight : (Fin T → Bool) → ℚ) (threshold : ℚ) (hthreshold : 0 < threshold) (hweight : ∀ (seed : Fin T → Bool), 0 ≤ weight seed) (hlarge : ∀ seed ∈ E, threshold ≤ weight seed) : eventProb E ≤ (∑ seed : Fin T → Bool, weight seed) / 2 ^ T / threshold

Markov's inequality for the finite uniform sample space. If every point in E has nonnegative weight at least threshold, then the probability of E is at most the uniform average weight divided by threshold.

Good seeds from probability bounds

theorem Complexity.exists_good_seed_of_sum_eventProb_lt_one {S : ℕ} {ι : Type u_1} (inputs : Finset ι) (bad : ι → Finset (Fin S → Bool)) (h : ∑ i ∈ inputs, eventProb (bad i) < 1) : ∃ (seed : Fin S → Bool), ∀ i ∈ inputs, seed ∉ bad i

The probabilistic method in probability form. If the sum, over a finite input set, of the probabilities of the corresponding bad-seed events is strictly below one, then one seed avoids every bad event.

theorem Complexity.exists_good_seed_of_eventProb_le_two_pow_succ (n S : ℕ) (bad : (Fin n → Bool) → Finset (Fin S → Bool)) (hbad : ∀ (x : Fin n → Bool), eventProb (bad x) ≤ 1 / 2 ^ (n + 1)) : ∃ (seed : Fin S → Bool), ∀ (x : Fin n → Bool), seed ∉ bad x

A 2^-(n+1) bad-seed bound for each n-bit input leaves a single seed that is good for all inputs simultaneously. The strict slack of one bit makes the argument uniform even when n = 0 or S = 0.

@[simp]

theorem Complexity.eventProb_empty {T : ℕ} : eventProb ∅ = 0

@[simp]

theorem Complexity.eventProb_univ {T : ℕ} : eventProb Finset.univ = 1

theorem Complexity.eventProb_compl {T : ℕ} (E : Finset (Fin T → Bool)) : eventProb Eᶜ = 1 - eventProb E

The probability of the complement of an event is one minus its probability.

theorem Complexity.eventProb_filter_bool_true (T : ℕ) (f : (Fin T → Bool) → Bool) : eventProb {w : Fin T → Bool | f w = true} = 1 - eventProb {w : Fin T → Bool | f w = false}

For a Boolean-valued experiment, success probability is one minus failure probability.

theorem Complexity.eventProb_union_le {T : ℕ} (E F : Finset (Fin T → Bool)) : eventProb (E ∪ F) ≤ eventProb E + eventProb F

The union bound in probability form: the probability of E ∪ F is at most the sum of their probabilities.

theorem Complexity.eventProb_biUnion_le {T : ℕ} {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (E : ι → Finset (Fin T → Bool)) : eventProb (s.biUnion E) ≤ ∑ i ∈ s, eventProb (E i)

The union bound over a finite family of events: the probability of the union ⋃ᵢ Eᵢ is at most the sum of the individual probabilities. The amplification workhorse — bounding the failure probability across many bad events.

theorem Complexity.eventProb_biUnion {T : ℕ} {ι : Type u_1} (s : Finset ι) (E : ι → Finset (Fin T → Bool)) (h : (↑s).PairwiseDisjoint E) : eventProb (s.biUnion E) = ∑ i ∈ s, eventProb (E i)

Finite additivity: the probability of a disjoint finite union is the sum of the probabilities of its events.

theorem Complexity.eventProb_eq_sum_fiberwise {T : ℕ} {ι : Type u_1} [DecidableEq ι] (E : Finset (Fin T → Bool)) (s : Finset ι) (f : (Fin T → Bool) → ι) (h : Set.MapsTo f ↑E ↑s) : eventProb E = ∑ i ∈ s, eventProb ({w ∈ E | f w = i})

Conditioning by a finite partition. If the statistic f maps every point of E into the finite index set s, then E is the disjoint union of its fibers and its probability is the sum of their probabilities.

theorem Complexity.eventProb_filter_of_constant_fibers {total compact ignored : ℕ} (htotal : total = compact + ignored) (randomSeed : (Fin total → Bool) → Fin compact → Bool) (Accept : (Fin total → Bool) → Prop) (Good : (Fin compact → Bool) → Prop) [DecidablePred Accept] [DecidablePred Good] (hfactor : ∀ (w : Fin total → Bool), Accept w ↔ Good (randomSeed w)) (hfiber : ∀ (seed : Fin compact → Bool), {w : Fin total → Bool | randomSeed w = seed}.card = 2 ^ ignored) : eventProb (Finset.filter Accept Finset.univ) = eventProb (Finset.filter Good Finset.univ)

Uniformly ignored random bits cancel from event probability. If an event on total = compact + ignored bits factors through a compact-seed projection whose fibers all have size 2 ^ ignored, its probability is exactly the probability of the corresponding compact event.

theorem Complexity.eventProb_repeatRandomSeed (k T : ℕ) (P : (Fin (k * T) → Bool) → Prop) [DecidablePred P] : eventProb {w : Fin (2 + k * (2 * T + 2)) → Bool | P (repeatRandomSeed k T w)} = eventProb (Finset.filter P Finset.univ)

The fixed-time repetition schedule's administrative choices do not change the probability of an event depending only on its k * T simulation bits.

theorem Complexity.eventProb_block {a b : ℕ} (P : (Fin a → Bool) → Prop) (Q : (Fin b → Bool) → Prop) [DecidablePred P] [DecidablePred Q] : eventProb {w : Fin (a + b) → Bool | P (blockFst a b w) ∧ Q (blockSnd a b w)} = eventProb (Finset.filter P Finset.univ) * eventProb (Finset.filter Q Finset.univ)

Independence across blocks (probability form). For an event that constrains the prefix and suffix of a length-a + b random string separately, the joint probability is the product of the two block probabilities. This is the probability-level counterpart of card_filter_block and the quantitative engine behind error amplification: k independent runs multiply their success probabilities.

theorem Complexity.eventProb_blockMajority_eq_false (T r : ℕ) (E : Finset (Fin T → Bool)) : eventProb {w : Fin ((2 * r + 1) * T) → Bool | blockMajority E w = false} = ∑ j ∈ Finset.range (r + 1), ↑((2 * r + 1).choose j) * eventProb E ^ j * (1 - eventProb E) ^ (2 * r + 1 - j)

Exact majority-failure probability across independent blocks. Splitting a uniform long seed into 2r + 1 blocks makes block-event membership independent, so the failure probability is the lower tail of the binomial distribution with success probability eventProb E.

theorem Complexity.binomial_lower_tail_le (r : ℕ) (p : ℚ) (hp_lower : 2 / 3 ≤ p) (hp_upper : p ≤ 1) : ∑ j ∈ Finset.range (r + 1), ↑((2 * r + 1).choose j) * p ^ j * (1 - p) ^ (2 * r + 1 - j) ≤ 1 / 3 * (8 / 9) ^ r

The lower tail of an odd binomial distribution with success probability at least 2/3 is at most (1/3) * (8/9)^r. This deliberately uses a coarse elementary bound rather than a Chernoff inequality: each failure term is bounded by (1/3) * (2/9)^r, and the lower-half binomial coefficients sum to 4^r.

theorem Complexity.eventProb_blockMajority_false_le_two_pow (T k : ℕ) (E : Finset (Fin T → Bool)) (hE : 2 / 3 ≤ eventProb E) : eventProb {w : Fin ((12 * k + 1) * T) → Bool | blockMajority E w = false} ≤ 1 / 2 ^ k

Concrete error amplification. If one T-bit trial succeeds with probability at least 2/3, then the strict majority of 12k + 1 independent trials fails with probability at most 1 / 2^k. The explicit odd repetition count avoids ties and is sufficient for later BPP and protocol amplification.

theorem Complexity.eventProb_blockMajority_true_ge_one_sub_two_pow (T k : ℕ) (E : Finset (Fin T → Bool)) (hE : 2 / 3 ≤ eventProb E) : 1 - 1 / 2 ^ k ≤ eventProb {w : Fin ((12 * k + 1) * T) → Bool | blockMajority E w = true}

Majority amplification on yes-instances: a source success probability at least 2/3 becomes at least 1 - 2^-k after 12k + 1 trials.

theorem Complexity.eventProb_blockMajority_true_le_two_pow (T k : ℕ) (E : Finset (Fin T → Bool)) (hE : eventProb E ≤ 1 / 3) : eventProb {w : Fin ((12 * k + 1) * T) → Bool | blockMajority E w = true} ≤ 1 / 2 ^ k

Majority amplification on no-instances: a source success probability at most 1/3 becomes at most 2^-k after 12k + 1 trials.

theorem Complexity.eventProb_map {T : ℕ} (e : (Fin T → Bool) ≃ (Fin T → Bool)) (E : Finset (Fin T → Bool)) : eventProb (Finset.map e.toEmbedding E) = eventProb E

Event probability is invariant under any relabeling of the sample space — in particular under permuting the bit positions (Equiv.arrowCongr σ) — since a bijection preserves cardinality.

theorem Complexity.NTM.acceptProb_eq_eventProb {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : tm.acceptProb x T = eventProb {choices : Fin T → Bool | have c' := tm.trace T choices (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one}

The PTM acceptance probability is exactly the event probability of the set of accepting choice sequences: this ties NTM.acceptProb to the abstract eventProb / Finset.card layer.

theorem Complexity.NTM.traceEventProb_eq_of_le_of_allChoicesHalt {n T T' : ℕ} (tm : NTM n) (c : Cfg n tm.Q) (event : Cfg n tm.Q → Prop) [DecidablePred event] (hle : T ≤ T') (hhalt : ∀ (choices : Fin T → Bool), tm.halted (tm.trace T choices c)) : eventProb {choices : Fin T' → Bool | event (tm.trace T' choices c)} = eventProb {choices : Fin T → Bool | event (tm.trace T choices c)}

Once every path from c has halted by time T, extending the observation clock to any T' ≥ T preserves the probability of every decidable event on the final configuration. Halted traces are fixed, and every length-T choice sequence has the same number of extensions, so the extra random bits cancel.

theorem Complexity.NTM.acceptProb_eq_of_le_of_allChoicesHalt {n T T' : ℕ} (tm : NTM n) (x : List Bool) (hle : T ≤ T') (hhalt : ∀ (choices : Fin T → Bool), tm.halted (tm.trace T choices (tm.initCfg x))) : tm.acceptProb x T' = tm.acceptProb x T

Once every path has halted by time T, extending the observation clock to any T' ≥ T leaves acceptance probability unchanged.

theorem Complexity.NTM.acceptProb_eq_of_le_of_allPathsHaltIn {n : ℕ} {T T' : ℕ → ℕ} (tm : NTM n) (hle : ∀ (m : ℕ), T m ≤ T' m) (hhalt : tm.AllPathsHaltIn T) (x : List Bool) : tm.acceptProb x (T' x.length) = tm.acceptProb x (T x.length)

A pointwise-larger clock gives the same acceptance probability once the machine satisfies AllPathsHaltIn for the smaller clock.

theorem Complexity.NTM.outputProb_eq_eventProb {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) (y : List Bool) : tm.outputProb x T y = eventProb {choices : Fin T → Bool | have c := tm.trace T choices (tm.initCfg x); c.state = tm.qhalt ∧ c.output.HasOutput y}

The PTM probability of output y is exactly the event probability of the choice sequences that halt with that output.

theorem Complexity.NTM.outputProb_eq_of_le_of_allChoicesHalt {n T T' : ℕ} (tm : NTM n) (x y : List Bool) (hle : T ≤ T') (hhalt : ∀ (choices : Fin T → Bool), tm.halted (tm.trace T choices (tm.initCfg x))) : tm.outputProb x T' y = tm.outputProb x T y

Once every path has halted by time T, extending the observation clock to any T' ≥ T leaves every output probability unchanged.

theorem Complexity.NTM.outputProb_eq_of_le_of_allPathsHaltIn {n : ℕ} {T T' : ℕ → ℕ} (tm : NTM n) (hle : ∀ (m : ℕ), T m ≤ T' m) (hhalt : tm.AllPathsHaltIn T) (x y : List Bool) : tm.outputProb x (T' x.length) y = tm.outputProb x (T x.length) y

A pointwise-larger clock gives the same output probabilities once the machine satisfies AllPathsHaltIn for the smaller clock.

theorem Complexity.NTM.acceptProb_eq_eventProb_repeatRandomSeed {n : ℕ} (tm : NTM n) (x : List Bool) (k T : ℕ) (P : (Fin (k * T) → Bool) → Prop) [DecidablePred P] (hfactor : ∀ (choices : Fin (2 + k * (2 * T + 2)) → Bool), (have c' := tm.trace (2 + k * (2 * T + 2)) choices (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one) ↔ P (repeatRandomSeed k T choices)) : tm.acceptProb x (2 + k * (2 * T + 2)) = eventProb (Finset.filter P Finset.univ)

A repeated machine's administrative random choices cancel from its acceptance probability whenever its accepting-path predicate factors through repeatRandomSeed. The result is the event probability on only the k * T simulation choices.