OAI/Computability/FourierCircuit/TensorCostAlgebra.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.CircuitCost.tensor_comm line 13
  2. theorem OAI.ExactFourier.CircuitCost.tensor_assoc line 18
  3. theorem OAI.ExactFourier.CircuitCost.tensor_sum line 24
  4. theorem OAI.ExactFourier.CircuitCost.tensor_one_le line 32
  5. theorem OAI.ExactFourier.CircuitCost.tensor_punit line 35
  6. theorem OAI.ExactFourier.CircuitCost.tensor_exchange line 40
  7. def OAI.ExactFourier.TensorAxis.funCoordinates line 54
  8. theorem OAI.ExactFourier.TensorAxis.power_entries line 62
  9. theorem OAI.ExactFourier.TensorAxis.power_fun_reindex line 72
  10. def OAI.ExactFourier.TensorAxis.appendCoordinates line 79

    Source documentation

    Grouping changes coordinate indexing only, not the scalar operation.

    def appendCoordinates (k : ℕ) : (l : ℕ)→Space α (k+l)≃(Space α k×Space α l)
 | 0 => (Equiv.prodPUnit _).symm
 | l+1 => ((appendCoordinates k l).prodCongr (Equiv.refl α)).trans (Equiv.prodAssoc _ _ _)

    Mentions: OAI.ExactFourier.TensorAxis.Space

  11. theorem OAI.ExactFourier.TensorAxis.power_append line 83
  12. theorem OAI.ExactFourier.TensorAxis.power_reindex line 98
  13. def OAI.ExactFourier.Amplification.avg line 118

    Source documentation

    Finite dimension-weighted sector average; no random choices enter a circuit.

    def avg (p : ℝ) (f : ℕ→ℝ) : ℕ→ℕ→ℝ
 | 0,r => f r
 | j+1,r => p*avg p f j (r+1)+(1-p)*avg p f j r
  14. theorem OAI.ExactFourier.Amplification.avg_mono line 122
  15. theorem OAI.ExactFourier.Amplification.avg_const_mul line 136
  16. theorem OAI.ExactFourier.Amplification.avg_rpow line 142
  17. def OAI.ExactFourier.Amplification.sectorCost line 170
  18. theorem OAI.ExactFourier.Amplification.cost_sectors line 176
  19. theorem OAI.ExactFourier.Amplification.cost_call_power line 195
  20. theorem OAI.ExactFourier.Amplification.sectorCost_avg line 206
  21. theorem OAI.ExactFourier.TensorAxis.power_group line 228
  22. theorem OAI.ExactFourier.TensorAxis.power_monomial line 243
  23. theorem OAI.ExactFourier.TensorAxis.source_power_reindex line 249
  24. theorem OAI.ExactFourier.Amplification.cost_source_power line 260
  25. theorem OAI.ExactFourier.Amplification.cost_group line 264
  26. theorem OAI.ExactFourier.Amplification.cost_reindexed_power line 269
  27. theorem OAI.ExactFourier.Amplification.complement_card line 275
  28. theorem OAI.ExactFourier.Amplification.cost_word_power line 280
  29. def OAI.ExactFourier.Amplification.normalizedCost line 319
  30. theorem OAI.ExactFourier.Amplification.normalized_add line 322
  31. theorem OAI.ExactFourier.Amplification.normalized_linear line 338
  32. theorem OAI.ExactFourier.Amplification.normalized_word line 345
  33. theorem OAI.ExactFourier.Amplification.normalized_recurrence line 368