OAI/Combinatorics/ContingencyTables/Sampling/ProfileRuntimeBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform public polynomial bound for the physical sampler

  1. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_scaled_power line 13
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.wordMeasure_from_bounds line 35
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.public_wordMeasure_bound line 49
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.samplingMachineTime_public_bound line 63

    Source documentation

    The explicit binary word count and physical compiler yield one polynomial bound in the manuscript's public input parameters.

    theorem samplingMachineTime_public_bound :
    ∃ C d : ℕ,0<C ∧ ∀ (m n : ℕ) (r : Fin m → ℕ) (c : Fin n → ℕ),
      (∑ i,r i)=∑ j,c j → ∀ k,
      samplingMachineTime (encodeSamplingInput r c k)≤C*(samplingSize n r k)^d := by
…