Exact dyadic distribution ensembles -- proof internals

The results reduce ensemble probability to exact counting over the underlying Boolean seed space. In particular, total mass follows by partitioning seeds into sample fibers, and product probability follows from the explicit block bijection.

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

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

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

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

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

theorem Complexity.DyadicEnsemble.probability_or_le_internal {α : 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

theorem Complexity.DyadicEnsemble.probability_mono_internal {α : 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

theorem Complexity.DyadicEnsemble.probability_congr_internal {α : 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

theorem Complexity.DyadicEnsemble.probability_map_internal {α : 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)

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

theorem Complexity.DyadicEnsemble.probability_product_internal {α : 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

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

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