OAI/MathematicalPhysics/Boltzmann/Jets/GeometricEntry.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Actual cold partners and densities at the three entry collisions

  1. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryPartner₀ line 25
  2. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryDensity₀ line 28
  3. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryPartner₁ line 31
  4. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryDensity₁ line 34
  5. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryPartner₂ line 37
  6. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryDensity₂ line 42
  7. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryAngularMass line 47
  8. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryPartner₀_error line 57
  9. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryPartner₁_error line 62
  10. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryPartner₂_error line 67
  11. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryMark line 91
  12. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryMark_ne_zero line 93
  13. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryMark_child line 97
  14. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryMark_rate line 108
  15. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.mediumPoint_entry₀ line 119
  16. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.mediumPoint_entry₁ line 123
  17. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.mediumPoint_entry₂ line 131
  18. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_entry_lower line 157
  19. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryAccess_measurable line 238
  20. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryAngularMass_measurable line 285
  21. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryVelocity₀ line 317
  22. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryVelocity₁ line 320
  23. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryVelocity₂ line 324
  24. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryState₁ line 328
  25. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryState₂ line 332
  26. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryState₃ line 337
  27. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryState_first line 342
  28. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryState_second line 350
  29. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryState_third line 359
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalParameterWeight_wait_eq line 385
  31. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryRate_first line 400
  32. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryRate_second line 411
  33. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryRate_third line 425
  34. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryTerminal line 457
  35. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryTerminal_measurable line 460
  36. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entry_integrand_eq line 465
  37. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryTimeMass line 514
  38. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryTimeMass_pos line 517
  39. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryAngularMass_sphere line 568
  40. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryTimeMass_le_history line 603
  41. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_entry_history_positive line 622
  42. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryTimeMass_le_beam_history line 638
  43. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_beam_entry_positive line 670
  44. def OAI.BoltzmannNonuniqueness.GeometricBackground.entryRegion line 708
  45. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.entryRegion_measurable line 711
  46. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_entry_measure_positive line 715
  47. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamDensity_mul_unit line 752
  48. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beam_gain_rate_scaling line 757
  49. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beam_marked_collision_scaling line 779
  50. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beam_collision_scaling line 789
  51. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beam_event_scaling line 799
  52. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.active_ae_velocity line 829
  53. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.active_ae_characteristic line 836
  54. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.background_eq_beamMeasure_ae_characteristic line 852
  55. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beam_history_scaling line 883
  56. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_density_entry_positive line 903