OAI/Combinatorics/ContingencyTables/Sampling/ExactGatePolynomial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform polynomial bound for the cheap public prefix

  1. def OAI.ContingencyTables.ExactGatePolynomial.measure line 19
  2. theorem OAI.ContingencyTables.ExactGatePolynomial.budget_polynomial line 22
  3. theorem OAI.ContingencyTables.ExactGatePolynomial.public_bound line 48

    Source documentation

    Any fixed polynomial print allowance still gives a uniform public polynomial bound for the prefix before the rare tabulation starts.

    theorem public_bound (print : Polynomial ℕ) : ∃ p : Polynomial ℕ,
    ∀ (m n : ℕ) (r : Fin m → ℕ) (c : Fin n → ℕ),
      (∑ i,r i)=∑ j,c j →
      let B := print.eval (ExactPrintCost.matrixSize (n := n) r)
…

    Mentions: OAI.ContingencyTables.ExactPrintCost.matrixSize