OAI/MathematicalPhysics/Boltzmann/Branching/MainCoreScaleWindow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Measurable regions selecting the unique main periodic core

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreRegion line 19
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.measurableSet_mainCoreRegion line 23
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreRegion_unique line 41
  4. def OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreKernel line 47
  5. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreKernel_sFinite line 52
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreKernel_eq line 58
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreKernel_eq_zero line 72
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.transverse_dilated_origin line 98
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreRegion_scale_radius line 105
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.mainCoreRegion_retained_scale_window line 122