OAI/MathematicalPhysics/Boltzmann/Approximation/CapActualLossDensity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Positivity and local integrability of the full physical cap density

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.physical_nonneg line 21
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.scaled_box_integrable line 26
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_le_value line 59
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.physical_scaled_twice line 69
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_full_bound line 79
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.backward_normalizedHot line 128
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.backward_normalizedSource line 137
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_backward_mild line 146
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_backward_source_integrable line 166
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_backward_between line 204
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_box_mass_comparison line 248
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.incomingRate_integrable line 297
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.incomingGainMeasure_finite line 309
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.incomingLossMeasure_finite line 318
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hotInitial_eq line 344
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotInitial_ratio_bound line 353
  17. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.slab_frequency_measurable line 397
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.loss_density_integrable line 417
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.initial_core_lower line 468
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.loss_measure_density_integral line 524
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.loss_measure_product_integral line 577
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.loss_cylinder_ae line 615
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.actual_loss_cylinder_integrable line 631
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.actual_loss_cylinder_integral line 642