Finite uniform-seed distribution ensembles

This module exposes exact distributions generated from arbitrary nonempty finite uniform seed spaces. It generalizes dyadic ensembles while preserving sampler multiplicity, and provides probability laws, pushforwards, products, point masses, normalization, and an exact dyadic-to-finite bridge.

theorem Complexity.uniformProbability_nonneg {Ω : Type u} [Fintype Ω] (event : Finset Ω) : 0 ≤ uniformProbability event

Uniform finite-event probabilities are nonnegative.

theorem Complexity.uniformProbability_le_one {Ω : Type u} [Fintype Ω] [Nonempty Ω] (event : Finset Ω) : uniformProbability event ≤ 1

Uniform finite-event probabilities are at most one in a nonempty sample space.

@[simp]

theorem Complexity.uniformProbability_empty {Ω : Type u} [Fintype Ω] : uniformProbability ∅ = 0

The empty event has uniform probability zero.

@[simp]

theorem Complexity.uniformProbability_univ {Ω : Type u} [Fintype Ω] [Nonempty Ω] : uniformProbability Finset.univ = 1

The entire nonempty sample space has uniform probability one.

theorem Complexity.uniformProbability_compl {Ω : Type u} [Fintype Ω] [DecidableEq Ω] [Nonempty Ω] (event : Finset Ω) : uniformProbability eventᶜ = 1 - uniformProbability event

Uniform probability of a complement is one minus the original probability.

theorem Complexity.uniformProbability_union_le {Ω : Type u} [Fintype Ω] [DecidableEq Ω] (event₁ event₂ : Finset Ω) : uniformProbability (event₁ ∪ event₂) ≤ uniformProbability event₁ + uniformProbability event₂

Union bound for arbitrary finite uniform sample spaces.

theorem Complexity.uniformProbability_eq_sum_fiberwise {Ω : Type u} {ι : Type v} [Fintype Ω] [DecidableEq Ω] [DecidableEq ι] (event : Finset Ω) (indices : Finset ι) (f : Ω → ι) (hmaps : Set.MapsTo f ↑event ↑indices) : uniformProbability event = ∑ i ∈ indices, uniformProbability ({seed ∈ event | f seed = i})

Conditioning by a finite partition of a uniform sample space.

theorem Complexity.uniformProbability_product {Ω : Type u} {Ξ : Type v} [Fintype Ω] [DecidableEq Ω] [Fintype Ξ] [DecidableEq Ξ] (P : Ω → Prop) (Q : Ξ → Prop) [DecidablePred P] [DecidablePred Q] : uniformProbability {seed : Ω × Ξ | P seed.1 ∧ Q seed.2} = uniformProbability (Finset.filter P Finset.univ) * uniformProbability (Finset.filter Q Finset.univ)

Independent finite uniform seeds multiply event probabilities.

theorem Complexity.uniformProbability_product_eq_average_fibers {advice : Type u} {challenge : Type v} [Fintype advice] [DecidableEq advice] [Nonempty advice] [Fintype challenge] [DecidableEq challenge] [Nonempty challenge] (event : advice → challenge → Prop) [DecidablePred fun (sample : advice × challenge) => event sample.1 sample.2] [(fixed : advice) → DecidablePred (event fixed)] : uniformProbability {sample : advice × challenge | event sample.1 sample.2} = (∑ fixed : advice, uniformProbability (Finset.filter (event fixed) Finset.univ)) / ↑(Fintype.card advice)

Uniform probability on a product is the average of its conditional fiber probabilities over the first coordinate.

theorem Complexity.exists_fiber_uniformProbability_ge {advice : Type u} {challenge : Type v} [Fintype advice] [DecidableEq advice] [Nonempty advice] [Fintype challenge] [DecidableEq challenge] [Nonempty challenge] (event : advice → challenge → Prop) [DecidablePred fun (sample : advice × challenge) => event sample.1 sample.2] [(fixed : advice) → DecidablePred (event fixed)] : ∃ (fixed : advice), uniformProbability {sample : advice × challenge | event sample.1 sample.2} ≤ uniformProbability (Finset.filter (event fixed) Finset.univ)

