OAI/MathematicalPhysics/Boltzmann/Approximation/SurvivalProfile.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A positive-measure region reached from the fixed initial hot core

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalCore line 17
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalCore_open line 22
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalCore_nonempty line 31
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalCore_positive_measure line 41
  5. theorem OAI.BoltzmannNonuniqueness.Published.initialSurvival_le_twoTimeSurvival line 74
  6. theorem OAI.BoltzmannNonuniqueness.Published.survival_source_unweight line 82
  7. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalProfile line 116
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalProfile_measurable line 120
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalProfile_nonneg line 126
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.survivalProfile_pos line 134