OAI/MathematicalPhysics/Boltzmann/Branching/TimeSourceCumulative.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere integrable prefixes imply integrability on smaller windows

  1. theorem OAI.BoltzmannNonuniqueness.Published.integrable_window_of_ae_prefix line 21
  2. theorem OAI.BoltzmannNonuniqueness.Published.timePrimitive_eq_interval line 63
  3. theorem OAI.BoltzmannNonuniqueness.Published.timePrimitive_measurable line 76
  4. theorem OAI.BoltzmannNonuniqueness.Published.timePrimitive_integrable line 83
  5. abbrev OAI.BoltzmannNonuniqueness.WeakTime.Phase line 107
  6. def OAI.BoltzmannNonuniqueness.WeakTime.timeSource line 109
  7. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeSource_finite line 112
  8. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeSource_integral line 122
  9. def OAI.BoltzmannNonuniqueness.WeakTime.phaseProjection line 130
  10. theorem OAI.BoltzmannNonuniqueness.WeakTime.phaseProjection_integrable line 133
  11. theorem OAI.BoltzmannNonuniqueness.WeakTime.phaseProjection_test_integral line 142
  12. theorem OAI.BoltzmannNonuniqueness.phaseHalfLine_measure line 184
  13. def OAI.BoltzmannNonuniqueness.timeTranslation line 189
  14. theorem OAI.BoltzmannNonuniqueness.timeTranslation_apply line 192
  15. theorem OAI.BoltzmannNonuniqueness.timeTranslation_halfLine line 195
  16. theorem OAI.BoltzmannNonuniqueness.timeTranslation_interval line 208
  17. theorem OAI.BoltzmannNonuniqueness.integral_timeTranslation_halfLine line 221
  18. theorem OAI.BoltzmannNonuniqueness.integral_timeTranslation_interval line 226
  19. theorem OAI.BoltzmannNonuniqueness.Published.timePrimitive_L1_continuous line 250
  20. def OAI.BoltzmannNonuniqueness.timePaste line 315
  21. theorem OAI.BoltzmannNonuniqueness.kinetic_halfLine_split line 318
  22. theorem OAI.BoltzmannNonuniqueness.timePaste_left_ae line 328
  23. theorem OAI.BoltzmannNonuniqueness.timePaste_right_ae line 335
  24. theorem OAI.BoltzmannNonuniqueness.timePaste_integral line 344
  25. theorem OAI.BoltzmannNonuniqueness.phaseIntervalBetween_measure line 386
  26. theorem OAI.BoltzmannNonuniqueness.timePaste_before_measure_le line 391
  27. theorem OAI.BoltzmannNonuniqueness.timePaste_after_measure_le line 401
  28. theorem OAI.BoltzmannNonuniqueness.timeTranslation_from_interval line 412
  29. theorem OAI.BoltzmannNonuniqueness.timePaste_integrable_bounded line 420
  30. theorem OAI.BoltzmannNonuniqueness.timePaste_property_ae line 438
  31. def OAI.BoltzmannNonuniqueness.Published.timeSpaceVolume line 473
  32. def OAI.BoltzmannNonuniqueness.Published.TimeLocalL1Converges line 476
  33. theorem OAI.BoltzmannNonuniqueness.Published.LocalL1Converges.time_restrict line 480
  34. theorem OAI.BoltzmannNonuniqueness.WeakTime.timeSource_cumulative line 511
  35. theorem OAI.BoltzmannNonuniqueness.WeakTime.cumulative_density_projection line 518