OAI/MathematicalPhysics/Boltzmann/Compactness/L1TruncationCauchy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Countably many L² approximations with uniform vanishing L¹ errors

  1. def OAI.BoltzmannNonuniqueness.Published.truncationError line 14
  2. theorem OAI.BoltzmannNonuniqueness.Published.truncationError_pos line 16
  3. theorem OAI.BoltzmannNonuniqueness.Published.truncationError_tendsto line 20
  4. structure OAI.BoltzmannNonuniqueness.Published.L1TruncationFamily line 25
  5. theorem OAI.BoltzmannNonuniqueness.Published.exists_L1TruncationFamily line 35
  6. theorem OAI.BoltzmannNonuniqueness.Published.integral_abs_le_of_eLpNorm_le line 81
  7. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationFamily.integrable line 94
  8. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationFamily.difference_error line 97
  9. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationFamily.difference_integral line 111
  10. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationFamily.exists_limits line 119
  11. structure OAI.BoltzmannNonuniqueness.Published.L1TruncationLimit line 145
  12. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationLimit.integrable line 157
  13. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationLimit.difference_integral line 160
  14. def OAI.BoltzmannNonuniqueness.Published.L1TruncationLimit.l1Value line 184
  15. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationLimit.l1Value_dist line 186
  16. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationLimit.cauchy line 199
  17. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationLimit.exists_L1_limit line 207
  18. theorem OAI.BoltzmannNonuniqueness.Published.L1TruncationFamily.exists_limit line 212