Exact dyadic distribution ensembles

This module exposes finite distribution ensembles represented by uniform Boolean seeds. It provides exact event probabilities, pushforwards, point masses, independent products, and normalization of the induced finite mass function.

Polynomial-time samplability and heuristic algorithms are deliberately separate layers: these definitions and counting theorems make no computational claim about the sample map.

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

Ensemble event probabilities are nonnegative.

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

Ensemble event probabilities are at most one.

@[simp]

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

The impossible event has probability zero.

@[simp]

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

The certain event has probability one.

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

Complementary events have complementary probabilities.

theorem Complexity.DyadicEnsemble.probability_or_le {α : Type u} (D : DyadicEnsemble α) (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

Union bound for two predicates on one ensemble slice.

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

Event probability is monotone under predicate implication.

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

Extensionally equal events have equal probability.

@[simp]

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

Exact pushforward law: measuring P after mapping samples by f is the same as measuring the preimage of P in the source ensemble.

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

The masses of all outputs in a slice's finite support sum exactly to one.

theorem Complexity.DyadicEnsemble.probability_product {α : Type u} {β : Type v} (D : DyadicEnsemble α) (E : DyadicEnsemble β) (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

Events on independently sampled components have product probability.

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

A point mass assigns probability one exactly to events containing its selected point.

theorem Complexity.DyadicEnsemble.probability_uniformBits (n : ℕ) (P : List Bool → Prop) [DecidablePred P] : uniformBits.probability n P = eventProb {seed : Fin n → Bool | P (List.ofFn seed)}

Event probability under uniform n-bit lists is ordinary finite uniform probability over Fin n → Bool.