OAI/MathematicalPhysics/Boltzmann/Compactness/PhysicalLinearContinuous.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Maxwellian-weighted frequency along all physical flights

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.weighted_frequency_integrable line 27
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.gain_path_integrable line 58
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.gain_path_integrable_full line 85
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.frequency_path_integrable_full line 94
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.flight_integrable_locally line 104
  6. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalLinearProfile line 140
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalLinearProfile_initial line 146
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_absolutelyContinuous line 150
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_eq_source line 168
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_le line 183
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalLinearProfile_nonneg line 207
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_hasDerivAt_ae line 216
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_source_integrable line 234
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalFullPositiveSource_measurable line 260
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_eq_source_full line 266
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_le_full line 274
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_integrable line 282
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_log_gain_bound line 323
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_normalized_gain_paths line 343
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_normalized_gain_integrable_of_slice line 377
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_normalized_gain_integrable line 419
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_normalized_loss_integrable line 448
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_renormalized_tested_paths line 497
  24. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_renormalized_source_integrable line 541
  25. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearRenormalizedField line 580
  26. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_renormalized_field_integrable line 588
  27. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearRenormalizedDensity line 634
  28. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearRenormalizedSource line 638
  29. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_renormalized_integral_paths line 643
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_renormalized_balance_terminal_zero line 675
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_renormalized_traces line 710
  32. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearRenormalizedEvolution line 743
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearRenormalizedEvolution_initial line 747
  34. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_renormalized_eulerian_traces line 753
  35. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalLinearProfile_measurable line 780
  36. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_unit_gain_integrable line 803
  37. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_slice_tendsto line 851