OAI/MathematicalPhysics/Boltzmann/Branching/TranslatedCoreKernel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Dilated free kernels for the actual periodic labels

  1. theorem OAI.BoltzmannNonuniqueness.ChartKernel.inputKernel_congr_base line 16
  2. def OAI.BoltzmannNonuniqueness.JetCopyDatum.latticeVector line 27
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.copyColdKernel line 29
  4. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.copyColdKernel_sFinite line 34
  5. def OAI.BoltzmannNonuniqueness.JetCopyDatum.copyFreeKernel line 39
  6. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.copyFreeKernel_sFinite line 42
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copyFreeKernel_eq line 47
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copyFreeKernel_bound line 62