OAI/MathematicalPhysics/Boltzmann/Branching/SeparatedMeasureTail.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Compact approximation by bounded separated spacetime–velocity tests

  1. def OAI.BoltzmannNonuniqueness.SeparatedTests.atom line 22
  2. def OAI.BoltzmannNonuniqueness.SeparatedTests.eval line 26
  3. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.eval_append line 30
  4. def OAI.BoltzmannNonuniqueness.SeparatedTests.product line 36
  5. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.eval_product line 40
  6. def OAI.BoltzmannNonuniqueness.SeparatedTests.algebra line 59
  7. def OAI.BoltzmannNonuniqueness.SeparatedTests.probe line 75
  8. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.probe_self line 89
  9. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.probe_pos line 91
  10. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.algebra_separatesPoints line 94
  11. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.exists_approximation line 109
  12. def OAI.BoltzmannNonuniqueness.SeparatedTests.cutoff line 136
  13. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.cutoff_mem line 151
  14. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.cutoff_eq_one line 154
  15. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.cutoff_eq_zero line 158
  16. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.exists_global_approximation line 163
  17. def OAI.BoltzmannNonuniqueness.SeparatedTests.evalBound line 220
  18. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.abs_eval_le line 224
  19. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.eval_integrable line 240
  20. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.eval_integral_tendsto line 245
  21. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.compact_test_integral_tendsto line 265
  22. theorem OAI.BoltzmannNonuniqueness.SeparatedTests.compact_test_tendsto_of_eventually_finite line 330