OAI/MathematicalPhysics/Boltzmann/Jets/ColdCentralVanishing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Compact cold cylinders and their exhaustion away from the axis

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderVolume line 22
  2. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderVolume_finite line 26
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldAxisCutoff line 33
  4. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldTransverseAnnulus line 36
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldTransverseAnnulus_compact line 39
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldAxisCutoff_measurable line 44
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderVolume_restrict_axis line 47
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldAxisCutoff_exhausts line 62
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderVolume_le_hotBaseWindowVolume line 87
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.cold_spatial_box_eq_ball line 117
  11. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderSet line 125
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderSet_measurable line 128
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderVolume_eq line 131
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldCylinderVolume_eq_hot_restrict line 141
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.physical_weak_cylinder line 158
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.cold_central_bound line 181