OAI/MathematicalPhysics/Boltzmann/Branching/DampedEndpointHistories.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Each marked event is damped free waiting followed by physical collision

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventKernel_eq_comp line 25
  2. def OAI.BoltzmannNonuniqueness.WeakTime.timeWeightedDensity line 57
  3. def OAI.BoltzmannNonuniqueness.WeakTime.timeWeightedSource line 60
  4. def OAI.BoltzmannNonuniqueness.WeakTime.dampedResidual line 63
  5. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeWeightedDensity_integrable line 66
  6. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeWeightedSource_finite line 71
  7. theorem OAI.BoltzmannNonuniqueness.WeakTime.time_phase_integrable line 79
  8. theorem OAI.BoltzmannNonuniqueness.WeakTime.ae_damped_measure_interval_balance line 90
  9. theorem OAI.BoltzmannNonuniqueness.WeakTime.positiveDensityMeasure_const_mul line 185
  10. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeWeighted_phaseSlice line 195
  11. theorem OAI.BoltzmannNonuniqueness.WeakTime.phaseIncrement_add line 203
  12. theorem OAI.BoltzmannNonuniqueness.WeakTime.undamp_measure_balance line 208
  13. theorem OAI.BoltzmannNonuniqueness.WeakTime.undamp_measure_balance_add line 225
  14. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_mediumEventKernel_remaining_le line 251
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_mediumEventKernel_pow_eq_comp line 270
  16. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedPhysicalEvent line 307
  17. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedPhysicalEvent_sFinite line 311
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_boundedMediumEventKernel_eq_physical line 316
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_boundedMediumEventKernel_remaining_le line 322
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_boundedMediumEventKernel_pow_eq_physical line 328
  21. def OAI.BoltzmannNonuniqueness.WeakTime.dampedSourceIncrement line 364
  22. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedSourceIncrement_lintegral line 367
  23. def OAI.BoltzmannNonuniqueness.WeakTime.residenceWeight line 412
  24. theorem OAI.BoltzmannNonuniqueness.WeakTime.residenceWeight_measurable line 416
  25. def OAI.BoltzmannNonuniqueness.WeakTime.residenceKernel line 423
  26. instance OAI.BoltzmannNonuniqueness.WeakTime.residenceKernel_sFinite line 427
  27. theorem OAI.BoltzmannNonuniqueness.WeakTime.residenceKernel_lintegral line 439
  28. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeWeightedSource_add line 477
  29. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeWeightedSource_density line 481
  30. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedResidual_source line 494
  31. theorem OAI.BoltzmannNonuniqueness.WeakTime.undamp_combined_source_balance line 500
  32. def OAI.BoltzmannNonuniqueness.WeakTime.phaseSeed line 530
  33. instance OAI.BoltzmannNonuniqueness.WeakTime.phaseSeed_sFinite line 533
  34. theorem OAI.BoltzmannNonuniqueness.WeakTime.residence_seed_lintegral line 537
  35. def OAI.BoltzmannNonuniqueness.WeakTime.phaseEndpointKernel line 572
  36. instance OAI.BoltzmannNonuniqueness.WeakTime.phaseEndpointKernel_sFinite line 576
  37. theorem OAI.BoltzmannNonuniqueness.WeakTime.phaseEndpointKernel_lintegral line 579
  38. theorem OAI.BoltzmannNonuniqueness.WeakTime.endpoint_source_comp line 589
  39. theorem OAI.BoltzmannNonuniqueness.WeakTime.endpoint_seed_comp line 603
  40. theorem OAI.BoltzmannNonuniqueness.WeakTime.triangular_time_integral line 632
  41. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedSource_time_integral line 674
  42. theorem OAI.BoltzmannNonuniqueness.WeakTime.occupation_eq_residence line 744
  43. theorem OAI.BoltzmannNonuniqueness.WeakTime.endpoint_finite_histories line 782