OAI/MathematicalPhysics/Boltzmann/Branching/AeKernelHistoryOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere kernel comparison suffices below an occupation measure

  1. theorem OAI.BoltzmannNonuniqueness.KernelHistoryOrder.measure_comp_mono_ae line 18
  2. theorem OAI.BoltzmannNonuniqueness.KernelHistoryOrder.measure_comp_mono_ae_of_le line 27
  3. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.restricted_source_renewal_ae line 38
  4. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.finite_occupation_histories_ae line 47