OAI/MathematicalPhysics/Boltzmann/Branching/ZeroProfileParameters.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A polynomial zero-seed supersolution uniform in the smallest jet scale

  1. def OAI.BoltzmannNonuniqueness.ZeroProfile.profile line 17
  2. def OAI.BoltzmannNonuniqueness.ZeroProfile.source line 19
  3. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.source_le_derivative line 21
  4. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.profile_hasDerivAt line 47
  5. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.integral_supersolution line 71
  6. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.source_difference line 117
  7. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.le_profile line 154
  8. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.profile_le_square line 187
  9. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.small_product line 217
  10. theorem OAI.BoltzmannNonuniqueness.ZeroProfile.parameters_exist line 223