OAI/MathematicalPhysics/Boltzmann/Jets/JetColdLimitComparison.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Gaussian control of the actual finite annular datum

  1. def OAI.BoltzmannNonuniqueness.JetFiniteGaussian.indices line 22
  2. def OAI.BoltzmannNonuniqueness.JetFiniteGaussian.coefficient line 24
  3. def OAI.BoltzmannNonuniqueness.JetFiniteGaussian.amplitude line 27
  4. theorem OAI.BoltzmannNonuniqueness.JetFiniteGaussian.truncated_eq_sum line 30
  5. theorem OAI.BoltzmannNonuniqueness.JetFiniteGaussian.coefficient_nonneg line 44
  6. theorem OAI.BoltzmannNonuniqueness.JetFiniteGaussian.amplitude_pos line 51
  7. theorem OAI.BoltzmannNonuniqueness.JetFiniteGaussian.term_bound line 58
  8. theorem OAI.BoltzmannNonuniqueness.JetFiniteGaussian.truncated_bound line 87
  9. theorem OAI.BoltzmannNonuniqueness.JetDampedSupersolution.envelope_integrable line 120
  10. theorem OAI.BoltzmannNonuniqueness.JetDampedSupersolution.cutoff_integral_bound line 146
  11. def OAI.BoltzmannNonuniqueness.JetFiniteLocal.liftToTorus line 182
  12. def OAI.BoltzmannNonuniqueness.JetFiniteLocal.seed line 185
  13. theorem OAI.BoltzmannNonuniqueness.JetFiniteLocal.measurable_seed line 188
  14. theorem OAI.BoltzmannNonuniqueness.JetFiniteLocal.seed_bound line 201
  15. theorem OAI.BoltzmannNonuniqueness.JetFiniteLocal.exists_local line 209
  16. theorem OAI.BoltzmannNonuniqueness.JetColdComparison.step_le line 246
  17. theorem OAI.BoltzmannNonuniqueness.JetColdComparison.picard_le line 321
  18. theorem OAI.BoltzmannNonuniqueness.JetColdComparison.limit_le line 348