OAI/MathematicalPhysics/Heisenberg/RoutedDissipation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Flow.frameEnergy line 21
  2. lemma OAI.Heisenberg.Flow.frameEnergy_nonneg line 25
  3. lemma OAI.Heisenberg.Flow.test_support_subset line 35
  4. theorem OAI.Heisenberg.Flow.finite_frame_energy line 42
  5. theorem OAI.Heisenberg.Flow.regular_frame_test line 81
  6. def OAI.Heisenberg.Exposure.quietEnergy line 107
  7. abbrev OAI.Heisenberg.SpatialFrame.Slots line 115
  8. def OAI.Heisenberg.SpatialFrame.available line 117
  9. def OAI.Heisenberg.SpatialFrame.extend line 120
  10. lemma OAI.Heisenberg.SpatialFrame.extend_apply line 124
  11. lemma OAI.Heisenberg.SpatialFrame.available_apply line 127
  12. lemma OAI.Heisenberg.SpatialFrame.available_nonempty line 130
  13. lemma OAI.Heisenberg.SpatialFrame.extend_nonneg line 143
  14. lemma OAI.Heisenberg.SpatialFrame.extend_supported line 152
  15. abbrev OAI.Heisenberg.SpatialFrame.Edges line 160
  16. lemma OAI.Heisenberg.SpatialFrame.frame_eq_pairs line 163
  17. theorem OAI.Heisenberg.SpatialFrame.frame_eq_sweep line 189
  18. def OAI.Heisenberg.SpatialFrame.blocked line 207
  19. lemma OAI.Heisenberg.SpatialFrame.blocked_finite line 211
  20. lemma OAI.Heisenberg.SpatialFrame.hole_not_blocked line 215
  21. lemma OAI.Heisenberg.SpatialFrame.available_unblocked line 220
  22. theorem OAI.Heisenberg.Flow.routed_sweep_pair line 228