OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperInputWordBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The sampler's bit budget in the original binary input parameters

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.scaled_square_pow line 13
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.scaled_square_pow644 line 16
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.power_mono_left line 22
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.word_budget_scaled line 25
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.sampling_dimension_bound line 32
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.sampling_internal_size_bound line 43
  7. theorem OAI.ContingencyTables.SmallGraphProfiles.sampling_word_budget_polynomial line 58

    Source documentation

    All fixed random-bit segments together have a uniform polynomial bound in dimensions, binary total margin, and requested accuracy.

    theorem sampling_word_budget_polynomial {m n : ℕ}
    (r : Fin m → ℕ) (c : Fin n → ℕ) (k : ℕ) :
    smallSamplerWordBudget (dimensionAllowance (I := Fin m) (J := Fin n))
…

    Mentions: OAI.ContingencyTables.smallSamplerWordBudget