Some first-coordinate fiber has probability at least the joint product probability.

theorem Complexity.uniformMean_le_threshold_add_probability {sample : Type u} [Fintype sample] [DecidableEq sample] [Nonempty sample] (value : sample → ℚ) (threshold : ℚ) (hupper : ∀ (input : sample), value input ≤ 1) : uniformMean value ≤ threshold + uniformProbability {input : sample | threshold ≤ value input} * (1 - threshold)

If a finite statistic is at most one, its mean is bounded by a threshold plus the probability of exceeding that threshold times the remaining range.

theorem Complexity.uniformMean_sub_div_le_probability_ge {sample : Type u} [Fintype sample] [DecidableEq sample] [Nonempty sample] (value : sample → ℚ) (lower threshold : ℚ) (hupper : ∀ (input : sample), value input ≤ 1) (hlower : lower ≤ uniformMean value) (hthreshold : threshold < 1) : (lower - threshold) / (1 - threshold) ≤ uniformProbability {input : sample | threshold ≤ value input}

Exact reverse averaging bound for a statistic bounded above by one.

theorem Complexity.half_epsilon_le_probability_ge_of_le_uniformMean {sample : Type u} [Fintype sample] [DecidableEq sample] [Nonempty sample] (value : sample → ℚ) (epsilon : ℚ) (hepsilon : 0 ≤ epsilon) (hupper : ∀ (input : sample), value input ≤ 1) (hmean : 1 / 2 + epsilon ≤ uniformMean value) : epsilon / 2 ≤ uniformProbability {input : sample | 1 / 2 + epsilon / 2 ≤ value input}

Hirahara's convenient half-advantage corollary: mean at least 1/2 + ε forces an ε/2 fraction of samples to have value at least 1/2 + ε/2.

theorem Complexity.uniformAtLeastOneProbability_eq_one_sub_pow {Ω : Type u} [Fintype Ω] [DecidableEq Ω] [Nonempty Ω] (event : Finset Ω) (trials : ℕ) : uniformAtLeastOneProbability event trials = 1 - (1 - uniformProbability event) ^ trials

Exact success probability for independent repetition: if one uniform draw lands in event with probability p, then at least one of trials draws lands there with probability 1 - (1 - p) ^ trials.

theorem Complexity.one_sub_pow_le_uniformAtLeastOneProbability {Ω : Type u} [Fintype Ω] [DecidableEq Ω] [Nonempty Ω] (event : Finset Ω) (trials : ℕ) (singleDrawLower : ℚ) (hlower : singleDrawLower ≤ uniformProbability event) : 1 - (1 - singleDrawLower) ^ trials ≤ uniformAtLeastOneProbability event trials

A lower bound on one-draw success lifts to the corresponding independent repetition bound.

theorem Complexity.trials_mul_div_one_add_le_uniformAtLeastOneProbability {Ω : Type u} [Fintype Ω] [DecidableEq Ω] [Nonempty Ω] (event : Finset Ω) (trials : ℕ) : ↑trials * uniformProbability event / (1 + ↑trials * uniformProbability event) ≤ uniformAtLeastOneProbability event trials

A denominator-free quantitative repetition bound: trials independent draws hit an event of probability p with probability at least trials * p / (1 + trials * p).

theorem Complexity.half_le_uniformAtLeastOneProbability_of_singleDrawLower {Ω : Type u} [Fintype Ω] [DecidableEq Ω] [Nonempty Ω] (event : Finset Ω) (trials : ℕ) (singleDrawLower : ℚ) (hlower : singleDrawLower ≤ uniformProbability event) (htrials : 1 ≤ ↑trials * singleDrawLower) : 1 / 2 ≤ uniformAtLeastOneProbability event trials

