OAI/MathematicalPhysics/Boltzmann/Branching/SupportedTensorConvergence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Uniform approximation by products of compactly supported velocity tests

  1. inductive OAI.BoltzmannNonuniqueness.Compactness.IsSupportedTensorSum line 19
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.tensorTest_tsupport_subset line 27
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.tensorTest_hasCompactSupport line 34
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.IsSupportedTensorSum.hasCompactSupport line 39
  5. theorem OAI.BoltzmannNonuniqueness.Compactness.IsTensorSum.cutoff line 47
  6. theorem OAI.BoltzmannNonuniqueness.Compactness.exists_supported_tensorSum_uniform line 63
  7. theorem OAI.BoltzmannNonuniqueness.Compactness.supported_integrable line 114
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.IsSupportedTensorSum.integral_tendsto line 118
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.supported_integral_error line 137
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.supported_integral_tendsto_of_tensor_tests line 145