OAI/MathematicalPhysics/Boltzmann/Branching/RationalUniformApproximation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Bounded rational renormalizations increasing to the identity

  1. def OAI.BoltzmannNonuniqueness.Renormalization.rationalFunction line 14
  2. theorem OAI.BoltzmannNonuniqueness.Renormalization.rationalFunction_hasDerivAt line 16
  3. theorem OAI.BoltzmannNonuniqueness.Renormalization.rationalFunction_derivWithin line 26
  4. def OAI.BoltzmannNonuniqueness.Renormalization.rational line 31
  5. theorem OAI.BoltzmannNonuniqueness.Renormalization.rational_nonneg line 46
  6. theorem OAI.BoltzmannNonuniqueness.Renormalization.rational_le_self line 50
  7. theorem OAI.BoltzmannNonuniqueness.Renormalization.rational_le_parameter line 56
  8. theorem OAI.BoltzmannNonuniqueness.Renormalization.rational_error line 62
  9. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_rational_eq line 81
  10. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_rational_error line 88
  11. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_rational_bounds line 95
  12. theorem OAI.BoltzmannNonuniqueness.Renormalization.weighted_rational_error_le line 102
  13. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.maxwellianLower line 131
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.maxwellianLower_pos line 134
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.maxwellianLower_le line 138
  16. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.rationalApproximation line 145
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rationalApproximation_measurable line 148
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rationalApproximation_error line 154
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rationalApproximation_L1_bound line 186
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rationalApproximation_uniform_L1 line 223