If the number of trials times a certified one-draw success lower bound is at least one, independent repetition succeeds with probability at least one half.

theorem Complexity.uniformProbability_equiv {Ω : Type u} {Ξ : Type v} [Fintype Ω] [DecidableEq Ω] [Fintype Ξ] [DecidableEq Ξ] (e : Ω ≃ Ξ) (P : Ξ → Prop) [DecidablePred P] : uniformProbability {x : Ω | P (e x)} = uniformProbability (Finset.filter P Finset.univ)

Relabeling a finite uniform sample space by an equivalence preserves event probability.

theorem Complexity.uniformProbability_eq {Ω : Type u} [Fintype Ω] [DecidableEq Ω] (x : Ω) : uniformProbability {y : Ω | y = x} = 1 / ↑(Fintype.card Ω)

Every point in a finite uniform sample space has reciprocal-cardinality probability.

theorem Complexity.FiniteEnsemble.probability_nonneg {α : Type u} (D : FiniteEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : 0 ≤ D.probability n P

Ensemble event probabilities are nonnegative.

theorem Complexity.FiniteEnsemble.probability_le_one {α : Type u} (D : FiniteEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : D.probability n P ≤ 1

Ensemble event probabilities are at most one.

@[simp]

theorem Complexity.FiniteEnsemble.probability_false {α : Type u} (D : FiniteEnsemble α) (n : ℕ) : (D.probability n fun (x : α) => False) = 0

@[simp]

theorem Complexity.FiniteEnsemble.probability_true {α : Type u} (D : FiniteEnsemble α) (n : ℕ) : (D.probability n fun (x : α) => True) = 1

theorem Complexity.FiniteEnsemble.probability_not {α : Type u} (D : FiniteEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : (D.probability n fun (x : α) => ¬P x) = 1 - D.probability n P

theorem Complexity.FiniteEnsemble.probability_or_le {α : Type u} (D : FiniteEnsemble α) (n : ℕ) (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] : (D.probability n fun (x : α) => P x ∨ Q x) ≤ D.probability n P + D.probability n Q

theorem Complexity.FiniteEnsemble.probability_mono {α : Type u} (D : FiniteEnsemble α) (n : ℕ) (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (x : α), P x → Q x) : D.probability n P ≤ D.probability n Q

theorem Complexity.FiniteEnsemble.probability_congr {α : Type u} (D : FiniteEnsemble α) (n : ℕ) (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (x : α), P x ↔ Q x) : D.probability n P = D.probability n Q

@[simp]

theorem Complexity.FiniteEnsemble.probability_map {α : Type u} {β : Type w} (D : FiniteEnsemble α) (f : α → β) (n : ℕ) (P : β → Prop) [DecidablePred P] : (D.map f).probability n P = D.probability n fun (x : α) => P (f x)

theorem Complexity.FiniteEnsemble.sum_mass_eq_one {α : Type u} [DecidableEq α] (D : FiniteEnsemble α) (n : ℕ) : ∑ x ∈ D.support n, D.mass n x = 1

theorem Complexity.FiniteEnsemble.probability_product {α : Type u} {β : Type w} (D : FiniteEnsemble α) (E : FiniteEnsemble β) (n : ℕ) (P : α → Prop) (Q : β → Prop) [DecidablePred P] [DecidablePred Q] : ((D.product E).probability n fun (xy : α × β) => P xy.1 ∧ Q xy.2) = D.probability n P * E.probability n Q

theorem Complexity.FiniteEnsemble.probability_dirac {α : Type u} (x : ℕ → α) (n : ℕ) (P : α → Prop) [DecidablePred P] : (dirac x).probability n P = if P (x n) then 1 else 0

@[simp]

theorem Complexity.DyadicEnsemble.probability_toFinite {α : Type u} (D : DyadicEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : D.toFinite.probability n P = D.probability n P

The finite-uniform embedding preserves every event probability exactly.