OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorExpectation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_coordinate line 19
2. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_pi_coordinate line 25
3. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.probability_pi_coordinate line 32
4. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_sum line 42
5. def OAI.LowSpaceSubsetSum.SeparatorExpectation.incidence line 47
6. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_incidence line 51
7. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.table_size_eq line 71

   Source documentation

   The indexed stored incidence array counts the same individual draws.

   theorem table_size_eq {ν : ℕ} {α β : Type*} (family : Fin ν → β)
       (compatible : α → β → Bool) (x : α) :
       (SeparatorIncidenceTable.table (Array.ofFn family) compatible x).size =
         incidence (fun y => compatible x y = true) family := by
   …

   Mentions: OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.table, OAI.LowSpaceSubsetSum.SeparatorExpectation.incidence

8. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_pi_product line 94

   Source documentation

   Product factorization uses the actual independent uniform family law.

   theorem mean_pi_product {ι : Type*} [Fintype ι] [DecidableEq ι] {Ψ : ι → Type*}
       [∀ i, Fintype (Ψ i)] (f : ∀ i, Ψ i → ℝ) :
       mean (fun draws : ∀ i, Ψ i => ∏ i, f i (draws i)) = ∏ i, mean (f i) := by
   …

9. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.sample_probability line 103

   Source documentation

   Exact probability that one sampled separator contains/avoids fixed masks.

   theorem sample_probability (U L R : Finset ι) (e : ℕ)
       (hL : L ⊆ U) (hR : R ⊆ U) (hd : Disjoint L R) (he : L.card ≤ e) :
       finiteUniformProbability (fun S : SeparatorSample U e => L ⊆ S.val ∧ Disjoint S.val R) =
         (Nat.choose (U.card - R.card - L.card) (e - L.card) : ℝ) / Nat.choose U.card e := by
   …

   Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.SeparatorSample

10. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.containment_probability line 127
11. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.avoidance_probability line 132
12. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_containment line 137
13. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_avoidance line 146