OAI/MathematicalPhysics/Boltzmann/Branching/SmoothTestFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Countably many compact smooth cutoffs covering an open spacetime region

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.exists_spacetime_cutoff_cover line 21
  2. abbrev OAI.BoltzmannNonuniqueness.Compactness.SupportedTest line 73
  3. instance OAI.BoltzmannNonuniqueness.Compactness.(instance at line 77) line 77
  4. instance OAI.BoltzmannNonuniqueness.Compactness.(instance at line 80) line 80
  5. def OAI.BoltzmannNonuniqueness.Compactness.supportedSeq line 83
  6. def OAI.BoltzmannNonuniqueness.Compactness.supportedFn line 86
  7. def OAI.BoltzmannNonuniqueness.Compactness.smoothTest line 88
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.smoothTest_smooth line 91
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.smoothTest_compact line 94
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.exists_countable_smooth_determining_tests line 98