OAI/MathematicalPhysics/Boltzmann/Branching/MainPositiveRemainderBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Positive iteration of the selected main-core collision kernel

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_action line 21
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_action_congr_ae line 30
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.iterate_positiveMain_congr_ae line 45
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.iterate_positiveMain_congr_ae_at line 60
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.iterate_positiveMain_bound line 73
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_action_mono_ae line 104
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.step_positiveMain_mono_ae line 118
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.step_positiveMain_mono_ae_at line 133
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.iterate_positiveMain_mono_ae line 148
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_residual_ae line 179
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_residual_ae_at line 202
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_residual_on_slab line 252
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.scaled_flight_distance_le line 302
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.main_collision_same_origin line 312
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_constant_sum_bound line 340
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.positiveMain_constant_sum_uniform line 379