OAI/MathematicalPhysics/Boltzmann/Branching/RestrictedCone.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds and kernel decompositions for restricted collision chains

  1. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_restrict_le line 18
  2. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.kernel_restrict_add line 25
  3. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.restrictedChain_uniform_bound line 32
  4. def OAI.BoltzmannNonuniqueness.PositiveIteration.inSpatialCone line 66
  5. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.flight_inSpatialCone line 69
  6. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.small_scaled_cone_in_cube line 81
  7. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.restrictedChain_cone_mono line 95