OAI/Computability/FourierCircuit/AmplificationMaster.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.Amplification.saving_exponent line 10
  2. theorem OAI.ExactFourier.Amplification.recurrence_bound line 19
  3. theorem OAI.ExactFourier.Amplification.tensor_amplification line 97

    Source documentation

    Tensor amplification for the literal finite winning word, with charged scalars.

    theorem tensor_amplification {q b : ℕ} (A : Matrix (Fin q) (Fin q) ℂ)
 (hb : 2≤b) (W : List (WordStep A (q^b))) (hW : wordMatrix W=tensorPower A b)
 (hw : wordCalls W<b*q^(b-1)) :
 ∃ a C : ℝ,0<a ∧ a<1 ∧ 0<C ∧ ∀ k,
 (cost (power A k) : ℝ)≤C*(q : ℝ)^k*(k+1 : ℝ)^a := by
…

    Mentions: OAI.ExactFourier.WordStep, OAI.ExactFourier.wordMatrix, OAI.ExactFourier.tensorPower, OAI.ExactFourier.wordCalls

  4. inductive OAI.ExactFourier.AParallel line 138

    Source documentation

    A disjoint union of forward calls and untouched coordinates.

    inductive AParallel : {α : Type}→ [Fintype α]→ [DecidableEq α]→Matrix α α ℂ→Prop
 | identity {α : Type} [Fintype α] [DecidableEq α] : AParallel (1 : Matrix α α ℂ)
 | atom : AParallel A
 | reindex {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
   (e : α≃β) {M : Matrix α α ℂ} (h : AParallel M) : AParallel (Matrix.reindex e e M)
 | sum {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
   {M : Matrix α α ℂ} {N : Matrix β β ℂ} (hM : AParallel M) (hN : AParallel N) :
   AParallel (Matrix.fromBlocks M 0 0 N)

variable {A} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
namespace AParallel
  5. theorem OAI.ExactFourier.AParallel.embed line 149
  6. structure OAI.ExactFourier.AFrame line 153
  7. theorem OAI.ExactFourier.AFrame.mono line 157
  8. theorem OAI.ExactFourier.AFrame.atom_mono line 159
  9. theorem OAI.ExactFourier.AFrame.reindex line 161
  10. theorem OAI.ExactFourier.AFrame.sum line 165
  11. def OAI.ExactFourier.AGenerated line 172
  12. theorem OAI.ExactFourier.AGenerated.identity line 176
  13. theorem OAI.ExactFourier.AGenerated.frame line 182
  14. theorem OAI.ExactFourier.AGenerated.mono line 184
  15. theorem OAI.ExactFourier.AGenerated.mul line 186
  16. theorem OAI.ExactFourier.AGenerated.weaken line 196
  17. theorem OAI.ExactFourier.AGenerated.reindex line 200
  18. theorem OAI.ExactFourier.AGenerated.sum line 210
  19. theorem OAI.ExactFourier.AGenerated.embed line 219
  20. theorem OAI.ExactFourier.AGenerated.from_pattern line 223
  21. def OAI.ExactFourier.ParallelTensorCost.Good line 246
  22. theorem OAI.ExactFourier.ParallelTensorCost.Good.reindex line 249
  23. theorem OAI.ExactFourier.ParallelTensorCost.Good.parallel line 257
  24. def OAI.ExactFourier.PiTensor.splitFirst line 310
  25. theorem OAI.ExactFourier.PiTensor.splitFirst_matrix line 316
  26. theorem OAI.ExactFourier.PiTensor.monomial line 325
  27. theorem OAI.ExactFourier.ParallelTensorCost.pi_good line 348
  28. theorem OAI.ExactFourier.ParallelTensorCost.pi_cost line 373