OAI/MathematicalPhysics/Boltzmann/Compactness/SelectedCoreSelection.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The selected main free core and its uniform positive gain bound

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedColdKernel line 20
  2. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedColdKernel_sFinite line 23
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedFreeKernel line 28
  4. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedFreeKernel_sFinite line 31
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedFreeKernel_bound line 36
  6. def OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMainKernel line 62
  7. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMainKernel_sFinite line 65
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMainKernel_bound line 70
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copyFreeKernel_scale_time_bound line 104
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedFreeKernel_scale_time_bound line 121
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMainKernel_scale_time_bound line 155
  12. def OAI.BoltzmannNonuniqueness.JetCopyDatum.copyCoreDensity line 193
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copyCoreDensity_measurable line 198
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copyColdKernel_density line 203
  15. def OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedCoreDensity line 211
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedCoreDensity_measurable line 216
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedColdKernel_density line 224
  18. theorem OAI.BoltzmannNonuniqueness.ChartKernel.inputKernel_eq_zero_of_base line 267
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedFreeKernel_eq_copy line 278
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedFreeKernel_eq_zero line 290
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedFreeKernel_zero_or_copy line 299