OAI/MathematicalPhysics/Boltzmann/Branching/SeedEscapeMeasure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Uniform free-flight escape of the bounded nonaxial seed

  1. theorem OAI.BoltzmannNonuniqueness.seed_flight_bounds line 21
  2. theorem OAI.BoltzmannNonuniqueness.seed_flight_radius_linear line 42
  3. theorem OAI.BoltzmannNonuniqueness.seed_flight_outside line 56
  4. theorem OAI.BoltzmannNonuniqueness.seed_flight_geometric_scale line 70
  5. def OAI.BoltzmannNonuniqueness.seedPhaseBump line 112
  6. def OAI.BoltzmannNonuniqueness.seedPhaseCutoff line 115
  7. theorem OAI.BoltzmannNonuniqueness.seedPhaseCutoff_smooth line 117
  8. theorem OAI.BoltzmannNonuniqueness.seedPhaseCutoff_compact line 120
  9. theorem OAI.BoltzmannNonuniqueness.seedPhaseCutoff_mem line 123
  10. theorem OAI.BoltzmannNonuniqueness.seedPhaseCutoff_one line 127
  11. theorem OAI.BoltzmannNonuniqueness.phaseSlice_weight_le line 134
  12. theorem OAI.BoltzmannNonuniqueness.phaseSlice_weight_apply_eq line 143
  13. def OAI.BoltzmannNonuniqueness.seedEscapeRegion line 171
  14. theorem OAI.BoltzmannNonuniqueness.seedEscapeRegion_measurable line 174
  15. theorem OAI.BoltzmannNonuniqueness.seed_mass_escapes line 179