OAI/MathematicalPhysics/Boltzmann/Branching/BoundedL1Tests.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuity and norm bounds for bounded measurable L¹ tests

  1. theorem OAI.BoltzmannNonuniqueness.Published.abs_integral_bounded_mul line 13
  2. theorem OAI.BoltzmannNonuniqueness.Published.abs_bounded_test_difference line 28
  3. theorem OAI.BoltzmannNonuniqueness.Published.bounded_test_L1_tendsto line 43
  4. theorem OAI.BoltzmannNonuniqueness.Published.scalar_tendsto_of_uniform_approximations line 61