ProfilePublicMachine.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Physical execution of the computed public profile sampler

lemma OAI.ContingencyTables.ProfilePrograms.printMatrix_alphabet line 12
lemma OAI.ContingencyTables.ProfilePrograms.publicSampling_alphabet line 22
lemma OAI.ContingencyTables.ProfilePrograms.samplingInput_nonzero line 25
def OAI.ContingencyTables.ProfilePrograms.samplingMachine line 35
def OAI.ContingencyTables.ProfilePrograms.samplingMachineTime line 38
theorem OAI.ContingencyTables.ProfilePrograms.samplingMachineTime_polynomial line 43
Source documentation
A single fixed transition table implements the public program, with cost controlled by its computed word schedule.
```
theorem samplingMachineTime_polynomial :
    ∃ p : Polynomial ℕ,∀ as,samplingMachineTime as≤p.eval
      (FiniteWordExecution.wordMeasure publicWordCount as) :=
…
```
Mentions: OAI.ContingencyTables.ProfilePrograms.samplingMachineTime, OAI.ContingencyTables.FiniteWordExecution.wordMeasure, OAI.ContingencyTables.ProfilePrograms.publicWordCount

theorem OAI.ContingencyTables.SmallGraphProfiles.samplingMachine_large_outputs line 62

Source documentation

Every actual machine execution in the nonempty large-rectangle branch halts and outputs a feasible original table.

theorem samplingMachine_large_outputs
    (hr : 0<(largeIndices (d^20,List.ofFn r)).length)
    (hc : 0<(largeIndices (d^20,List.ofFn c)).length)
    (htotal : (∑ i,r i)=∑ j,c j) (k t : ℕ)
    (ht : samplingMachineTime (Algorithms.encodeSamplingInput r c k)≤t) :
    ∀ bits : Bits t,∃ X : Table r c,
      Algorithms.OutputsTable samplingMachine (Algorithms.encodeSamplingInput r c k) bits X.val := by
…

Mentions: OAI.ContingencyTables.Algorithms.encodeSamplingInput, OAI.ContingencyTables.Table, OAI.ContingencyTables.Algorithms.OutputsTable