OAI/MathematicalPhysics/Boltzmann/Jets/GeometricAnnularFrequency.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual geometric cold coefficients are close throughout a short physical cylinder

  1. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beam_near_on_cylinder line 22
  2. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.cylinder_small_of_density_scale line 67
  3. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.exists_characteristic_cutoff_near_clock line 94
  4. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_damped_bounded_block_growth line 149
  5. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_damped_finite_block_growth line 198
  6. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_finite_block_growth line 247
  7. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.annular_frequency_bound line 293