OAI/MathematicalPhysics/Boltzmann/Jets/OriginMeshLimit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The cost of removing collisions close to a transverse origin

  1. def OAI.BoltzmannNonuniqueness.PositiveIteration.nearOriginRegion line 22
  2. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.nearOriginRegion_measurable line 25
  3. def OAI.BoltzmannNonuniqueness.PositiveIteration.nearOriginKernel line 31
  4. def OAI.BoltzmannNonuniqueness.PositiveIteration.awayOriginKernel line 36
  5. instance OAI.BoltzmannNonuniqueness.PositiveIteration.nearOriginKernel_sFinite line 41
  6. instance OAI.BoltzmannNonuniqueness.PositiveIteration.awayOriginKernel_sFinite line 46
  7. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.originKernel_decomposition line 51
  8. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_nearOrigin_bound line 58
  9. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.finiteGainChain_measurable line 125
  10. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_slab_congr line 136
  11. def OAI.BoltzmannNonuniqueness.JetCopyDatum.meshFamily line 147
  12. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.meshFamily_sFinite line 152
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.meshFamily_apply line 157
  14. def OAI.BoltzmannNonuniqueness.JetCopyDatum.meshWeights line 166
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScale_chain_eq_mesh line 170
  16. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.restrictedChain_origin_deletion line 224
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.origin_scale_five_tendsto line 315