OAI/MathematicalPhysics/Boltzmann/Branching/EntrySites.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A short three-collision path stays in a bounded region outside the hole

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.nearby_entry_cylinder line 19
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.short_three_flights line 29
  3. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.nearby_beamDensity_lower line 57
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.entrySite₀ line 87
  5. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.entrySite₁ line 90
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.entrySite₂ line 93
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.entrySites_bounded line 96