OAI/NumberTheory/TwoPoint/Walks/WeightedWordBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Size and coefficient budgets for the actual finite-word expansion.

  1. lemma OAI.TwoPointCorrelations.weightedWord_coefficient_budget line 9
  2. lemma OAI.TwoPointCorrelations.weightedStateCircuit_size_budget line 44