OAI/MathematicalPhysics/Heisenberg/QuietSweeps.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.MeshPair.quietSweep line 29
  2. lemma OAI.Heisenberg.MeshPair.residual_supported line 34
  3. lemma OAI.Heisenberg.MeshPair.quietSweep_supported line 46
  4. def OAI.Heisenberg.MeshPair.maskedGenerator line 53
  5. lemma OAI.Heisenberg.MeshPair.quietSweep_eq line 57
  6. def OAI.Heisenberg.MeshPair.quietEnergy line 75
  7. lemma OAI.Heisenberg.MeshPair.quietEnergy_nonneg line 79
  8. lemma OAI.Heisenberg.MeshPair.masked_dirichlet line 85
  9. theorem OAI.Heisenberg.MeshPair.quietSweep_energy line 102
  10. lemma OAI.Heisenberg.MeshPair.quietSweep_contraction line 122
  11. def OAI.Heisenberg.MeshPair.killedBetween line 136
  12. lemma OAI.Heisenberg.MeshPair.killedBetween_substochastic line 139
  13. lemma OAI.Heisenberg.MeshPair.killedBetween_same line 170
  14. lemma OAI.Heisenberg.MeshPair.killedBetween_transpose line 179
  15. def OAI.Heisenberg.MeshPair.residualBetween line 188
  16. lemma OAI.Heisenberg.MeshPair.residualBetween_substochastic line 193
  17. lemma OAI.Heisenberg.MeshPair.residualBetween_same line 212
  18. lemma OAI.Heisenberg.MeshPair.residualBetween_transpose line 219
  19. lemma OAI.Heisenberg.MeshPair.residualBetween_supported line 229
  20. def OAI.Heisenberg.Exposure.holeCut line 247
  21. lemma OAI.Heisenberg.Exposure.holeCut_transport line 252
  22. lemma OAI.Heisenberg.Exposure.holeCut_quiet line 259
  23. lemma OAI.Heisenberg.Exposure.layerRevealed_swap line 267
  24. def OAI.Heisenberg.Exposure.exposedStep line 281
  25. lemma OAI.Heisenberg.Exposure.exposedStep_quiet line 288
  26. def OAI.Heisenberg.Exposure.exposedSweep line 303
  27. lemma OAI.Heisenberg.Exposure.holeCut_quiet_segment line 311
  28. theorem OAI.Heisenberg.Exposure.exposedSweep_quiet line 323