OAI/MathematicalPhysics/Heisenberg/RegularKernels.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Flow.regular_mono_M line 22
  2. theorem OAI.Heisenberg.Flow.regular_injection_energy line 31
  3. def OAI.Heisenberg.SlotMaximum.value line 94
  4. lemma OAI.Heisenberg.SlotMaximum.attained line 97
  5. lemma OAI.Heisenberg.SlotMaximum.dominates line 103
  6. lemma OAI.Heisenberg.SlotMaximum.nonneg line 108
  7. lemma OAI.Heisenberg.SlotMaximum.zero_of_zero line 116
  8. theorem OAI.Heisenberg.SlotMaximum.edge_energy line 123
  9. theorem OAI.Heisenberg.SlotMaximum.pairing_le line 132
  10. def OAI.Heisenberg.SlotMaximum.test line 137
  11. lemma OAI.Heisenberg.SlotMaximum.test_apply line 145
  12. lemma OAI.Heisenberg.RoutedFlow.Network.pairing_square_bound line 155
  13. lemma OAI.Heisenberg.RoutedFlow.Network.pairing_injections line 162
  14. theorem OAI.Heisenberg.RoutedFlow.Network.slot_injection_bound line 174
  15. theorem OAI.Heisenberg.Flow.regular_slot_test line 220
  16. def OAI.Heisenberg.Flow.goodMass line 260
  17. lemma OAI.Heisenberg.Flow.goodMass_nonneg line 264
  18. theorem OAI.Heisenberg.Flow.kernel_pairing_split line 272
  19. theorem OAI.Heisenberg.Flow.regular_kernel_test line 301