Elementary uniform probabilities on finite sample spaces

These lemmas keep the sampling estimates for exchanges finite and explicit.

noncomputable def EGZ.Expansion.finiteProb {A : Type u_1} [Fintype A] (P : A → Prop) : ℝ

The probability of a predicate under the uniform distribution on a finite type.

Equations

• EGZ.Expansion.finiteProb P = Finset.univ.expect fun (a : A) => if P a then 1 else 0

theorem EGZ.Expansion.finiteProb_nonneg {A : Type u_1} [Fintype A] (P : A → Prop) : 0 ≤ finiteProb P

theorem EGZ.Expansion.finiteProb_mono {A : Type u_1} [Fintype A] {P Q : A → Prop} (h : ∀ (a : A), P a → Q a) : finiteProb P ≤ finiteProb Q

@[simp]

theorem EGZ.Expansion.finiteProb_true {A : Type u_1} [Fintype A] [Nonempty A] : (finiteProb fun (x : A) => True) = 1

@[simp]

theorem EGZ.Expansion.finiteProb_false {A : Type u_1} [Fintype A] : (finiteProb fun (x : A) => False) = 0

theorem EGZ.Expansion.finiteProb_le_one {A : Type u_1} [Fintype A] [Nonempty A] (P : A → Prop) : finiteProb P ≤ 1

theorem EGZ.Expansion.finiteProb_not {A : Type u_1} [Fintype A] [Nonempty A] (P : A → Prop) : (finiteProb fun (a : A) => ¬P a) = 1 - finiteProb P

theorem EGZ.Expansion.finiteProb_exists_le {A : Type u_1} {I : Type u_2} [Fintype A] [Fintype I] (P : I → A → Prop) : (finiteProb fun (a : A) => ∃ (i : I), P i a) ≤ ∑ i : I, finiteProb (P i)

theorem EGZ.Expansion.exists_forall_not_of_sum_finiteProb_lt_one {A : Type u_1} {I : Type u_2} [Fintype A] [Nonempty A] [Fintype I] (P : I → A → Prop) (h : ∑ i : I, finiteProb (P i) < 1) : ∃ (a : A), ∀ (i : I), ¬P i a

theorem EGZ.Expansion.finiteProb_prod {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (P : A × B → Prop) : finiteProb P = Finset.univ.expect fun (a : A) => finiteProb fun (b : B) => P (a, b)

theorem EGZ.Expansion.expect_pi_split {I : Type u_1} [Fintype I] [DecidableEq I] (A : I → Type u_2) [(i : I) → Fintype (A i)] (i : I) (f : ((i : I) → A i) → ℝ) : (Finset.univ.expect fun (x : (i : I) → A i) => f x) = Finset.univ.expect fun (a : A i) => Finset.univ.expect fun (b : (j : { j : I // j ≠ i }) → A ↑j) => f ((Equiv.piSplitAt i A).symm (a, b))

theorem EGZ.Expansion.expect_pi_eval {I : Type u_1} [Fintype I] [DecidableEq I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] (i : I) (f : A i → ℝ) : (Finset.univ.expect fun (x : (i : I) → A i) => f (x i)) = Finset.univ.expect fun (a : A i) => f a

theorem EGZ.Expansion.finiteProb_pi_eval {I : Type u_1} [Fintype I] [DecidableEq I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] (i : I) (P : A i → Prop) : (finiteProb fun (x : (i : I) → A i) => P (x i)) = finiteProb P

theorem EGZ.Expansion.finiteProb_eq_card {A : Type u_1} [Fintype A] (P : A → Prop) [DecidablePred P] : finiteProb P = ↑(Finset.filter P Finset.univ).card / ↑(Fintype.card A)

@[simp]

theorem EGZ.Expansion.finiteProb_eq {A : Type u_1} [Fintype A] (a : A) : (finiteProb fun (x : A) => x = a) = 1 / ↑(Fintype.card A)

theorem EGZ.Expansion.expect_pi_pair {I : Type u_1} [Fintype I] [DecidableEq I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] {i j : I} (hij : j ≠ i) (f : A i → A j → ℝ) : (Finset.univ.expect fun (x : (k : I) → A k) => f (x i) (x j)) = Finset.univ.expect fun (a : A i) => Finset.univ.expect fun (b : A j) => f a b

The two samples at distinct coordinates of a finite product are independent, including when the coordinate types differ.

theorem EGZ.Expansion.finiteProb_pi_pair {I : Type u_1} [Fintype I] [DecidableEq I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] {i j : I} (hij : j ≠ i) (P : A i → A j → Prop) : (finiteProb fun (x : (k : I) → A k) => P (x i) (x j)) = Finset.univ.expect fun (a : A i) => finiteProb (P a)

theorem EGZ.Expansion.finiteProb_pi_collision_le {I : Type u_1} {B : Type u_2} [Fintype I] [DecidableEq I] (A : I → Type u_3) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] (v : (i : I) → A i → B) (hv : ∀ (i : I), Function.Injective (v i)) {i j : I} (hij : j ≠ i) : (finiteProb fun (x : (k : I) → A k) => v i (x i) = v j (x j)) ≤ 1 / ↑(Fintype.card (A j))

A collision after injectively encoding the two coordinate types has probability at most the reciprocal size of the second coordinate type.

theorem EGZ.Expansion.finiteProb_not_injective_le {I : Type u_1} {B : Type u_2} [Fintype I] [DecidableEq I] (A : I → Type u_3) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] (v : (i : I) → A i → B) (hv : ∀ (i : I), Function.Injective (v i)) {M : ℝ} (hM : 0 < M) (hsize : ∀ (i : I), M ≤ ↑(Fintype.card (A i))) : (finiteProb fun (x : (i : I) → A i) => ¬Function.Injective fun (i : I) => v i (x i)) ≤ ↑(Fintype.card I) ^ 2 / M

A union bound controls all repeated positions in an independent sample. The deliberately loose square bound avoids ordering the indices.