OAI/MathematicalPhysics/Boltzmann/Branching/PhaseDecompositionNorm.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

The essential supremum norm along free transport

  1. def OAI.BoltzmannNonuniqueness.PhaseEssSup.size line 20
  2. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_nonneg line 22
  3. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_le line 24
  4. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_difference line 31
  5. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_flight line 45
  6. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.time_difference line 51
  7. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.continuousOn_size line 83
  8. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.continuousOn_ratio line 102
  9. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.ratio_attains_max line 111
  10. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.ae_abs_le_size line 138
  11. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_le_ae line 145
  12. def OAI.BoltzmannNonuniqueness.PhaseEssSup.canonical line 153
  13. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.measurable_canonical line 156
  14. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.canonical_bounds line 160
  15. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.canonical_ae_at_time line 165
  16. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_difference_ae line 189
  17. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.hot_difference_ae line 204
  18. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.value_le_ae line 262
  19. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.mild_size_le line 292
  20. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.time_idempotent line 327
  21. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.continuous_size line 331
  22. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.canonical_ae line 349
  23. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_congr_ae line 372
  24. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.continuous_size_of_mildAE line 376
  25. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.mild_size_le_of_ae line 394
  26. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_le_cold_add_hot line 430