OAI/MathematicalPhysics/Boltzmann/Compactness/RenormalizedIntegrability.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Measurability and integrability of the renormalized collision source

  1. theorem OAI.BoltzmannNonuniqueness.Renormalization.measurable_derivative_comp line 32
  2. theorem OAI.BoltzmannNonuniqueness.Renormalization.derivative_mul_integrable line 39
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.change_normalizer_bound line 63
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_change_normalizer line 82
  5. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_measurable line 122
  6. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_integrable line 131
  7. theorem OAI.BoltzmannNonuniqueness.renormalizedIntegrand_integrable line 141
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.density_over_renormalization_le line 189
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.renormalized_loss_bound line 197
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integrable_maxwellian_firstMoment line 218
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.renormalized_loss_integrable line 242
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.renormalized_loss_uniformIntegrable line 286
  13. theorem OAI.BoltzmannNonuniqueness.gain_le_loss_add_extendedProduction line 358
  14. theorem OAI.BoltzmannNonuniqueness.weighted_gain_le_loss_add_extendedProduction line 378
  15. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_uniformIntegrable line 413
  16. theorem OAI.BoltzmannNonuniqueness.Renormalization.derivative_uniformIntegrable line 429
  17. theorem OAI.BoltzmannNonuniqueness.Renormalization.chain_rule line 468
  18. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_chain_rule line 489
  19. theorem OAI.BoltzmannNonuniqueness.gain_le_scaled_loss_add_entropy line 525
  20. theorem OAI.BoltzmannNonuniqueness.gain_le_scaled_loss_add_extendedProduction line 545
  21. theorem OAI.BoltzmannNonuniqueness.scaled_entropy_cost_tendsto line 564
  22. def OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPreRate line 585
  23. def OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPostRate line 589
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPreRate_measurable line 593
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPostRate_measurable line 601
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPreRate_nonneg line 609
  27. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPreRate_integral line 613
  28. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPreRate_integrable line 622
  29. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPostRate_nonneg line 659
  30. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPostRate_entropy_bound line 666
  31. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPostRate_integrable line 686
  32. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedPostRate_integral line 718
  33. theorem OAI.BoltzmannNonuniqueness.Renormalization.tested_chain_rule line 741
  34. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_tested_chain_rule line 770
  35. theorem OAI.BoltzmannNonuniqueness.Renormalization.integral_path_data line 811
  36. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_integral_path line 822
  37. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_tested_integral_path line 831
  38. theorem OAI.BoltzmannNonuniqueness.Renormalization.localized_integral_path line 857
  39. theorem OAI.BoltzmannNonuniqueness.Renormalization.derivative_comp_aestronglyMeasurable line 910
  40. theorem OAI.BoltzmannNonuniqueness.Renormalization.derivative_mul_integrable_of_normalized line 922
  41. theorem OAI.BoltzmannNonuniqueness.KineticTest.weighted_slice_integrable line 956
  42. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_integrable_of_ae line 985