OAI/MathematicalPhysics/Boltzmann/Collision/VelocityFourierMultiplier.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Nonconcentration of Lebesgue velocities on affine transport hyperplanes

  1. theorem OAI.BoltzmannNonuniqueness.Published.inner_velocity_surjective line 16
  2. theorem OAI.BoltzmannNonuniqueness.Published.affine_velocity_hyperplane_null line 25
  3. theorem OAI.BoltzmannNonuniqueness.Published.evolution_velocity_hyperplane_null line 39
  4. theorem OAI.BoltzmannNonuniqueness.lintegral_velocity_polar line 65
  5. theorem OAI.BoltzmannNonuniqueness.radial_cubic_unit_integral line 85
  6. def OAI.BoltzmannNonuniqueness.Published.velocityMultiplier line 123
  7. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_nonneg line 126
  8. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_le_one line 129
  9. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_continuous line 134
  10. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_antitone line 142
  11. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_tendsto line 152
  12. def OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass line 163
  13. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_integrable line 166
  14. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass_nonneg line 171
  15. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass_antitone line 175
  16. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass_continuous line 195
  17. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass_tendsto line 211
  18. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass_uniform_decay line 230
  19. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_smul line 260
  20. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplier_large_scale line 266
  21. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass_large_scale line 276
  22. theorem OAI.BoltzmannNonuniqueness.Published.velocityMultiplierMass_high_frequency line 281
  23. def OAI.BoltzmannNonuniqueness.Published.complexVelocityMultiplier line 318
  24. theorem OAI.BoltzmannNonuniqueness.Published.complexVelocityMultiplier_norm_sq line 321
  25. theorem OAI.BoltzmannNonuniqueness.Published.complexVelocityMultiplier_norm_le_one line 327
  26. theorem OAI.BoltzmannNonuniqueness.Published.complexVelocityMultiplier_continuous line 333