Documentation

VCVio.OracleComp.ProbComp

Discrete compatibility laws for uniform oracle sampling #

Finite support and discrete output-probability equations for the uniform sampling operations.

source
@[simp]
theorem ProbComp.finSupport_uniformFin (n : ℕ) :
finSupport $[0..n] = Finset.univ
source
theorem ProbComp.probOutput_uniformFin_eq_div (n : ℕ) (m : Fin (n + 1)) :
Pr[= m | $[0..n]] = 1 / (↑n + 1)
source
@[simp]
theorem ProbComp.probOutput_uniformFin (n : ℕ) (m : Fin (n + 1)) :
Pr[= m | $[0..n]] = (↑n + 1)⁻¹
source
@[simp]
theorem ProbComp.probEvent_uniformFin (n : ℕ) (p : Fin (n + 1) → Prop) [DecidablePred p] :
probEvent $[0..n] p = ↑(Fin.countP fun (i : Fin (n + 1)) => decide (p i)) / ↑(n + 1)
source
theorem ProbComp.probFailure_uniformFin (n : ℕ) :
Pr[⊥ | $[0..n]] = 0
source
@[simp]
theorem ProbComp.probOutput_uniformRange (n m : ℕ) (k : Fin (m + 1)) (h : n < m) :
Pr[= k | uniformRange n m h] = if n ≤ ↑k then (↑m - ↑n + 1)⁻¹ else 0
source
@[simp]
theorem ProbComp.finSupport_uniformRange (n m : ℕ) (h : n < m) :
finSupport (uniformRange n m h) = Finset.Icc (Fin.ofNat (m + 1) n) (Fin.ofNat (m + 1) m)
source
@[simp]
theorem ProbComp.probEvent_uniformRange (n m : ℕ) (p : Fin (m + 1) → Prop) [DecidablePred p] (h : n < m) :
probEvent (uniformRange n m h) p = ↑{x : Fin (m + 1) | n ≤ ↑x ∧ p x}.card / (↑m - ↑n + 1)
source
theorem ProbComp.probFailure_uniformRange (n m : ℕ) (h : n < m) :
Pr[⊥ | uniformRange n m h] = 0
source
@[simp]
theorem ProbComp.finSupport_uniformSelectList {α : Type} [DecidableEq α] (xs : List α) :
finSupport ($xs) = xs.toFinset
source
@[simp]
theorem ProbComp.probOutput_uniformSelectList {α : Type} [DecidableEq α] (xs : List α) (x : α) :
Pr[= x | $xs] = ↑(List.count x xs) / ↑xs.length
source
@[simp]
theorem ProbComp.probFailure_uniformSelectList {α : Type} (xs : List α) :
Pr[⊥ | $xs] = if xs.isEmpty = true then 1 else 0
source
@[simp]
theorem ProbComp.probEvent_uniformSelectList {α : Type} (xs : List α) (p : α → Prop) [DecidablePred p] :
probEvent ($xs) p = ↑(List.countP (fun (b : α) => decide (p b)) xs) / ↑xs.length
source
@[simp]
theorem ProbComp.finSupport_uniformSelectVector {α : Type} {n : ℕ} (xs : Vector α (n + 1)) [DecidableEq α] :
finSupport ($xs) = xs.toList.toFinset
source
@[simp]
theorem ProbComp.probOutput_uniformSelectVector {α : Type} {n : ℕ} (xs : Vector α (n + 1)) [DecidableEq α] (x : α) :
Pr[= x | $!xs] = ↑(Vector.count x xs) / (↑n + 1)
source
@[simp]
theorem ProbComp.probEvent_uniformSelectVector {α : Type} {n : ℕ} (xs : Vector α (n + 1)) (p : α → Prop) [DecidablePred p] :
probEvent ($xs) p = ↑(List.countP (fun (b : α) => decide (p b)) xs.toList) / (↑n + 1)
source
@[simp]
theorem ProbComp.probOutput_uniformSelectListVector {α : Type} {n : ℕ} (xs : List.Vector α (n + 1)) [DecidableEq α] (x : α) :
Pr[= x | $!xs] = ↑(List.count x xs.toList) / (↑n + 1)
source
@[simp]
theorem ProbComp.probEvent_uniformSelectListVector {α : Type} {n : ℕ} (xs : List.Vector α (n + 1)) (p : α → Prop) [DecidablePred p] :
probEvent ($!xs) p = ↑(List.countP (fun (b : α) => decide (p b)) xs.toList) / (↑n + 1)
source
@[simp]
theorem ProbComp.finSupport_uniformSelectFinset {α : Type} (s : Finset α) [DecidableEq α] :
finSupport ($s) = if s.Nonempty then s else ∅
source
@[simp]
theorem ProbComp.probOutput_uniformSelectFinset {α : Type} (s : Finset α) [DecidableEq α] (x : α) :
Pr[= x | $s] = if x ∈ s then (↑s.card)⁻¹ else 0
source
@[simp]
theorem ProbComp.probEvent_uniformSelectFinset {α : Type} (s : Finset α) (p : α → Prop) [DecidablePred p] :
probEvent ($s) p = ↑{x ∈ s | p x}.card / ↑s.card
source
@[simp]
theorem ProbComp.probFailure_uniformSelectFinset {α : Type} (s : Finset α) :
Pr[⊥ | $s] = if s.Nonempty then 0 else 1
source
@[simp]
theorem ProbComp.finSupport_uniformSelectArray {α : Type} (xs : Array α) [DecidableEq α] :
finSupport ($xs) = xs.toList.toFinset
source
@[simp]
theorem ProbComp.probFailure_uniformSelectArray {α : Type} (xs : Array α) :
Pr[⊥ | $xs] = if xs.size = 0 then 1 else 0
source
@[simp]
theorem ProbComp.finSupport_uniformSelectMultiset {α : Type} (s : Multiset α) [DecidableEq α] :
finSupport ($s) = s.toFinset
source
@[simp]
theorem ProbComp.probOutput_uniformSelectMultiset {α : Type} (s : Multiset α) [DecidableEq α] (x : α) :
Pr[= x | $s] = ↑(Multiset.count x s) / ↑s.card
source
@[simp]
theorem ProbComp.probEvent_uniformSelectMultiset {α : Type} (s : Multiset α) (p : α → Prop) [DecidablePred p] :
probEvent ($s) p = ↑(Multiset.countP p s) / ↑s.card
source
@[simp]
theorem ProbComp.probFailure_uniformSelectMultiset {α : Type} (s : Multiset α) :
Pr[⊥ | $s] = if 0 < s.card then 0 else 1
source
@[simp]
theorem finSupport_coin :
finSupport OracleComp.coin = {true, false}
source
@[simp]
theorem probOutput_coin (b : Bool) :
Pr[= b | OracleComp.coin] = 2⁻¹
source
@[simp]
theorem probEvent_coin (p : Bool → Prop) [DecidablePred p] :
probEvent OracleComp.coin p = if p true then if p false then 1 else 2⁻¹ else if p false then 2⁻¹ else 0
source
theorem probFailure_coin :
Pr[⊥ | OracleComp.coin] = 0