OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveEndpointHistory.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Axial spatial escape forces the actual positive fifth gain to vanish

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positive_five_axial_escape_tendsto line 25
  2. theorem OAI.BoltzmannNonuniqueness.WeakTime.exists_nonzero_phaseSlice line 75
  3. theorem OAI.BoltzmannNonuniqueness.WeakTime.exists_positive_seed_slice line 92
  4. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_unit_factorial_bound line 122
  5. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.sum_iterate_const_le_exp line 136
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_exponential_bound line 159
  7. theorem OAI.BoltzmannNonuniqueness.positive_endpoint_of_pointwise line 201
  8. theorem OAI.BoltzmannNonuniqueness.single_endpoint_history_le line 216
  9. theorem OAI.BoltzmannNonuniqueness.covered_hot_positive_history line 228