OAI/MathematicalPhysics/Boltzmann/Branching/CompactParameterConvergence.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Compact time primitives for the characteristic weak equation

  1. def OAI.BoltzmannNonuniqueness.WeakTime.primitive line 21
  2. theorem OAI.BoltzmannNonuniqueness.WeakTime.primitive_hasDerivAt line 23
  3. theorem OAI.BoltzmannNonuniqueness.WeakTime.primitive_deriv line 28
  4. theorem OAI.BoltzmannNonuniqueness.WeakTime.primitive_contDiff line 33
  5. theorem OAI.BoltzmannNonuniqueness.WeakTime.primitive_eq_zero_left line 40
  6. theorem OAI.BoltzmannNonuniqueness.WeakTime.primitive_eq_zero_right line 52
  7. theorem OAI.BoltzmannNonuniqueness.WeakTime.primitive_support line 61
  8. theorem OAI.BoltzmannNonuniqueness.WeakTime.primitive_compact line 72
  9. theorem OAI.BoltzmannNonuniqueness.WeakTime.exists_test_primitive line 77
  10. def OAI.BoltzmannNonuniqueness.Compactness.tensorTest line 127
  11. inductive OAI.BoltzmannNonuniqueness.Compactness.IsTensorSum line 131
  12. theorem OAI.BoltzmannNonuniqueness.Compactness.IsTensorSum.mul line 137
  13. def OAI.BoltzmannNonuniqueness.Compactness.tensorAlgebra line 156
  14. theorem OAI.BoltzmannNonuniqueness.Compactness.tensorAlgebra_separates line 173
  15. theorem OAI.BoltzmannNonuniqueness.Compactness.exists_tensorSum_near_compact line 184
  16. theorem OAI.BoltzmannNonuniqueness.Compactness.test_integrable line 213
  17. theorem OAI.BoltzmannNonuniqueness.Compactness.IsTensorSum.integral_tendsto line 217
  18. theorem OAI.BoltzmannNonuniqueness.Compactness.integral_test_error line 235
  19. theorem OAI.BoltzmannNonuniqueness.Compactness.integral_tendsto_of_tensor_tests line 242
  20. theorem OAI.BoltzmannNonuniqueness.Compactness.tendsto_integral_mul_common_support line 295
  21. theorem OAI.BoltzmannNonuniqueness.GainPullback.uniform_on_compact_of_joint_continuous line 342
  22. theorem OAI.BoltzmannNonuniqueness.GainPullback.uniform_on_compact_of_joint_restriction line 356