OAI/MathematicalPhysics/Boltzmann/Branching/BoundedMeshStep.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A positive first-collision angular cap for bounded incoming velocities

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_bounded_endpoint_cap line 19
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_near_partner_positive line 39
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.exists_separated_beam line 49
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.nearby_partner_distance line 57
  5. theorem OAI.BoltzmannNonuniqueness.Published.dampedLineResolvent_norm_le line 76
  6. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineResolvent_support line 84
  7. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineAverage_norm_le line 90
  8. theorem OAI.BoltzmannNonuniqueness.Published.integrable_bounded_memLp_two line 108
  9. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineAverage_memLp_two line 116
  10. def OAI.BoltzmannNonuniqueness.JetCopyDatum.boundedMeshWeight line 142
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.boundedMeshWeight_measurable line 146
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.boundedMeshWeight_le_one line 153
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.boundedMeshWeight_support line 162
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.boundedMeshWeight_mul line 173
  15. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_restrict_eq_indicator line 193
  16. theorem OAI.BoltzmannNonuniqueness.Published.bounded_integrable_square_le line 216
  17. theorem OAI.BoltzmannNonuniqueness.Published.bounded_average_energy line 230
  18. theorem OAI.BoltzmannNonuniqueness.Published.bounded_average_L2_norm line 243
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScale_restricted_step_eq line 279