OAI/MathematicalPhysics/Boltzmann/Branching/OffAxisBoxExhaustion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Choosing a bounded representative of a collision kernel on the null axis

  1. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurableSet_offAxis line 21
  2. def OAI.BoltzmannNonuniqueness.ChartKernel.offAxis line 26
  3. instance OAI.BoltzmannNonuniqueness.ChartKernel.offAxis_sFinite line 30
  4. theorem OAI.BoltzmannNonuniqueness.ChartKernel.offAxis_apply line 36
  5. theorem OAI.BoltzmannNonuniqueness.ChartKernel.offAxis_axis line 41
  6. theorem OAI.BoltzmannNonuniqueness.ChartKernel.offAxis_ae line 46
  7. theorem OAI.BoltzmannNonuniqueness.ChartKernel.action_offAxis_ae line 70
  8. theorem OAI.BoltzmannNonuniqueness.ChartKernel.action_offAxis_normalized_congr_ae line 79
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.ae_zero_time_slab_of_boxes line 105