ExactPhysicalCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A physical cost bound for every finite prefix of the exact sampler

def OAI.ContingencyTables.ExactPhysicalCost.typedBudget line 15
def OAI.ContingencyTables.ExactPhysicalCost.budget line 18

theorem OAI.ContingencyTables.ExactPhysicalCost.prefix_correct_cost line 24

Source documentation

The compiler's quadratic overhead is charged to the actual finite prefix cost. The executable program is still the same unbounded sampler.

theorem prefix_correct_cost (as : List Symbol) (N B : ℕ)
    (hB : (ExactCoreProgram.prefixExperiment (exactParsedMargins as) N).All
      (fun o => o.elim 0 GreedyFeasibleTable.printMatrixRealizer.cost≤B)) :
    ∃ q,Implements program.table (output as)
      (program.initial (Tape.mk₁ (packed as))) q ∧
      (∀ g : Option MatrixCode → ℚ,
        q.mean g=(ExactCoreProgram.prefixExperiment (exactParsedMargins as) N).mean g) ∧
      q.cost≤budget as N B := by
…

Mentions: OAI.ContingencyTables.ExactCoreProgram.prefixExperiment, OAI.ContingencyTables.ExactPhysicalCost.budget

lemma OAI.ContingencyTables.ExactPhysicalCost.typedBudget_le_scaled line 43
lemma OAI.ContingencyTables.ExactPhysicalCost.factor_le_scaled line 50
lemma OAI.ContingencyTables.ExactPhysicalCost.quadratic_budget line 65
Source documentation
One fixed coefficient bounds the compiler overhead for all prefix lengths.
```
lemma quadratic_budget (as : List Symbol) (N B : ℕ) :
    budget as N B≤budget as 1 B*(N+1)^2 := by
…
```
Mentions: OAI.ContingencyTables.ExactPhysicalCost.budget