OAI/MathematicalPhysics/Heisenberg/PolynomialLimits.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Schedule.phaseHom line 17
  2. lemma OAI.Heisenberg.Schedule.phaseHom_sub line 25
  3. def OAI.Heisenberg.Schedule.reverseIndex line 30
  4. lemma OAI.Heisenberg.Schedule.reverseIndex_next line 36
  5. lemma OAI.Heisenberg.Schedule.reverseIndex_prev line 42
  6. lemma OAI.Heisenberg.Schedule.reverse_phase_spatial line 52
  7. lemma OAI.Heisenberg.Schedule.reverse_phase_completion line 67
  8. lemma OAI.Heisenberg.MeshPair.prefix_cons line 99
  9. lemma OAI.Heisenberg.MeshPair.prefix_congr line 106
  10. lemma OAI.Heisenberg.MeshPair.prefix_reverse line 112
  11. lemma OAI.Heisenberg.MeshPair.squareNorm_toLp line 129
  12. lemma OAI.Heisenberg.MeshPair.energy_two_prefixes line 132
  13. lemma OAI.Heisenberg.Schedule.reverse_run line 172
  14. lemma OAI.Heisenberg.Schedule.reverse_predecessor line 177
  15. lemma OAI.Heisenberg.Exposure.layerSum_reverse line 196
  16. lemma OAI.Heisenberg.Exposure.reversed_period_sweep line 211
  17. lemma OAI.Heisenberg.Pin.nonzero_uniform_limit_disk line 236
  18. lemma OAI.Heisenberg.Pin.polynomial_disk line 270
  19. theorem OAI.Heisenberg.Pin.polynomial_nonvanishing_limit line 292