OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveRestrictedChain.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Transverse spatial escape forces the actual positive fifth gain to vanish

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positive_five_transverse_escape_tendsto line 25
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positive_two_gain_axial_tendsto line 76
  3. theorem OAI.BoltzmannNonuniqueness.lintegral_of_ae_tendsto_le line 112
  4. theorem OAI.BoltzmannNonuniqueness.integrable_of_positive_limit_budget line 126
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positive_five_large_velocity_tendsto line 152
  6. def OAI.BoltzmannNonuniqueness.PositiveIteration.deletionCoefficient line 224
  7. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.deletionCoefficient_ne_top line 228
  8. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_deletion_bound line 236
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positive_axial_gain_tendsto line 300
  10. def OAI.BoltzmannNonuniqueness.PositiveIteration.restrictedChain line 358
  11. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.restrictedChain_measurable line 364
  12. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_restrict_slab_mono line 372
  13. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.restrict_add_compl line 385
  14. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.restrictedChain_deletion_bound line 392