OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicLinearApproximation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The gain discrepancy against the actual linear characteristic profile

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_gain_discrepancy_L1 line 23
  2. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearComparisonError line 89
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearComparisonError_measurable line 97
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearComparisonError_nonneg line 109
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.positive_linear_comparison line 115
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_loss_residual_L1 line 181
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_comparison_error_L1 line 201
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_positive_difference_L1 line 253
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_approximation_L1 line 319
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_density_strong line 367