Finite uniform-seed distribution ensembles -- proof internals

The generic finite probability laws are proved by exact cardinal arithmetic. Ensemble laws then instantiate them with each slice's explicit nonempty seed space.

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

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

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

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

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

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

theorem Complexity.uniformProbability_eq_sum_fiberwise_internal {Ω : 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})

theorem Complexity.uniformProbability_product_internal {Ω : 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)

theorem Complexity.uniformProbability_product_eq_average_fibers_internal {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)

theorem Complexity.exists_fiber_uniformProbability_ge_internal {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)

theorem Complexity.uniformMean_le_threshold_add_probability_internal {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)

theorem Complexity.uniformMean_sub_div_le_probability_ge_internal {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}

theorem Complexity.half_epsilon_le_probability_ge_of_le_uniformMean_internal {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}

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

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

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

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

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

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

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

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

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

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

theorem Complexity.FiniteEnsemble.probability_not_internal {α : 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_internal {α : 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_internal {α : 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_internal {α : 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_map_internal {α : 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_internal {α : Type u} [DecidableEq α] (D : FiniteEnsemble α) (n : ℕ) : ∑ x ∈ D.support n, D.mass n x = 1

theorem Complexity.FiniteEnsemble.probability_product_internal {α : 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_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_toFinite_internal {α : Type u} (D : DyadicEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : D.toFinite.probability n P = D.probability n P