OAI/Computability/FourierCircuit/CascadeLimit.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The real limit used by the cascade-to-corner argument. Only the fixed real prices are compared; no continuity of a price functional is used.

  1. def OAI.ExactFourier.cascadeError line 11
  2. theorem OAI.ExactFourier.cascadeError_tendsto line 15
  3. theorem OAI.ExactFourier.fixed_price_of_cascade line 39
  4. theorem OAI.ExactFourier.MatrixPrice.corner_block line 66
  5. theorem OAI.ExactFourier.MatrixPrice.submatrix_equiv line 112
  6. def OAI.ExactFourier.extendInjection line 135
  7. theorem OAI.ExactFourier.extendInjection_inl line 142
  8. theorem OAI.ExactFourier.MatrixPrice.corner line 150
  9. theorem OAI.ExactFourier.MatrixPrice.le_shear line 178
  10. theorem OAI.ExactFourier.TypedDAG.price line 188
  11. def OAI.ExactFourier.TypedDAG.weightedBlocks line 205
  12. def OAI.ExactFourier.TypedDAG.blockMatrix line 210
  13. theorem OAI.ExactFourier.TypedDAG.size_weightedBlocks line 213
  14. theorem OAI.ExactFourier.TypedDAG.eval_weightedBlocks line 219
  15. def OAI.ExactFourier.TypedDAG.addIdentity line 230
  16. theorem OAI.ExactFourier.TypedDAG.size_addIdentity line 232
  17. theorem OAI.ExactFourier.TypedDAG.eval_addIdentity line 235
  18. theorem OAI.ExactFourier.Boundary.exists_tensor_coefficient_dag line 253
  19. abbrev OAI.ExactFourier.Boundary.Times line 296
  20. theorem OAI.ExactFourier.Boundary.card_times line 298
  21. def OAI.ExactFourier.Boundary.timeActiveSplit line 325
  22. def OAI.ExactFourier.Boundary.activeMatrix line 332
  23. theorem OAI.ExactFourier.Boundary.active_split line 336
  24. theorem OAI.ExactFourier.Boundary.active_price line 355