OAI/MathematicalPhysics/Boltzmann/Approximation/CapAnnularMassGrowth.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The actual hot occupation measure satisfies the positive renewal equation

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.characteristic_occupation_equation line 39
  2. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.localHistoryKernel line 106
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.characteristic_finite_occupation_histories line 112
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.characteristic_finite_endpoint_histories line 168
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.characteristic_localized_measure_balance line 246
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.localizedNormalBeam_le_retained_ae line 311
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.characteristic_comparison_endpoint_histories line 358
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.covered_comparison_endpoint_histories line 442
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.localized_normal_endpoint_histories line 533
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLateBoxMass_cap line 589
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLateBoxMass_finite line 606
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.hotLateBoxMass_real_cap line 613
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.covered_normal_endpoint_histories line 639
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.positive_history_transfer line 693
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.entry_window line 751
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.exists_actual_entry line 857
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.persisting_entry line 924
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.window_mass_growth_from_blocks line 1013
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.annular_growth_parameters line 1064
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.uniform_late_zero_parameters line 1153
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.annular_mass_growth line 1247