OAI/Combinatorics/ContingencyTables/Machines/PublicInputLength.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Binary input lengths for the sampling machine

  1. lemma OAI.ContingencyTables.Algorithms.encodeNat_length line 12
  2. lemma OAI.ContingencyTables.Algorithms.encodeNat_length_le line 15
  3. lemma OAI.ContingencyTables.Algorithms.natWords_length line 22
  4. lemma OAI.ContingencyTables.Algorithms.encodeMargins_length line 32
  5. theorem OAI.ContingencyTables.Algorithms.encodeSamplingInput_length line 58

    Source documentation

    The bit input length is polynomial in the parameters used by the paper's public sampling statement.

    theorem encodeSamplingInput_length {m n : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ)
    (htotal : (∑ i,r i)=∑ j,c j) (k : ℕ) :
    (encodeSamplingInput r c k).length ≤ 5*(samplingSize n r k)^2 := by
…

    Mentions: OAI.ContingencyTables.Algorithms.encodeSamplingInput, OAI.ContingencyTables.Algorithms.samplingSize